Proof systems for partial incorrectness logic (partial reverse Hoare logic)
Yukihiro Oda
TL;DR
The paper addresses partial reverse Hoare logic, formalizing triples $[P]\, C\,[Q]$ whose semantics are the dual of total Hoare logic. It introduces two proof systems, an ordinary PRHL and a CPRHL (cyclic) system, and proves both sound and relatively complete; the ordinary system relies on the weakest pre-condition predicate $wpr(C,Q)$ for completeness, while the cyclic system achieves completeness by transforming cyclic proofs into ordinary ones. The results show that cyclic proofs can avoid explicit loop invariants during proof search, while maintaining equivalence to the ordinary system. This framework enables robust verification of systems where the final state guarantees the initial state (e.g., authentication and digital signatures) and lays groundwork for future extensions to separation logic and other Hoare-style logics.
Abstract
Partial incorrectness logic (partial reverse Hoare logic) has recently been introduced as a new Hoare-style logic that over-approximates the weakest pre-conditions of a program and a post-condition. It is expected to verify systems where the final state must guarantee its initial state, such as authentication, secure communication tools and digital signatures. However, the logic has only been given semantics. This paper defines two proof systems for partial incorrectness logic (partial reverse Hoare logic): ordinary and cyclic proof systems. They are sound and relatively complete. The relative completeness of our ordinary proof system is proved by showing that the weakest pre-condition of a while loop and a post-condition is its loop invariant. The relative completeness of our cyclic proof system is also proved by providing a way to transform any cyclic proof into an ordinary proof.