一句话：用抽象解释统一刻画正确性与不正确性转换式程序逻辑，并给出构造可靠完备证明系统的计算式方法。
本文研究转换式程序逻辑中的正确性（correctness）与不正确性（incorrectness），并扩展它们以显式处理终止与非终止。作者证明这些逻辑可视为自然关系语义的右像变换器的抽象解释，该语义同时涵盖有穷与无穷执行。这一视角使不同逻辑可通过各自对语义的抽象进行比较，而非通过更困难的形式证明系统比较。更重要的是，该形式化提供了构造性方法：通过对语义做抽象，可计算出可靠且完备的形式证明系统。作为示例，作者将 Hoare 逻辑扩展至覆盖非确定性程序的所有可能行为，并设计出一种新的前置条件（不）正确性逻辑。
We study transformational program logics for correctness and incorrectness that we extend to explicitly handle both termination and nontermination. We show that the logics are abstract interpretations of the right image transformer for a natural relational semantics covering both finite and infinite executions. This understanding of logics as abstractions of a semantics facilitates their comparisons through their respective abstractions of the semantics (rather that the much more difficult comparison through their formal proof systems). More importantly, the formalization provides a calculational method for constructively designing the sound and complete formal proof system by abstraction of the semantics. As an example, we extend Hoare logic to cover all possible behaviors of nondeterministic programs and design a new precondition (in)correctness logic.
@article{paperbot2621,
title = {Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation},
author = {Patrick Cousot},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632849}
}