将 ?? 关系型霍尔逻辑（Relational Hoare Logic）编码为标准霍尔逻辑（Standard Hoare Logic）

《Proceedings of the ACM on Programming Languages》：Encode the ?? Relational Hoare Logic into Standard Hoare Logic

本文提出一种通用编码理论，将非确定性的??关系哈勒逻辑转化为标准哈勒逻辑，通过重定义三元有效性并封装模式到断言，无需修改逻辑框架或重新验证正确性。

　　

摘要

验证实际程序的功能正确性可以分解为两部分：（1）细化证明，用于证明该程序实现了更抽象的高级程序；（2）在高级层次上的算法正确性证明。关系Hoare逻辑是一种强大的工具，可用于实现细化证明，但通常需要超出标准Hoare逻辑的进一步形式化处理。特别是在非确定性环境中，需要使用??关系Hoare逻辑。现有的方法将这种逻辑编码为包含“幽灵状态”和“不变量”的Hoare逻辑，但这些扩展显著增加了形式化的复杂性和正确性证明的开销。本文提出了一种通用编码理论，可以将??关系Hoare逻辑简化为标准（一元）Hoare逻辑。具体来说，我们建议重新定义关系Hoare三元组（triples）的有效性，同时保留原有的证明规则，然后将??模式封装在断言（assertions）中。我们已经证明，编码后的标准Hoare三元组的有效性与所需的关系Hoare三元组的有效性是等价的。此外，该编码理论还表明，常见的关系Hoare逻辑证明规则实际上是标准Hoare逻辑证明规则的特例，且关系证明步骤对应于标准证明步骤。通过定义一个谓词Exec，我们的理论使标准Hoare逻辑能够证明??关系属性，而无需修改逻辑框架或重新验证正确性。