Conditional (Hoare Calculus)

hoare-calculus

Definition

Conditional Rule

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

where is a boolean expression.

Reasoning

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

1. If the condition is true, the then-branch () leads to .
2. If the condition is false, the else-branch () leads to .

In both cases, the precondition is augmented with the knowledge of whether the branch condition 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:

Case Analysis

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