Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:proving_correctness_of_some_small_examples [2010/02/22 12:16] vkuncak |
sav08:proving_correctness_of_some_small_examples [2010/02/23 12:31] vkuncak |
||
---|---|---|---|
Line 46: | Line 46: | ||
* [[Notion of inductive loop invariant]] | * [[Notion of inductive loop invariant]] | ||
* What is and is not inductive loop invariant in this example | * What is and is not inductive loop invariant in this example | ||
+ | |||
+ | A verification condition formula for preserving an invariant: | ||
+ | |||
+ | ++++| | ||
+ | \[ | ||
+ | r = i * x \land i=i+1 \land r' = r + x \rightarrow r' = i' * x | ||
+ | \] | ||
+ | ++++ | ||
+ | * we will see methods to prove such invariants | ||
=== Transforming iterative version === | === Transforming iterative version === |