Auto-active program verification rests on the ability to effectively the translation from annotated programs into verification conditions that are then discharged by automated theorem provers in the background. Characteristic such tools, e.g., Why3, Dafny, and Viper, is that this process does not involve user interaction, expecting all guiding hints like invariants to be given upfront. For sequential correctness, this paradigm is well established, thanks to approaches like weakest precondition generation and symbolic execution. However, to capture temporal properties, the specification language of choice for a broader system perspective, additional concerns and challenges are introduced into the translation and proof. Approaches based on symbolic model-checking can verify such properties on system models, e.g., using automata constructions. However, ascribing temporal properties to structured and data-intensive programs is more difficult. Several program calculi have been proposed in the literature, each of which on their own falls short in some regard of supporting an auto-active workflow. However, all essential ideas, while perhaps some are not widely acknowledged, are in fact found in the literature. In this paper, we demonstrate how to assemble these ideas into a weakest-precondition calculus for linear temporal properties and demonstrate it with examples.

翻译：自动主动式程序验证依赖于将带标注程序有效转换为验证条件的能力，这些验证条件随后由自动化定理证明器在后台处理。诸如Why3、Dafny和Viper等工具的特点是：该过程无需用户交互，要求所有指导性提示（如不变量）均需预先提供。对于顺序正确性，得益于最弱前置条件生成和符号执行等方法，该范式已相当成熟。然而，为捕捉时序属性（从更宏观的系统视角选择的规范语言），转换与证明过程会引入额外的考量与挑战。基于符号模型检测的方法可在系统模型上验证此类属性，例如通过自动机构造实现。但将时序属性赋予结构化且数据密集型的程序则更为困难。文献中已提出多种程序演算方法，各自在支持自动主动式工作流方面均存在不足。然而，所有核心思想（尽管部分可能未获广泛认知）实际上皆已见于文献。本文展示了如何将这些思想整合为面向线性时序属性的最弱前置条件演算，并通过示例加以演示。