一句话：将契约检查统一重构为并发进程间通信，并在核心演算中嵌入多种监控策略及证明其正确性。
软件工程中契约系统有多种执行策略，如 Eiffel 的前后条件检查、惰性、可选和并行执行等，但每种策略通常都要从零构建监控系统。论文观察到契约本质上是程序与监控器之间的通信，因此把契约检查重构为并发进程之间的通信。该视角揭示了严格、惰性及并发等执行策略之间的内在联系，并将它们嵌入一个核心演算中；作者还通过模拟给出了一种编码的正确性证明。最后，该框架能够启发此前无法表达的新监控方法和契约。
Abstract Contract systems have come to play a vital role in many aspects of software engineering. This has resulted in a wide variety of approaches to enforcing contracts—ranging from the straightforward pre-condition and post-condition checking of Eiffel to lazy, optional, and parallel enforcement strategies. Each of these approaches has its merits, but each has required ground-up development of an entire contract monitoring system. We present a unified approach to understanding this variety, while also opening the door to as-yet-undiscovered strategies. By observing that contracts are fundamentally about communication between a program and a monitor, we reframe contract checking as communication between concurrent processes. This brings out the underlying relations between widely studied enforcement strategies, including strict and lazy enforcement as well as concurrent approaches, including new contracts and strategies. We show how each of these can be embedded into a core calculus, and demonstrate a proof (via simulation) of correctness for one such encoding. Finally, we show that our approach suggests new monitoring approaches and contracts not previously expressible.
@article{paperbot332,
title = {An extended account of contract monitoring strategies as patterns of communication},
author = {CAMERON SWORDS and AMR SABRY and SAM TOBIN-HOCHSTADT},
journal = {Journal of Functional Programming},
volume = {28},
year = {2018},
doi = {10.1017/s0956796818000047}
}