Implication (Hoare Calculus)

hoare-calculus

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

Intuition

If $\Pi$ is correct for $F^{\prime }$ and $G^{\prime }$, then it is also correct for any stronger precondition $F$ and any weaker postcondition $G$.

This rule is used to adapt a proof step when the surrounding assertions do not match exactly.

Example

$$\frac{x>5⟹x>0\{x>0\}x:=2\{x=2\}x=2⟹x\le 3}{\{x>5\}x:=2\{x\le 3\}}{}_{\text{(imp)}}$$

The program assignment is already known to satisfy the middle triple. The rule of consequence then strengthens the precondition from $x>0$ to $x>5$ and weakens the postcondition from $x=2$ to $x\le 3$.

Semantic Requirement

The implications $F⟹F^{\prime }$ and $G^{\prime }⟹G$ are usually proved using the semantics of the underlying logic, not the Hoare calculus itself. This is closely related to monotonicity of entailment.