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. We also give a new logic for $\forall\exists$ properties and prove its alignment completeness.

翻译：在关系验证中，计算步骤的合理对齐有助于使用简单的关系断言来证明程序间的关系。关系霍尔逻辑（RHL）提供了体现多种执行对齐方式的组合规则。看似更灵活的对齐方式可通过基于程序转移关系的乘积自动机来表达。在完备霍尔逻辑基础上，单一退化对齐规则（自组合）构成了针对$\forall\forall$性质且具有通常逻辑完备性的RHL。此前提出的对齐完备性概念被认为是更令人满意的度量标准，部分规则被证明对若干特定形式的对齐自动机具有对齐完备性。本文证明：对于由标准规则与基于带测试克林代数的语义保持重写规则组成的RHL，其对一般类$\forall\forall$对齐自动机具有对齐完备性。我们还针对$\forall\exists$性质提出了一种新逻辑，并证明了其对齐完备性。