Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties. This paper presents a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that any functional correctness property proven for a choreography also holds for its compiled implementation.

翻译：编排式编程是一种以自顶向下方式开发并发或分布式系统的范式。程序（称为编排）详细描述了进程间所需的交互，并可通过消息传递编译为分布式实现。编排式语言通常能保证无死锁性，并提供编排及其编译实现之间的操作对应关系，但迄今为止鲜有研究验证其他性质。本文提出了一种用于推理编排行为的霍尔风格逻辑，并通过代表性示例阐述了其应用。我们证明该逻辑是可靠且完备的，并讨论了其判定的可判定性。利用编排式编程的现有成果，我们证明：对编排证实的任何功能正确性属性，同样适用于其编译实现。