Implication (Hoare Calculus)

hoare-calculus

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

Intuition

If a program $\Pi$ is correct with respect to a precondition $F^{\prime }$ and postcondition $G^{\prime }$, then it is also correct if:

1. We start in a “stricter” state $F$ that satisfies $F^{\prime }$.
2. We end in a state $G^{\prime }$ that satisfies a more “lenient” condition $G$.

This rule is essential for connecting different steps in a Hoare proof, as it allows matching the postcondition of one command with the precondition of the next, even if they are not syntactically identical.

Semantic Requirement

The implications $F⟹F^{\prime }$ and $G^{\prime }⟹G$ are often proven using the semantics of the underlying logic (e.g. predicate logic) rather than the rules of the Hoare calculus itself.