Editing Loop invariant (section)

===Example===
The following example illustrates how this rule works.  Consider the program

 while (x < 10)
     x := x+1;

One can then prove the following Hoare triple:

:<math>\{x\leq10\}\; \mathtt{while}\ (x<10)\ x := x+1\;\{x=10\}</math>

The condition ''C'' of the <code>while</code> loop is <math>x<10</math>.  A useful loop invariant {{mvar|I}} has to be guessed; it will turn out that <math>x\leq10</math> is appropriate.  Under these assumptions it is possible to prove the following Hoare triple:

:<math>\{x<10 \land x\leq10\}\; x := x+1 \;\{x\leq10\}</math>

While this triple can be derived formally from the rules of Floyd-Hoare logic governing assignment, it is also intuitively justified: Computation starts in a state where <math>x<10 \land x\leq10</math> is true, which means simply that <math>x<10</math> is true.  The computation adds 1 to {{mvar|x}}, which means that <math>x\leq10</math> is still true (for integer x).

Under this premise, the rule for <code>while</code> loops permits the following conclusion:

:<math>\{x\leq10\}\; \mathtt{while}\ (x<10)\ x := x+1 \;\{\lnot(x<10) \land x\leq10\}</math>

However, the post-condition <math>\lnot(x<10)\land x\leq10</math> ({{mvar|x}} is less than or equal to 10, but it is not less than 10) is [[Logical equivalence|logically equivalent]] to <math>x=10</math>, which is what we wanted to show.

The property <math>0 \leq x</math> is another invariant of the example loop, and the trivial property <math>\mathrm{true}</math> is another one.
Applying the above inference rule to the former invariant yields <math>\{0 \leq x\}\; \mathtt{while}\ (x<10)\ x := x+1\;\{10 \leq x\}</math>.
Applying it to invariant <math>\mathrm{true}</math> yields <math>\{\mathrm{true}\}\; \mathtt{while}\ (x<10)\ x := x+1\;\{10 \leq x\}</math>, which is slightly more expressive.