Assignment Rule

The basis of all correctness proofs is provided by the Assignment Rule, which states that the following Hoare tripple is (totally) correct:

$$\langle \alpha[E/x] \rangle \; x := E \; \langle \alpha \rangle$$

Here $E$ is some value, easily computed from the current state variables, either using library functions, or maybe $E$ is a variable or a constant. $x$ is a state variable name, and $\alpha[E/x]$ is the predicate $\alpha$ with $x$ replaced by $E$ where-ever it occurs.

This rule is sound (i.e. does give correct tripples) because if the output to $x := E$ is to satisfy $\alpha$ it is enough that $E$ satisfies the same condition $x$ had to satisfy according to $\alpha$.

It is also complete (i.e. the precondition is as weak (= general) as possible), so $\alpha[E/x]$ is the weakest possible precondition given the piece of code $x := E$ and postcondition $\langle \alpha\rangle$.