- English only

# Lab for Automated Reasoning and Analysis LARA

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