Correct Program

program-proofing

Definition

Correct Program

A correct program is a program that satisfies its specification.

More precisely, for a precondition $F$ and a postcondition $G$, the program is correct if every input state that satisfies $F$ leads, after execution, to a state that satisfies $G$.

Idea

The correctness statement can be read as:

• the precondition describes the allowed inputs,
• the program transforms those inputs,
• the postcondition describes the required result.

For every state $\sigma \in \mathcal{S}$, if $[F]\sigma$ is true, then the resulting state ${\sigma }^{\prime }=[\Pi ]\sigma$ should also make $[G]{\sigma }^{\prime }$ true.

Correctness

Partial Correctness

Definition

Partially Correct Program

A program $\Pi$ is partially correct with respect to a precondition $P$ and a postcondition $Q$ if, for every execution that starts in a state satisfying $P$ and terminates, the resulting state satisfies $Q$.

In Hoare notation, this is written as:

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

Link to original

Total Correctness

Definition

Totally Correct Program

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]$$

Link to original

Methods

Hoare Calculus

Definition

Hoare Calculus

The Hoare calculus is a calculus for reasoning about the correctness of programs. It uses Hoare triples together with axioms and inference rules to show that a program transforms states satisfying a precondition into states satisfying a postcondition.

Link to original

Weakest Precondition

Definition

Weakest Precondition

The weakest precondition of a program $\Pi$ and a postcondition $G$ is the most general (least restrictive) formula $\mathrm{wp}(\Pi ,G)$ such that the Hoare triple $\{\mathrm{wp}(\Pi ,G)\}\Pi \{G\}$ is totally correct.

Equivalently, $\mathrm{wp}(\Pi ,G)$ characterises exactly the states from which $\Pi$ terminates in a state satisfying $G$.

$$\{\mathrm{wp}(\Pi ,G)\}=\{\sigma \in \mathcal{S}\mid [\Pi ]\sigma \text{ is defined and }[G]([\Pi ]\sigma )=\text{true}\}$$

If a precondition $F$ implies $\mathrm{wp}(\Pi ,G)$, then $\{F\}\Pi \{G\}$ is totally correct.

Link to original

Annotation Calculus

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\}$.

Link to original

Strongest Postcondition

Definition

Strongest Postcondition

The strongest postcondition of a program $\Pi$ and a precondition $F$ is the most specific (most restrictive) formula $\mathrm{sp}(F,\Pi )$ such that the Hoare triple $\{F\}\Pi \{\mathrm{sp}(F,\Pi )\}$ is partially correct.

Equivalently, it is the set of states reached by executing $\Pi$ from states satisfying $F$:

$$\{\mathrm{sp}(F,\Pi )\}=\{[\Pi ]\sigma \mid \sigma \in \{F\}\text{ and }[\Pi ]\sigma \text{ is defined}\}$$ $$=[\Pi ](\{F\})$$

If a postcondition $G$ is implied by $\mathrm{sp}(F,\Pi )$, then $\{F\}\Pi \{G\}$ is partially correct.

Link to original

Examples

$\{1\}x:=2\{x=2\}$

This specification is totally correct and therefore also partially correct. The assignment always terminates, and after execution the value of $x$ is $2$, which satisfies the postcondition.

$\{1\}x:=2\{x=3\}$

This specification is neither totally correct nor partially correct. The program terminates, but the final value of $x$ is always $2$, so the postcondition $x=3$ is never satisfied. A counterexample is any state, since the postcondition fails after execution.

$\{1\}\text{while }x>2\text{ do }x:=x-1\{x=2\}$

This specification is neither totally correct nor partially correct under the given precondition. If the initial state has $x=0$, the loop condition is false and the program terminates immediately with $x=0$, so the postcondition fails. Hence even partial correctness does not hold.

$\{1\}\text{while }x\ne 2\text{ do }x:=x-1\{x=2\}$

This specification is partially correct but not totally correct. Whenever the loop terminates, it does so with $x=2$, so the postcondition is satisfied. However, for some initial states, such as $x=0$, the loop decreases $x$ forever and never reaches $2$, so termination is not guaranteed.

$\{x>5\}\text{while }x\ne 2\text{ do }x:=x-1\{x=2\}$

This specification is totally correct and therefore also partially correct. The precondition ensures that the loop starts from a value greater than $5$, so repeated decrements must eventually reach $2$. The program then terminates with $x=2$, which satisfies the postcondition.

Example

$\{x=x_0\wedge y=y_0\}$

$z:=0;$

$\text{while }y\ne 0\text{ do }$

$z:=z+x;$

$y:=y-1$

$\text{od}$

$\{z=x_0\ast y_0\}$

The postcondition is the expected product computation: the loop adds $x$ to $z$ exactly once for each decrement of $y$.

This is partially correct because whenever the loop terminates, the value of $z$ is the product $x_0\ast y_0$.

However, it is not automatically totally correct, because if $y<0$ initially, then $y$ moves away from $0$ and the loop never terminates.

To obtain total correctness, the precondition must be strengthened with $y\ge 0$.

Example

$\{x\ge 1\}$

$\text{while }x>1\text{ do}$

$\text{if }x=(x/2)\ast 2\text{ then }$

$x:=x/2$

$\text{else}$

$x:=3\ast x+1$

$\text{fi}$

$\text{od}$

$\{x=1\}$

This specification is partially correct: whenever the program terminates, the final value is $x=1$, which satisfies the postcondition.

However, it is not known whether the program always terminates for every input with $x\ge 1$. Therefore, total correctness is an open question here, as expressed by the Collatz conjecture.

Example

$\{x\ge 2\}$

$y:=2;$

$\text{while }y<x\wedge \neg (\text{lstPrim}(y)\wedge \text{lstPrim}(2x-y))\text{ do}$

$y:=y+1$

$\text{od}$

$\{\text{lstPrim}(y)\wedge \text{lstPrim}(2x-y)\}$

The program searches for two prime numbers whose sum is $2x$. It is partially correct because, if it terminates, the postcondition states exactly what the program has found.

It is also totally correct for the stated precondition, because the loop can only iterate finitely many times: $y$ starts at $2$ and increases by $1$ until it reaches $x$.

The deeper mathematical question is whether the postcondition is always reachable, which is the content of the Goldbach conjecture.

$\{1\}\Pi \{1\}$

This specification is partially correct for every program $\Pi$, because if the program terminates, the postcondition $1$ is always true.

It is totally correct exactly when $\Pi$ terminates for every input state.

$\{1\}\Pi \{0\}$

This specification is partially correct only if $\Pi$ never terminates on any input state. If the program ever terminates, then the postcondition $0$ fails.

It is never totally correct, because total correctness would require termination and satisfaction of $0$ at the same time.

$\{0\}\Pi \{1\}$

This specification is partially correct and totally correct for every program $\Pi$.

The precondition is false, so there are no allowed input states. The specification is therefore vacuously true.

$\{0\}\Pi \{0\}$

This specification is also partially correct and totally correct for every program $\Pi$.

Again, the precondition is false, so the specification is vacuously true.