Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Partial Incorrectness Logic

Lena Verscht, Ānrán Wáng, Benjamin Lucien Kaminski

TL;DR

This work develops partial incorrectness logic as a dual to partial/total correctness within Hoare-style reasoning, using Dijkstra-style predicate transformers to relate preconditions and postconditions. It introduces strongest liberal post and weakest liberal pre operators, and shows how partial correctness and partial incorrectness can be established through fixed-point reasoning, aided by Park induction and variant-based termination techniques. The paper further develops reachability analysis via liberal and non-liberal transformers, provides backward-variant rules for proving reachability, and demonstrates applications such as under-approximation triples and backtracking responsibilities to isolate relevant variables and origins. Although focused on deterministic and reversible programs, the framework extends to nondeterministic and irreversible computations and to quantitative expectations, offering a unified, dual perspective on correctness and reachability with practical proof techniques.

Abstract

Reasoning about program correctness has been a central topic in static analysis for many years, with Hoare logic (HL) playing an important role. The key notions in HL are partial and total correctness. Both require that program executions starting in a specified set of initial states (the precondition) reach a designated set of final states (the postcondition). Partial correctness is more lenient in that it does not require termination, effectively deeming divergence acceptable. We explore partial incorrectness logic, which stands in relation to O'Hearn's "total" incorrectness logic as partial correctness does to total correctness: Partial correctness allows divergence, partial incorrectness allows unreachability. While the duality between divergence and unreachability may not be immediately apparent, we explore this relationship further. Our chosen formalism is predicate transformers à la Dijkstra. We focus here on deterministic and reversible programs, though the discussion extends to nondeterministic and irreversible computations, both of which introduce additional nondeterminism that must be addressed.

Partial Incorrectness Logic

TL;DR

This work develops partial incorrectness logic as a dual to partial/total correctness within Hoare-style reasoning, using Dijkstra-style predicate transformers to relate preconditions and postconditions. It introduces strongest liberal post and weakest liberal pre operators, and shows how partial correctness and partial incorrectness can be established through fixed-point reasoning, aided by Park induction and variant-based termination techniques. The paper further develops reachability analysis via liberal and non-liberal transformers, provides backward-variant rules for proving reachability, and demonstrates applications such as under-approximation triples and backtracking responsibilities to isolate relevant variables and origins. Although focused on deterministic and reversible programs, the framework extends to nondeterministic and irreversible computations and to quantitative expectations, offering a unified, dual perspective on correctness and reachability with practical proof techniques.

Abstract

Reasoning about program correctness has been a central topic in static analysis for many years, with Hoare logic (HL) playing an important role. The key notions in HL are partial and total correctness. Both require that program executions starting in a specified set of initial states (the precondition) reach a designated set of final states (the postcondition). Partial correctness is more lenient in that it does not require termination, effectively deeming divergence acceptable. We explore partial incorrectness logic, which stands in relation to O'Hearn's "total" incorrectness logic as partial correctness does to total correctness: Partial correctness allows divergence, partial incorrectness allows unreachability. While the duality between divergence and unreachability may not be immediately apparent, we explore this relationship further. Our chosen formalism is predicate transformers à la Dijkstra. We focus here on deterministic and reversible programs, though the discussion extends to nondeterministic and irreversible computations, both of which introduce additional nondeterminism that must be addressed.

Paper Structure

This paper contains 18 sections, 1 theorem, 8 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Correctness and Termination
  3. Weakest (Liberal) Pre
  4. Total and Partial Correctness
  5. Termination
  6. Proving termination using variants
  7. Incorrectness and Reachability
  8. Strongest (Liberal) Post
  9. Total and Partial Incorrectness
  10. Reachability
  11. Proving reachability using variants
  12. Partial Incorrectness: Applications
  13. Underapproximation triples
  14. Backtracking responsibilities
  15. Conclusion
  16. ...and 3 more sections

Key Result

lemma 1

Let $(X, {\preceq})$ be a complete partial order and $f\colon X \to X$ be monotonic. Then for all $I \in X$,

Figures (2)

  • Figure 1: Termination versus reachability.
  • Figure 2: Calculating the strongest liberal post.

Theorems & Definitions (1)

  • lemma 1: Park Induction