Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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)
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 ===
 
sav08/proving_correctness_of_some_small_examples.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice