Totally Correct Program (Hoare Calculus)

program-proofing

Definition

Total Correctness

A program $\Pi$ is totally correct with respect to a precondition $P$ and a postcondition $Q$ if it is partially correct and guaranteed to terminate for all inputs satisfying $P$.

$$\text{Total Correctness}=\text{Partial Correctness}+\text{Termination}$$

In Hoare notation, this is sometimes denoted using square brackets:

$${\models }_{tot}[P]\Pi [Q]$$

Formal Semantics

A triple $\{F\}\Pi \{G\}$ is totally correct if for all states $\sigma \in \mathcal{S}$:

$$[F]\sigma =1⟹{\sigma }^{\prime }=[\Pi ]\sigma \text{ is defined}\wedge [G]{\sigma }^{\prime }=1$$

Verification

Proving total correctness is generally more difficult than proving partial correctness because it requires an additional proof of termination.

1. Partial Correctness: Proven using standard Hoare calculus rules and invariants.
2. Termination: Proven by identifying a loop variant (or termination function)—a mapping from the program state to a well-founded set (typically the natural numbers $\mathbb{N}$) that strictly decreases with each iteration.

Non-Determinism

For non-deterministic programs, total correctness requires that all possible execution paths terminate and satisfy the postcondition.