Standard Backward Assignment (Hoare Calculus)

hoare-calculus

Definition

Standard Backward Assignment

The assignment rule describes how an assignment $v:=e$ affects the truth of an assertion $G$. It is defined as:

$$\{G[e/v]\}v:=e\{G\}{}_{\text{(asgn)}}$$

where $G[e/v]$ denotes the substitution of all free occurrences of variable $v$ in $G$ with the expression $e$.

Mechanics

To prove that $G$ holds after the assignment $v:=e$, one must show that $G$ would have held if $v$ had already been replaced by $e$ before the assignment.

This rule is called “backward” because it works from the postcondition to the precondition. It is typically easier to use than the forward assignment rule, as it does not require existential quantifiers to track the “old” value of $v$.

Example

To achieve $x>5$ after $x:=x+1$, the precondition must be:

$$(x+1)>5⟹x>4$$

Thus:

$$\{x>4\}x:=x+1\{x>5\}$$