Cyclic Proofs in Hoare Logic and its Reverse

TL;DR

This work connects axiomatic and cyclic proof systems for both partial and total Hoare logic and their dual reverse Hoare logic, revealing that cyclic proofs share a uniform rule set across these logics while differing in global soundness conditions. It shows that partial variants rely on coinductive interpretations and total variants on inductive descent, proving soundness directly and relative completeness via translations from standard proofs. The paper also extends cyclic proofs to reverse Hoare logic, demonstrating dualities and providing translations between traditional and cyclic proofs. Together, these results offer a unified, constructive framework for reasoning about correctness and incorrectness in imperative programs, with potential for practical verification tooling.

Abstract

We examine the relationships between axiomatic and cyclic proof systems for the partial and total versions of Hoare logic and those of its dual, known as reverse Hoare logic (or sometimes incorrectness logic). In the axiomatic proof systems for these logics, the proof rules for looping constructs involve an explicit loop invariant, which in the case of the total versions additionally require a well-founded termination measure. In the cyclic systems, these are replaced by rules that simply unroll the loops, together with a principle allowing the formation of cycles in the proof, subject to a global soundness condition that ensures the well-foundedness of the circular reasoning. Interestingly, the cyclic soundness conditions for partial Hoare logic and its reverse are similar and essentially coinductive in character, while those for the total versions are also similar and essentially inductive. We show that these cyclic systems are sound, by direct argument, and relatively complete, by translation from axiomatic to cyclic proofs.

Figures (6)

• Figure 1: Summary of our developments. $\mathtt{PHL}$ (resp. $\mathtt{THL}$) is partial (resp. total) Hoare logic, and $\mathtt{PRHL}$ (resp. $\mathtt{TRHL}$) is partial (resp. total) reverse Hoare logic.
• Figure 2: Operational semantics of while programs.
• Figure 3: Proof rules for Hoare triples. Partial Hoare logic $PHL$ uses the rule $\hbox{(Inv)}$ and total Hoare logic $THL$ uses $\hbox{(Inv-Total)}$, with all other rules shared. Variable $x'$ is fresh in rule $\hbox{($:=$)}$ and variable $t$ is fresh in $\hbox{(Inv-Total)}$.
• Figure 4: Proof rules for reverse Hoare triples. Partial reverse Hoare logic $PRHL$ uses the rules $\hbox{(RInv-Partial)}$, while total reverse Hoare logic $TRHL$ uses $\hbox{(RInv-Total)}$, with all other rules shared. Variable $x'$ is fresh in rule $\hbox{(R:=)}$ and variable $n$ is fresh in $\hbox{(RInv-Total)}$.
• Figure 5: Cyclic proof rules for Hoare triples. $x'$ is fresh in $\hbox{(C:=)}$, and $z$ and $t$ are not in $fv(C)$ in $\hbox{(Sub)}$.

Theorems & Definitions (29)

• definition 1: Validity
• remark 1
• proposition 1: Soundness
• theorem 1: Relative completeness Cook:1978
• remark 2
• proposition 2: Soundness
• proof
• theorem 2: Relative completeness
• definition 2: Pre-proof
• definition 3: Trace Simpson:17