三十七年的关系Hoare逻辑:对其原则和历史的评论 (Thirty-seven years of relational Hoare logic: remarks on its principles and history)

from arxiv, A version appears in proceedings of ISOLA 2020. Version2: fix typos, minor clarifications, add a citation. Version3: copy edits, add citations on completeness. Version 4: minor corrections

Relational Hoare logics extend the applicability of modular, deductive verification to encompass important 2-run properties including dependency requirements such as confidentiality and program relations such as equivalence or similarity between program versions. A considerable number of recent works introduce different relational Hoare logics without yet converging on a core set of proof rules. This paper looks backwards to little known early work. This brings to light some principles that clarify and organize the rules as well as suggesting a new rule and a new notion of completeness.

翻译：Hoare 关系逻辑扩展了模块和扣减核查的适用性,包括重要的双运行特性,包括依赖性要求,如保密和程序关系,如程序版本之间的等同或相似性。许多近期著作引入了不同的关系 Hoare 逻辑,而没有在核心的一套证据规则上找到一致。本文向后看的是鲜为人知的早期工作。这引出了一些澄清和组织规则以及提出新规则和新完整性概念的原则。