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.
翻译:在关系核查方面,明智地调整计算步骤有助于用简单的关系论来证明程序之间的关系。关系 Hoare逻辑(RHL)提供了包含各种对齐的构成规则。似乎更灵活的调整可以在基于程序过渡关系的产品自动配对中表现。通常情况下,RHL可以使用单一的退化校准规则来完成。调整完整性的概念以前是作为一种更令人满意的措施提出的,它以对齐自动式为基础,而有些规则则表明与少数特定形式的对齐自动式对齐相一致。使用基于Kleene代数的语义保留重写规则来进行测试,显示RHL完全与非常一般的对齐自动对齐等级相一致。除了解决一般对齐性这一开放的问题外,这种基于人类友好语法的推理与便于自动核查的自动表达之间的结果桥梁。