• English only

# Differences

This shows you the differences between two versions of the page.

 sav08:proving_correctness_of_some_small_examples [2010/02/22 12:16]vkuncak sav08:proving_correctness_of_some_small_examples [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2010/02/23 12:31 vkuncak 2010/02/22 12:16 vkuncak 2010/02/22 12:13 vkuncak 2009/02/17 23:36 vkuncak 2008/02/17 19:26 vkuncak 2008/02/17 19:22 vkuncak 2008/02/17 19:22 vkuncak 2008/02/17 19:21 vkuncak 2008/02/17 19:18 vkuncak 2008/02/17 19:04 vkuncak 2008/02/17 19:04 vkuncak 2008/02/17 19:03 vkuncak created2008/02/17 18:56 vkuncak 2008/02/17 18:38 vkuncak 2008/02/17 18:37 vkuncak 2008/02/17 18:37 vkuncak 2008/02/17 18:35 vkuncak 2008/02/17 17:20 vkuncak created Next revision Previous revision 2010/02/23 12:31 vkuncak 2010/02/22 12:16 vkuncak 2010/02/22 12:13 vkuncak 2009/02/17 23:36 vkuncak 2008/02/17 19:26 vkuncak 2008/02/17 19:22 vkuncak 2008/02/17 19:22 vkuncak 2008/02/17 19:21 vkuncak 2008/02/17 19:18 vkuncak 2008/02/17 19:04 vkuncak 2008/02/17 19:04 vkuncak 2008/02/17 19:03 vkuncak created2008/02/17 18:56 vkuncak 2008/02/17 18:38 vkuncak 2008/02/17 18:37 vkuncak 2008/02/17 18:37 vkuncak 2008/02/17 18:35 vkuncak 2008/02/17 17:20 vkuncak created 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: + + ++++| + \begin{equation*} + r = i * x \land i=i+1 \land r' = r + x \rightarrow r' = i' * x + \end{equation*} + ++++ + * we will see methods to prove such invariants === Transforming iterative version === === Transforming iterative version ===