Hoare Calculus

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.

Properties

Soundness

The Hoare calculus is sound. Every statement about the correctness of a program proven using the Hoare calculus is true.

Completeness

The Hoare calculus is complete. Every statement about the correctness of a program is provable using the Hoare calculus, if the validity of occurring formulas can be proven.

Triple

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.

Link to original

Inference Rules

Empty Program

Definition

Empty Program (Hoare Calculus)

The empty program skip does nothing. It leaves the program state unchanged.

In Hoare notation, this means:

$$\{F\}\mathbf{skip}\{F\}{}_{\text{(skip)}}$$

Link to original

Sequential Composition

Definition

Sequential Composition (Hoare Calculus)

The composition rule allows for reasoning about the execution of two programs in sequence ($\Pi ;\Omega$). It is defined as:

$$\frac{\{F\}\Pi \{G\}\{G\}\Omega \{H\}}{\{F\}\Pi ;\Omega \{H\}}{}_{\text{(comp)}}$$

Link to original

Implication

Definition

Implication (Rule of Consequence)

The rule of consequence allows the precondition to be strengthened and the postcondition to be weakened.

Formally,

$$\frac{F⟹F^{\prime }\{F^{\prime }\}\Pi \{G^{\prime }\}{G}^{\prime }⟹G}{\{F\}\Pi \{G\}}{}_{\text{(imp)}}$$

Here, $F⟹F^{\prime }$ means that $F$ is stronger than $F^{\prime }$, and $G^{\prime }⟹G$ means that $G$ is weaker than $G^{\prime }$.

Link to original

Standard Backward Assignment

Definition

Standard Backward Assignment

The assignment rule describes how an assignment $v:=e$ affects the truth of an assertion $G$. It is defined as:

$$\{G[e/v]\}v:=e\{G\}{}_{\text{(asgn)}}$$

where $G[e/v]$ denotes the substitution of all free occurrences of variable $v$ in $G$ with the expression $e$.

Link to original

Forward Assignment

Definition

Floyd's Rule ( Hoare Calculus)

Floyd’s rule or forward assignment provides a way to reason about assignment $v:=e$ in a forward direction, meaning it calculates the strongest postcondition from a given precondition $F$. It is defined as:

$$\{F\}v:=e\{\exists v^{\prime }:F[v^{\prime }/v]\wedge v=e[v^{\prime }/v]\}{}_{\text{(f-asgn)}}$$

where $v^{\prime }$ is a fresh variable representing the value of $v$ before the assignment.

Link to original

Simplified Forward Assignment

Definition

Simplified Forward Assignment

Under specific side conditions, the assignment rule can be simplified to:

$$\{F\}v:=e\{F\wedge v=e\}{}_{\text{(s-asgn)}}$$

Side Conditions:

1. $v$ does not occur in $F$.
2. $v$ does not occur in $e$.

Link to original

Conditional

Definition

Conditional Rule

The conditional rule allows for reasoning about branching statements (if-then-else). It is defined as:

$$\frac{\{F\wedge e\}\Pi \{G\}\{F\wedge \neg e\}\Omega \{G\}}{\{F\}\mathbf{if}e\mathbf{then}\Pi \mathbf{else}\Omega \mathbf{fi}\{G\}}{}_{\text{(if)}}$$

where $e$ is a boolean expression.

Link to original

Correctness

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

Link to original

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

Axioms

An axiom is a Hoare triple that is valid without premises.

Specific empty-program axiom

$\{x=1\}\mathbf{skip}\{x=1\}$ is a correct axiom, but very specific.

General empty-program axiom

$\{F\}\mathbf{skip}\{F\}$, for arbitrary $F$, is a correct axiom and much more general.

Incorrect overgeneralisation

$\{F\}\mathbf{skip}\{G\}$, for arbitrary $F$ and $G$, is not correct. For example, $\{x>0\}\mathbf{skip}\{x>1\}$ is false when $\sigma (x)=1$.

Abort axiom

$\{F\}\mathbf{abort}\{G\}$ is a correct axiom for partial correctness. The program never reaches a final state, so the postcondition is never violated.

A special case is

$$\{1\}\mathbf{abort}\{0\}$$

which is also correct by the rule of consequence.

Examples

Swapping values

$$\frac{\frac{P\Rightarrow F[x/t]\{F[x/t]\}t:=x\{F\}}{\{P\}t:=x\{F\}}\text{(imp)}\frac{\frac{F\Rightarrow G[y/x]\{G[y/x]\}x:=y\{G\}}{\{F\}x:=y\{G\}}\text{(imp)}\frac{G\Rightarrow Q[t/y]\{G[t/y]\}y:=t\{Q\}}{\{G\}y:=t\{Q\}}\text{(imp)}}{\{F\}x:=y;y:=t\{Q\}}\text{(sc)}}{\{P:x=x_0\wedge y=y_0\}t:=x;x:=y;y:=t\{Q:x=y_0\wedge y=x_0\}}\text{(sc)}$$

We have to find a $F,G$, such that:

$$\begin{array}{rl}\text{(i)}& P\Rightarrow F[x/t]\\ \text{(ii)}& F\Rightarrow G[y/x]\\ \text{(iii)}& G\Rightarrow Q[t/y]\end{array}$$

are tautologies.

Two obvious choices for $F$ and $G$ are:

$$\begin{array}{rl}\text{(ii)}& F\equiv G[y/x]\\ \text{(iii)}& G\equiv Q[t/y]\end{array}$$

program backwards.

Start with the final postcondition $Q$. For the assignment $y:=t$, the standard backward choice is the weakest precondition $Q[t/y]$. So we choose:

$$G\equiv Q[t/y]$$

Then (iii) becomes immediate.

Apply the same idea once more to $x:=y$. Its backward choice is:

$$F\equiv G[x/y]$$

Then (ii) becomes immediate.

So $F$ and $G$ are chosen to make the last two proof obligations hold automatically. Only (i) remains to be checked.

Thus, we still have to show that $P\Rightarrow F[x/t]$, i.e. show that

$$P\Rightarrow Q[t/y][y/x][x/t]$$

is a valid statement.

$$\begin{array}{rlrl}P& \Rightarrow Q[t/y][y/x][x/t]& & \\ (x=x_0\wedge y=y_0)& \Rightarrow (x=y_0\wedge y=x_0)[t/y][y/x][x/t]& & \\ (x=x_0\wedge y=y_0)& \Rightarrow (x=y_0\wedge t=x_0)[y/x][x/t]& & \\ (x=x_0\wedge y=y_0)& \Rightarrow (y=y_0\wedge t=x_0)[x/t]& & \\ (x=x_0\wedge y=y_0)& \Rightarrow (y=y_0\wedge x=x_0)& & \square \end{array}$$