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 (sequential composition), atop a complete Hoare logic, comprises a RHL for $\forall\forall$ properties that is complete in the sense of Cook. The notion of alignment completeness was previously proposed as an additional 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 sound and alignment complete for a new general class of automata. The $\forall\forall$ and $\forall\exists$ automata are shown to be semantically complete. Thus both logics are complete in the sense of Cook. The paper includes discussion of why alignment is not the only important principle for relational reasoning and proposes entailment completeness as further means to evaluate RHLs.

翻译：在关系验证中，计算步骤的明智对齐有助于使用简单的关系断言证明程序间关系。关系霍尔逻辑（RHL）提供了体现不同执行对齐方式的组合规则。表面上更灵活的对齐方式可以通过基于程序转移关系的乘积自动机来表达。在完备的霍尔逻辑基础上，单个退化对齐规则（顺序组合）构成了针对$\forall\forall$性质的RHL，该逻辑在Cook意义上是完备的。对齐完备性概念先前被提出作为额外度量标准，一些规则已被证明相对于几种特定形式的对齐自动机具有对齐完备性。本文证明了针对$\forall\forall$对齐自动机的一般类别，由标准规则及基于带测试的Kleene代数的语义保持重写规则组成的RHL具有对齐完备性。本文引入了一种新的$\forall\exists$性质逻辑，并证明其相对于新的一般自动机类别是可靠且对齐完备的。研究证明$\forall\forall$和$\forall\exists$自动机具有语义完备性，因此两种逻辑在Cook意义上都是完备的。本文还讨论了为何对齐并非关系推理的唯一重要原则，并提出将蕴涵完备性作为评估RHL的进一步手段。