Editing Loop invariant (section)

==Floyd–Hoare logic==
In [[Hoare logic|Floyd–Hoare logic]],<ref>{{cite book 
 | contribution-url=http://www.cse.chalmers.se/edu/year/2017/course/TDA384_LP1/files/lectures/additional-material/AssigningMeanings1967.pdf
 | author=Robert W. Floyd
 | contribution=Assigning Meanings to Programs
 | editor=J.T. Schwartz
 | title=Proceedings of Symposia in Applied Mathematics
 | publisher=American Mathematical Society
 | location=Providence, RI
 | series=Mathematical Aspects of Computer Science
 | volume=19
 | pages=19–32
 | year=1967 }}</ref><ref>{{Cite journal
 |last1=Hoare 
 |first1=C. A. R. 
 |author-link1=C.A.R. Hoare 
 |title=An axiomatic basis for computer programming 
 |doi=10.1145/363235.363259 
 |journal=[[Communications of the ACM]] 
 |volume=12 
 |issue=10 
 |pages=576&ndash;580 
 |date=October 1969 
 |s2cid=207726175 
 |url=http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf 
 |url-status=dead 
 |archive-url=https://web.archive.org/web/20160304013345/http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf 
 |archive-date=2016-03-04 
}}</ref> the [[partial correctness]] of a [[while loop]] is governed by the following rule of inference:

:<math>\frac{\{C\land I\}\;\mathrm{body}\;\{I\}} {\{I\}\;\mathtt{while}\ (C)\ \mathrm{body}\;\{\lnot C\land I\}}</math>

This means:
* If some property {{mvar|I}} is preserved by the code <math>\mathrm{body}</math> —more precisely, if {{mvar|I}} holds after the execution of <math>\mathrm{body}</math> whenever both {{mvar|C}} and {{mvar|I}} held beforehand— ''(upper line)'' then
* {{mvar|C}} and {{mvar|I}} are guaranteed to be false and true, respectively, after the execution of the whole loop <math>\mathtt{while}\ (C)\ \mathrm{body}</math>, provided {{mvar|I}} was true before the loop ''(lower line)''.

In other words: The rule above is a deductive step that has as its premise the [[Hoare triple]] <math>\{C\land I\}\;\mathrm{body}\;\{I\}</math>.  This triple is actually a [[relation (mathematics)|relation]] on machine states.  It holds whenever starting from a state in which the boolean expression <math>C\land I</math> is true and successfully executing some code called <math>\mathrm{body}</math>, the machine ends up in a state in which {{mvar|I}} is true.  If this relation can be proven, the rule then allows us to conclude that successful execution of the program <math>\mathtt{while}\ (C)\ \mathrm{body}</math> will lead from a state in which {{mvar|I}} is true to a state in which <math>\lnot C\land I</math> holds.  The boolean formula {{mvar|I}} in this rule is called a loop invariant.

With some variations in the notation used, and with the premise that the loop halts, this rule is also known as the '''Invariant Relation Theorem'''.<ref name="conway-gries">{{cite book |last1=Conway |first1=Richard |author-link1=Richard W. Conway |last2=Gries |first2=David |author-link2=David Gries|year=1973 |title=An Introduction to Programming: A Structured Approach using PL/1 and PL/C |publisher=Winthrop |location=Cambridge, Massachusetts | pages=198–200 }}</ref><ref>{{cite book | title=Software Error Detection through Testing and Analysis | author-first=J. C. | author-last= Huang | publisher=John Wiley & Sons |location= Hoboken, New Jersey | year= 2009 | pages=156–157 }}</ref>  As one 1970s textbook presents it in a way meant to be accessible to student programmers:<ref name="conway-gries"/>

Let the notation <code>P { seq } Q</code> mean that if <code>P</code> is true before the sequence of statements <code>seq</code> run, then <code>Q</code> is true after it.  Then the invariant relation theorem holds that

:<code>P & c { seq } P</code>
::implies   
:<code>P { DO WHILE (c); seq END; } P & ¬c</code>

===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.