Lab for Automated Reasoning and Analysis 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.
  
 
sav08/notion_of_inductive_loop_invariant.txt · Last modified: 2008/05/29 11:41 by barbara
 
© EPFL 2018 - Legal notice