Differences
This shows you the differences between two versions of the page.
Next revision Both sides next revision | |||
sav08:notion_of_inductive_loop_invariant [2008/02/18 11:22] vkuncak created |
sav08:notion_of_inductive_loop_invariant [2008/02/18 11:42] vkuncak |
||
---|---|---|---|
Line 16: | Line 16: | ||
s2; | s2; | ||
} | } | ||
+ | s3; | ||
} | } | ||
Line 29: | Line 30: | ||
s2; | s2; | ||
} | } | ||
+ | s3; | ||
} | } | ||
- | if the following conditions hold: | + | if the following three conditions hold: |
- | - //I// **holds initially**: in all states satisfying Pre, when execution reaches loop entry, | + | - //I// **holds initially**: in all states satisfying //Pre//, when execution reaches loop entry, //I// holds |
+ | - //I// is **preserved**: if we assume that //I// and the loop condition //(e)// hold, then we can prove that //I// will hold again after executing //s2// | ||
+ | - //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. |