Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:notion_of_inductive_loop_invariant [2008/02/18 11:42] vkuncak |
sav08:notion_of_inductive_loop_invariant [2008/05/29 11:41] (current) 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 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. |