Choreographic programming is a paradigm where developers write the global specification (called choreography) of a communicating system, and then a correct-by-construction distributed implementation is compiled automatically. Unfortunately, it is possible to write choreographies that cannot be compiled, because of issues related to an agreement property known as knowledge of choice. This forces programmers to reason manually about implementation details that may be orthogonal to the protocol that they are writing. Amendment is an automatic procedure for repairing uncompilable choreographies. We present a formalisation of amendment from the literature, built upon an existing formalisation of choreographic programming. However, in the process of formalising the expected properties of this procedure, we discovered a subtle counterexample that invalidates the original published and peer-reviewed pen-and-paper theory. We discuss how using a theorem prover led us to both finding the issue, and stating and proving a correct formulation of the properties of amendment.
翻译:舞蹈编程是一种范式,即开发者编写通信系统的全球规格(称为舞蹈),然后自动编译一个按部就班的分布式实施。 不幸的是,有可能写出无法编辑的舞蹈,因为与协议属性有关的问题被称为选择知识。这迫使编程者手工解释可能与他们正在编写的协议相形见绌的执行细节。修正是修复不兼容的舞蹈的自动程序。我们以现有的舞蹈编程正规化为基础,从文献中提出修正的正规化。然而,在将这一程序的预期属性正规化的过程中,我们发现了一个微妙的反比示例,它使原始出版的和同行评审的笔纸理论无效。我们讨论使用标本证明如何使我们找到问题,并表明和证明修正的正确表述。</s>