使关系Hoare逻辑对齐完备
摘要：关于关系验证的议题上，通过具有适当排序的计算步骤我们能够轻松证明程序之间关系，而使用简单的关系断言。关系霍尔逻辑（RHL）提供了一些组合规则来执行各种排序方式。似乎更加灵活的排序方式可以通过基于程序转换关系的乘积自动机来表达。在使用单个退化排序规则时，RHL可以被认为是完整的。关于排序完整性的概念之前被提出为一种更为满意的度量方式，基于排序自动机，并且一些规则已被证明与一些特定的排序自动机形式是排序完整的。通过使用基于Kleene代数与测试的语义保持重写规则，我们证明了一种RHL与一类非常通用的排序自动机是排序完整的。除了解决排序完整性的未解问题，此结果还在人性化的基于语法的推理和有助于自动验证的自动机表示之间建立了桥梁。
作者：Anindya Banerjee, Ramana Nagasamudram, David A. Naumann
论文ID：2212.10338
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-21