论文标题
三十七年的关系hoare逻辑：关于其原理和历史的评论
Thirty-seven years of relational Hoare logic: remarks on its principles and history
论文作者
论文摘要
关系hoare逻辑扩展了模块化，演绎验证的适用性，以涵盖重要的2次属性，包括依赖性要求，例如机密性和程序关系，例如等价或程序版本之间的相似性。最近的许多作品引入了不同的关系hoare逻辑，而没有融合一组核心证明规则。本文向后看鲜为人知的早期工作。这阐明了一些澄清和组织规则的原则，并提出了新的规则和新的完整概念。
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.
