Hoare Triple

logic verification hoare-calculus

Definition

Hoare Triple

A Hoare triple is a construct used in Hoare calculus to describe how the execution of a piece of code changes the state of the computation. It is written as:

$$\{P\}\Pi \{Q\}$$

where:

• $P$ is the precondition: an assertion that must hold before the execution of $\Pi$.
• $\Pi$ is the command or program fragment.
• $Q$ is the postcondition: an assertion that must hold after $\Pi$ terminates.

Semantics

The meaning of a Hoare triple depends on whether we consider partial or total correctness.

Partial Correctness

Partial Correctness

The triple $\{P\}\Pi \{Q\}$ holds under partial correctness if, whenever $\Pi$ starts in a state satisfying $P$ and if it terminates, then the resulting state satisfies $Q$.

This is often denoted as:

$${\models }_{par}\{P\}\Pi \{Q\}$$

Total Correctness

Total Correctness

The triple $[P]\Pi [Q]$ (or sometimes $\{P\}\Pi \{Q\}$ with explicit termination) holds under total correctness if, whenever $\Pi$ starts in a state satisfying $P$, it must terminate, and the resulting state satisfies $Q$.

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

Formal Verification

In program verification, Hoare triples are used as the building blocks for proofs. The goal is to show that a program is partially correct or totally correct with respect to its specification given by the precondition and postcondition.