LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Last revision Both sides next revision
sav08:notion_of_inductive_loop_invariant [2008/02/18 11:42]
vkuncak
sav08:notion_of_inductive_loop_invariant [2008/03/11 08:13]
pedagand
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 satisy the desired postcondition.