Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:notion_of_inductive_loop_invariant [2008/03/11 08:13] pedagand |
sav08:notion_of_inductive_loop_invariant [2008/05/29 11:41] barbara typo |
||
---|---|---|---|
Line 38: | Line 38: | ||
- //I// is **strong enough**: if we assume that //I// holds and the loop condition //(e)// does not hold, then we can prove that //Post// holds after executing //s3// | - //I// is **strong enough**: if we assume that //I// holds and the loop condition //(e)// does not hold, then we can prove that //Post// holds after executing //s3// | ||
- | Explanation: because //I// holds initially and it is preserved, by induction from **holds initially** and **preserved** follows that //I// will hold in every loop iteration. The **strong enough** condition ensures that when loop terminates, the rest of the program will satisy the desired postcondition. | + | Explanation: because //I// holds initially and it is preserved, by induction from **holds initially** and **preserved** follows that //I// will hold in every loop iteration. The **strong enough** condition ensures that when loop terminates, the rest of the program will satisfy the desired postcondition. |