Editing Hoare logic (section)

===Assignment axiom schema===

The assignment axiom states that, after the assignment, any predicate that was previously true for the right-hand side of the assignment now holds for the variable. Formally, let {{mvar|P}} be an assertion in which the variable {{mvar|x}} is [[Free variables and bound variables|free]]. Then:

<!-- NB: This version of the axiom schema is sound. Do not exchange the precondition with the postcondition. -->
: <math>\dfrac{}{\{P[E/x]\} x := E \{P\}}</math>

where <math>P[E/x]</math> denotes the assertion {{mvar|P}} in which each [[Free variables and bound variables|free occurrence]] of {{mvar|x}} has been [[Substitution (logic)|replaced]] by the expression {{mvar|E}}.

The assignment axiom scheme means that the truth of <math>P[E/x]</math> is equivalent to the after-assignment truth of {{mvar|P}}. Thus were <math>P[E/x]</math> true prior to the assignment, by the assignment axiom, then {{mvar|P}} would be true subsequent to which. Conversely, were <math>P[E/x]</math> false (i.e. <math>\neg P[E/x]</math> true) prior to the assignment statement, {{mvar|P}} must then be false afterwards.

Examples of valid triples include:
:*<math>\{ x+1 = 43 \}   y := x + 1   \{ y = 43 \}</math>
:*<math>\{ x + 1 \leq N \}  x := x  + 1  \{ x \leq N \}</math>

All preconditions that are not modified by the expression can be carried over to the postcondition. In the first example, assigning <math>y:=x+1</math> does not change the fact that <math>x+1=43</math>, so both statements may appear in the postcondition. Formally, this result is obtained by applying the axiom schema with {{mvar|P}} being (<math>y=43</math> and <math>x+1=43</math>), which yields <math>P[(x+1)/y]</math> being (<math>x+1=43</math> and <math>x+1=43</math>), which can in turn be simplified to the given precondition <math>x+1=43</math>.

The assignment axiom scheme is equivalent to saying that to find the precondition, first take the post-condition and replace all occurrences of the left-hand side of the assignment with the right-hand side of the assignment. Be careful not to try to do this backwards by following this ''incorrect'' way of thinking: <math>\{P\} x:=E \{P[E/x]\}</math>;
this rule leads to nonsensical examples like:
: <math>\{ x = 5 \} x := 3 \{ 3 = 5 \}</math>

Another ''incorrect'' rule looking tempting at first glance is <math>\{P\} x:=E \{P \wedge x=E\}</math>; it leads to nonsensical examples like:
: <math>\{ x = 5 \}   x := x + 1   \{ x = 5 \wedge x = x + 1 \}</math>

While a given postcondition {{mvar|P}} uniquely determines the precondition <math>P[E/x]</math>, the converse is not true. For example:
:*<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}   x := y \cdot y   \{ 0 \leq x \wedge x \leq 9 \}</math>,
:*<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}   x := y \cdot y   \{ 0 \leq x \wedge y\cdot y \leq 9 \}</math>,
:*<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}   x := y \cdot y   \{ 0 \leq y\cdot y \wedge x \leq 9 \} </math>, and
:*<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}   x := y \cdot y   \{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}</math>
are valid instances of the assignment axiom scheme.

The assignment axiom proposed by Hoare ''does not apply'' when more than one name may refer to the same stored value. For example,
: <math>\{ y = 3 \}   x := 2   \{ y = 3 \}</math>
is wrong if {{mvar|x}} and {{mvar|y}} refer to the same variable ([[aliasing (computing)|aliasing]]), although it is a proper instance of the assignment axiom scheme (with both <math>\{P\}</math> and <math>\{P[2/x]\}</math> being <math>\{y=3\}</math>).