Hoare Calculus

hoare-calculus

Definition

Hoare Calculus

Hoare calculus is a formal system used to reason about the correctness of programs. It uses a set of axioms and inference rules to prove that if a program starts in a state satisfying a specific condition (precondition), it will end in a state satisfying another condition (postcondition).

Properties

Soundness

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

Completeness

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)

$$\{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 for the strengthening of the precondition and the weakening of the postcondition. It is formally expressed as:

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

where:

• $F⟹F^{\prime }$ means that $F$ is stronger than $F^{\prime }$ (it restricts the state space more).
• $G^{\prime }⟹G$ means that $G$ is weaker than $G^{\prime }$ (it is a more general requirement).

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

Partial Correctness

Definition

Partial Correctness

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

Total Correctness

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

Examples

Example: 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 choice for $F$ and $G$ are:

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

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