The behavior of concurrent, asynchronous procedures depends in general on the call context, because of the global protocol that governs scheduling. This context cannot be specified with the state-based Hoare-style contracts common in deductive verification. Recent work generalized state-based to trace contracts, which permit to specify the internal behavior of a procedure, such as calls or state changes, but not its call context. In this article we propose a program logic of context-aware trace contracts for specifying global behavior of asynchronous programs. We also provide a sound proof system that addresses two challenges: To observe the program state not merely at the end points of a procedure, we introduce the novel concept of an observation quantifier. And to combat combinatorial explosion of possible call sequences of procedures, we transfer Liskov's principle of behavioral subtyping to the analysis of asynchronous procedures.

翻译：并发异步过程的行为通常依赖于调用上下文，这是由于控制调度的全局协议所致。这种上下文无法通过演绎验证中常见的基于状态的Hoare式合约来指定。近期研究将状态合约泛化为迹合约，允许指定过程的内部行为（如调用或状态变化），但无法指定其调用上下文。本文提出了一种上下文感知迹合约的程序逻辑，用于指定异步程序的全局行为。我们还提供了一个可靠的证明系统，以应对两个挑战：为观察过程端点之外的程序状态，我们引入了观察量词的新颖概念；为应对过程调用序列组合爆炸问题，我们将Liskov行为子类型化原则迁移至异步过程的分析中。