Conditional (Hoare Calculus)

hoare-calculus

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.

Reasoning

To prove that a conditional statement satisfies a postcondition $G$ starting from $F$, one must show that:

1. If the condition $e$ is true, the then-branch ($\Pi$) leads to $G$.
2. If the condition $e$ is false, the else-branch ($\Omega$) leads to $G$.

In both cases, the precondition is augmented with the knowledge of whether the branch condition $e$ was satisfied or not.

One-sided Conditional

For an if-then statement without an else branch (implicitly else skip), the rule simplifies using the skip rule:

$$\frac{\{F\wedge e\}\Pi \{G\}F\wedge \neg e⟹G}{\{F\}\mathbf{if}e\mathbf{then}\Pi \mathbf{fi}\{G\}}$$

Case Analysis

The conditional rule is essentially a form of case analysis on the value of the guard $e$.