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.

翻译：我们研究了面向正确性与不正确性的变换程序逻辑，并将其扩展以显式处理终止与非终止两种情况。我们证明，这些逻辑是对涵盖有限与无限执行的自然关系语义的右像变换器的抽象解释。将逻辑理解为语义的抽象，有助于通过它们对语义的各自抽象进行比较（而非通过其形式证明系统进行更困难的比较）。更重要的是，该形式化提供了一种计算方法，通过语义抽象建设性地设计出完备且正确的形式证明系统。作为示例，我们将霍尔逻辑扩展以覆盖非确定性程序的所有可能行为，并设计了一种新的前置条件（不）正确性逻辑。