为某些和所有的完全关系Höare逻辑进行对齐
摘要：关于关系验证，在计算步骤的恰当对齐下，使用简单的关系断言可以证明程序之间的关系。关系 Hoare 逻辑 (RHL) 提供了组合规则，其中包含了各种执行对齐的方式。看似更灵活的对齐方式可以基于程序转换关系来表示为乘积自动机。在完整的 Hoare 逻辑之上，一个单一的退化对齐规则 (自身复合) 组成了一个对于全量性质 $forallforall$ 的 RHL，在常规逻辑意义上是完备的。对于衡量完备性的概念，之前提出了对齐完备性作为一种更令人满意的度量，并且证明了一些规则相对于一些自发的对齐自动机形式是对齐完备的。本文证明了对于一般类别的 $forallforall$ 对齐自动机，关于由标准规则以及基于带测试 Kleene 代数的语义保持改写规则组成的 RHL 的对齐完备性。我们还给出了一个关于 $forallexists$ 性质的新逻辑，并证明了其对齐完备性。
作者：Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
论文ID：2307.10045
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-20