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 (Cook'78). 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. Recent work by D'Osualdo et al highlights the importance of completeness relative to assumptions (which we term entailment completeness), and presents $\forall\forall$ examples seemingly beyond the scope of RHLs. Additional rules enable these examples to be proved in our RHL, shedding light on the open problem of entailment completeness.

翻译：在关系验证中，对计算步骤的合理对齐有助于利用简单的关系断言证明程序间的关系。关系霍尔逻辑（RHL）提供了一系列组合规则，体现了执行过程的不同对齐方式。看似更灵活的对齐方式可通过基于程序转移关系的乘积自动机来表达。在完备的霍尔逻辑基础上，单一退化对齐规则（自组合）构成了针对全称全称（∀∀）性质的RHL，该逻辑在常规逻辑意义上具有完备性（Cook'78）。对齐完备性概念此前被提出作为更令人满意的衡量标准，部分规则被证明针对几种特设对齐自动机形式具有对齐完备性。本文证明：对于由标准规则与基于带测试Kleene代数的语义保持重写规则组成的RHL，该逻辑针对一般类别的∀∀对齐自动机具有对齐完备性。我们提出了一种针对全称存在（∀∃）性质的新逻辑，并证明其对齐完备性。进一步证明∀∀和∀∃自动机具有语义完备性，因此这两种逻辑在常规意义上均完备。D'Osualdo等人近期的工作强调了相对于假设的完备性（我们称为蕴含完备性）的重要性，并展示了看似超出RHL表达范围的∀∀实例。通过增加额外规则，这些实例可在我们的RHL中得到证明，这为蕴含完备性的开放问题提供了新的见解。