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. Seemingly more flexible alignments can be expressed in terms of product automata based on program transition relations. A RHL can be complete, in the ordinary sense, using a single degenerate alignment rule. The notion of alignment completeness was previously proposed as a more satisfactory measure, based on alignment automata, and some rules were shown to be alignment complete with respect to a few ad hoc forms of alignment automata. Using a rule of semantics-preserving rewrites based on Kleene algebra with tests, an RHL is shown to be alignment complete with respect to a very general class of alignment automata. Besides solving the open problem of general alignment completeness, this result bridges between human-friendly syntax-based reasoning and automata representations that facilitate automated verification.

翻译：在关系验证中，计算步骤的合理对齐有助于使用简单的断言证明程序间的关系。关系霍尔逻辑（RHL）提供了体现各种对齐方式的组合规则。看似更灵活的对齐可以通过基于程序转移关系的乘积自动机表述。从常规意义上，RHL可采用单一退化对齐规则达到完备性。此前提出的对齐完备性概念，基于对齐自动机作为更合理的度量标准，并针对少数特定形式的对齐自动机证明了某些规则的完备性。本文利用基于带测试的克莱尼代数的语义保持重写规则，证明了一种RHL对于非常普遍的对齐自动机类别具有对齐完备性。该结果不仅解决了通用对齐完备性的开放问题，还架起了友好的人机交互式语法推理与便于自动化验证的自动机表示之间的桥梁。