一句话：为 Actor 语言提出两种递归结构的新型契约，用于约束消息接收者及其通信行为，并证明 blame 分配的正确性。
Actor 语言以异步消息传递建模并发，但组件往往隐式假设其通信伙伴的行为，随着系统复杂度上升，这些假设未被满足时会导致组件难以组合与集成。本文将契约式设计（design-by-contract）引入 Actor 程序，提出两种新型契约：一种用于表达对消息期望接收者的属性约束，另一种用于约束该接收者的通信行为；由于契约具有递归结构，它们可以管辖整条通信链。作者在 Scheme 的 Actor 扩展上实现了该契约系统，对其给出形式化描述，并规定契约违反时如何分配 blame。最后，作者通过形式化并证明一个 blame 正确性定理，证明该契约系统及其 blame 分配机制是正确的。
Actor languages model concurrency as processes that communicate through asynchronous message sends. Unfortunately, as the complexity of these systems increases, it becomes more difficult to compose and integrate their components. This is because of assumptions made by components about their communication partners which may not be upheld when they remain implicit. In this paper, we bring design-by-contract programming to actor programs through a contract system that enables expressing constraints on receiver-related properties. Expressing properties about the expected receiver of a message, and about this receiver’s communication behavior, requires two novel types of contracts. Through their recursive structure, these contracts can govern entire communication chains. We implement the contract system for an actor extension of Scheme, describe it formally, and show how to assign blame in case of a contract violation. Finally, we prove our contract system and its blame assignment correct by formulating and proving a blame correctness theorem.
@article{VandenbogaerdeS24,
title = {Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts},
author = {Bram Vandenbogaerde and Quentin Stiévenart and Coen De Roover},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674643}
}