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 .

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:

Sequential Composition

Assertions are placed between statements to link them:

where and must be valid.

Conditional

Branching statements require annotations in both branches:

While Loop

Loops require the specification of a loop invariant :

Verification Condition Generation

To prove a Hoare triple using the annotation calculus:

1. Annotate the program starting from the postcondition (working backwards) or the precondition (working forwards).
2. Ensure that every adjacent pair is a valid Hoare triple.
3. For every point where two assertions meet (e.g., at the start of the program where the user-defined meets the calculated ), prove the implication .

Examples

Conditional

The conditional is annotated by splitting the proof into the then and else branches.

The postcondition after the fi is the disjunction of the two branch-specific strongest postconditions.

Swapping Values

To verify the swapping of two variables and with initial values :

Relationship to WP

The process of annotating a program backwards from a postcondition 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.