Annotation Calculus

hoare-calculus program-proofing

Definition

Annotation Calculus

The annotation calculus is a system for verifying the correctness of programs by systematically inserting assertions (annotations) between statements. It serves as a more readable, linear alternative to the Hoare calculus tree representation, effectively “tracking” the state through the program.

An annotated program consists of a sequence of commands and assertions $\{F_0\}{\Pi }_1\{F_1\}{\Pi }_2\dots \{F_n\}$.

Rules

The rules of the annotation calculus correspond to the inference rules of the Hoare calculus.

Assignment

The assertion before an assignment is typically derived using the backward assignment rule:

$$\{G[e/v]\}v:=e\{G\}$$

Sequential Composition

Assertions are placed between statements to link them:

$$\{F\}\Pi ;\{G\}\Omega \{H\}$$

where $\{F\}\Pi \{G\}$ and $\{G\}\Omega \{H\}$ must be valid.

Conditional

Branching statements require annotations in both branches:

$$\{F\}\mathbf{if}e\mathbf{then}\{F\wedge e\}\Pi \{G\}\mathbf{else}\{F\wedge \neg e\}\Omega \{G\}\mathbf{fi}\{G\}$$

While Loop

Loops require the specification of a loop invariant $I$:

$$\{I\}\mathbf{while}e\mathbf{do}\{I\wedge e\}\Pi \{I\}\mathbf{od}\{I\wedge \neg e\}$$

Verification Condition Generation

To prove a Hoare triple $\{P\}\Pi \{Q\}$ using the annotation calculus:

1. Annotate the program $\Pi$ starting from the postcondition $Q$ (working backwards) or the precondition $P$ (working forwards).
2. Ensure that every adjacent pair $\{A\}\Pi \{B\}$ is a valid Hoare triple.
3. For every point where two assertions $F,F^{\prime }$ meet (e.g., at the start of the program where the user-defined $P$ meets the calculated $F^{\prime }$), prove the implication $F⟹F^{\prime }$.

Examples

Example: Swapping Values

To verify the swapping of two variables $x$ and $y$ with initial values $x_0,y_0$:

$$\begin{array}{rl}& \{x=x_0\wedge y=y_0\}\\ & t:=x;\\ & \{t=x_0\wedge y=y_0\}\\ & x:=y;\\ & \{t=x_0\wedge x=y_0\}\\ & y:=t\\ & \{y=x_0\wedge x=y_0\}\end{array}$$

Relationship to WP

The process of annotating a program backwards from a postcondition $Q$ is essentially a step-by-step calculation of the weakest liberal precondition.

Verification Conditions

In complex programs, especially those with loops, the annotation calculus generates verification conditions (VCs), logical formulas that must be proven valid to ensure the correctness of the program.