A foundational characterization of Hoare Logic
This resolves a long-standing open problem in program verification by establishing the precise logical power of Hoare Logic.
The authors prove that partial-correctness assertions about iterative programs are provable in Hoare Logic if and only if they are provable in second-order logic with comprehension restricted to first-order predicates, providing the first correct foundational characterization of Hoare Logic.
We show that a partial-correctness assertion about an iterative program is provable in Hoare Logic iffit is provable in standard second-order logic with comprehension restricted to first-order predicates. This equivalence was claimed twice in the past, both with faulty proofs, and seems to be the first foundational characterization of Hoare Logic.