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. | ||