LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

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] (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 //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.