Floyd's Rule (Hoare Calculus)

hoare-calculus

Definition

Floyd's Rule ( Hoare Calculus)

Floyd’s rule or forward assignment provides a way to reason about assignment in a forward direction, meaning it calculates the strongest postcondition from a given precondition . It is defined as:

where is a fresh variable representing the value of before the assignment.

Mechanics

Unlike the backward assignment rule, Floyd’s rule tracks the “history” of the variable:

1. asserts that the precondition held for the old value .
2. asserts that the new value of is the result of evaluating using the old value .

The existential quantifier is necessary because the original value of is “lost” during assignment, but its relationship to the new state must be preserved for the proof.

Example:

Given the triple , applying Floyd’s rule yields:

By substituting with (since ), we obtain:

Complexity

Floyd’s rule is generally more complex to apply manually than the backward rule because it introduces quantifiers. However, it is the more “natural” way to think about program execution as a forward transformation of state.