Partial Incorrectness Logic

TL;DR

This paper introduces a new logic for reasoning about program unreachability and divergence, extending traditional correctness logic to better handle partial correctness and divergence in deterministic programs.

Contribution

It develops the concept of partial incorrectness logic, relating divergence and unreachability, and formalizes it using predicate transformers for deterministic and reversible programs.

Findings

Defines partial incorrectness logic as an extension of correctness logic.

Explores the relationship between divergence and unreachability.

Provides a formal framework using predicate transformers.

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 \`a 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.