现在它能编译了！不可编译协议的可认证自动修复
计算机科学中的逻辑
2023-03-01 v1 编程语言
摘要
choreographic 编程是一种范式，开发者编写通信系统的全局规范（称为 choreography），然后自动编译出构造即正确的分布式实现。遗憾的是，由于与称为选择知识（knowledge of choice）的协议属性相关的问题，可能会写出无法编译的 choreography。这迫使程序员手动推理可能与其所写协议正交的实现细节。Amendment 是一种修复不可编译 choreography 的自动过程。我们基于已有的 choreographic 编程形式化，给出了文献中 amendment 的形式化。然而，在形式化该过程预期属性的过程中，我们发现了一个微妙的反例，它推翻了原先发表并经过同行评审的纸笔理论。我们讨论了如何使用定理证明器引导我们发现该问题，并陈述和证明 amendment 属性的一个正确表述。
引用
@article{arxiv.2302.14622,
title = {Now It Compiles! Certified Automatic Repair of Uncompilable Protocols},
author = {Luís Cruz-Filipe and Fabrizio Montesi},
journal= {arXiv preprint arXiv:2302.14622},
year = {2023}
}