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 $v:=e$ in a forward direction, meaning it calculates the strongest postcondition from a given precondition $F$. It is defined as:

$$\{F\}v:=e\{\exists v^{\prime }:F[v^{\prime }/v]\wedge v=e[v^{\prime }/v]\}{}_{\text{(f-asgn)}}$$

where $v^{\prime }$ is a fresh variable representing the value of $v$ before the assignment.

Mechanics

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

1. $F[v^{\prime }/v]$ asserts that the precondition held for the old value $v^{\prime }$.
2. $v=e[v^{\prime }/v]$ asserts that the new value of $v$ is the result of evaluating $e$ using the old value $v^{\prime }$.

The existential quantifier $\exists v^{\prime }$ is necessary because the original value of $v$ is “lost” during assignment, but its relationship to the new state must be preserved for the proof.

Example:

Given the triple $\{x=a\}x:=x+1\{Q\}$, applying Floyd’s rule yields:

$$Q\equiv \exists x^{\prime }:(x^{\prime }=a)\wedge (x=x^{\prime }+1)$$

By substituting $x^{\prime }$ with $a$ (since $x^{\prime }=a$), we obtain:

$$Q\equiv x=a+1$$

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.