Specifying and Verifying Future Conditions

doi:10.1007/978-3-032-07106-4_5

2026-01-01

PRE

Yahui Song *

Darius Foo

Wei-Ngan Chin

DOI：10.1007/978-3-032-07106-4_5

原文链接

原文求助

摘要

En 中文

本文形式化定义了未来条件，其补充了传统的先条件和后条件，以提供对每个函数行为和期望的更全面规范。先条件规定了每次函数调用前的所需状态，而后条件定义了完成后的即时结果（后状态）。未来条件通过指定函数调用结束后出现的预期时序行为和状态来扩展此范式，这些状态可能影响后续操作或程序状态。这三类条件共同形成了一种强大的规范机制，用于在各种时序上下文中推理API行为。然而，现有未来条件推理技术存在三个关键局限性：蕴含检查效率低下、程序行为下近似不足以及循环展开受限。为解决这些挑战，我们提出了一套过近似的Hoare风格前向规则，可处理每方法声明仅处理一次的未来条件。此外，我们提出了一种新颖的解决方案，通过未来条件袋来建模递归行为，这些条件可被启发式综合并在验证系统中进行验证。我们在Coq中正式证明了我们提案的正确性，并使用实验结果证明其在检测非平凡、真实世界API误用方面的有效性。

Keyword:

Future Conditions

Hoare Logic

Linear Temporal Logic

Separation Logic

Coq Proof Assistant