In the setting of message passing software, De Nicola and Hennessy must-preorder defines when a program improves on another one. Since this preorder does not come equipped with a viable proof method, using it requires an alternative relation that characterises it. The literature presents at least four different definitions of such alternative preorders, depending on whether communication is synchronous or asynchronous and on whether there is value-passing or not. The existence of these different definitions complicates the overall theory, hinders the development of tools, and, upon the whole, suggests a lack of understanding of the properties necessary and sufficient to reason on the must-preorder. This paper presents the first alternative characterisation that works at least in all the four settings mentioned above. We achieve this result thanks to an axiomatic approach that is calculus independent, by highlighting the role of blocking and non-blocking actions, and by introducing the novel notion of label abstraction. Label abstractions capture the essence of safe substitutivity w.r.t. interactions, and they let us obtain a unique proof of soundness and a unique proof of completeness that work in all the mentioned settings. We believe this generalises and simplifies the overall theory, while letting us present the existing results in a uniform way. Our proofs are constructive and our result is entirely mechanised in Rocq.

翻译：在消息传递软件的背景下，De Nicola与Hennessy提出的must-预序定义了程序改进另一个程序的条件。由于该预序本身未配备可行的证明方法，使用它需要一种替代关系来对其刻画。现有文献至少提出了四种不同的替代预序定义，这些定义取决于通信是同步还是异步，以及是否存在值传递。这些不同定义的存在使整体理论复杂化，阻碍了工具的开发，并且总体上表明对推理must-预序所必需和充分的属性缺乏理解。本文首次提出了一种至少在上述四种场景中均适用的替代刻画。我们通过一种独立于演算的公理化方法，强调阻塞与非阻塞动作的作用，并引入新颖的标签抽象概念，取得了这一成果。标签抽象捕捉了关于交互的安全可替换性本质，使我们能够获得在所有提及场景中均有效的唯一正确性证明和唯一完备性证明。我们相信这概括并简化了整体理论，同时使我们能够以统一的方式呈现现有结果。我们的证明是构造性的，且全部结果在Rocq中实现了机械化。