Ramana Nagasamudram ; Anindya Banerjee ; David A. Naumann - Alignment complete relational Hoare logics for some and all

lmcs:13921 - Logical Methods in Computer Science, November 10, 2025, Volume 21, Issue 4 - https://doi.org/10.46298/lmcs-21(4:21)2025
Alignment complete relational Hoare logics for some and allArticle

Authors: Ramana Nagasamudram ; Anindya Banerjee ; David A. Naumann

    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.


    Volume: Volume 21, Issue 4
    Published on: November 10, 2025
    Accepted on: September 18, 2025
    Submitted on: July 11, 2024
    Keywords: Logic in Computer Science

    Consultation statistics

    This page has been seen 299 times.
    This article's PDF has been downloaded 129 times.