In relational verification, judicious alignment of computational steps facilitates proof of relations between programs using simple relational assertions. Relational Hoare logics (RHL) provide compositional rules that embody various alignments of executions. Seemingly more flexible alignments can be expressed in terms of product automata based on program transition relations. A single degenerate alignment rule (self-composition), atop a complete Hoare logic, comprises a RHL for $\forall\forall$ properties that is complete in the ordinary logical sense. The notion of alignment completeness was previously proposed as a more satisfactory measure, and some rules were shown to be alignment complete with respect to a few ad hoc forms of alignment automata. This paper proves alignment completeness with respect to a general class of $\forall\forall$ alignment automata, for a RHL comprised of standard rules together with a rule of semantics-preserving rewrites based on Kleene algebra with tests. A new logic for $\forall\exists$ properties is introduced and shown to be alignment complete. The $\forall\forall$ and $\forall\exists$ automata are shown to be semantically complete. Thus the logics are both complete in the ordinary sense.

翻译：在关系验证中，计算步骤的精确对齐有助于使用简单的关系断言来证明程序间的关系。关系霍尔逻辑（RHL）提供了包含多种执行对齐方式的组合推理规则。基于程序转移关系构建的乘积自动机可表达看似更灵活的对齐方式。在完备霍尔逻辑基础上，单一退化对齐规则（自组合）构成了适用于全称-全称（∀∀）性质的RHL，该逻辑在普通逻辑意义上具有完备性。本文提出比对对齐完备性更合理的度量标准，并证明某些规则针对若干特定形式的对齐自动机具有对齐完备性。本研究证明，由标准规则与基于带测试的克林代数（KAT）的语义保持重写规则构成的RHL，对一般类别的通用全称-全称（∀∀）对齐自动机具有对齐完备性。我们进一步提出适用于全称-存在（∀∃）性质的新型逻辑，并证明其对齐完备性。通过证明∀∀和∀∃自动机的语义完备性，表明这两种逻辑在普通意义上均具有完备性。