修正编排的契约

分布式交互可以通过编排进行适当设计。此类抽象可被视为多个分布式参与方协调的全局描述。全局断言通过用逻辑公式标注多方会话类型来验证交换消息的内容，从而定义编排的契约。引入此类约束是一个关键的设计问题，因为可能很难指定允许各方在不违反契约的情况下取得进展的契约。在本文中，我们提出了三种自动修正不一致全局断言的方法。通过讨论其适用性以及修正后的全局断言与原始（不一致）断言之间的关系，对这些方法进行了比较。