Simplified Forward Assignment (Hoare Calculus)

hoare-calculus

Definition

Simplified Forward Assignment

Under specific side conditions, the assignment rule can be simplified to:

$$\{F\}v:=e\{F\wedge v=e\}{}_{\text{(s-asgn)}}$$

Side Conditions:

1. $v$ does not occur in $F$.
2. $v$ does not occur in $e$.

Intuition

This rule is a special case of Floyd’s rule. When the variable $v$ is not present in the precondition $F$ or the expression $e$, the “old” value of $v$ does not influence the validity of $F$, and the facts in $F$ remain unchanged by the assignment.

Derivation from Floyd’s Rule

Applying the full Floyd’s rule $\{F\}v:=e\{\exists v^{\prime }:F[v^{\prime }/v]\wedge v=e[v^{\prime }/v]\}$ with the side conditions:

• $F[v^{\prime }/v]=F$ (since $v\notin F$)
• $e[v^{\prime }/v]=e$ (since $v\notin e$)

The postcondition becomes $\exists v^{\prime }:(F\wedge v=e)$. Since $v^{\prime }$ no longer appears in the formula, the quantifier can be dropped, yielding $F\wedge v=e$.

Restricted Use

This rule is invalid if the side conditions are not met. For example, $\{x=1\}x:=2\{x=1\wedge x=2\}$ is correct, but $\{x=1\}x:=x+1\{x=1\wedge x=x+1\}$ results in a contradiction ($x=1\wedge x=2$).