LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision Both sides next revision
sav07_lecture_4_skeleton [2007/03/22 20:34]
vkuncak
sav07_lecture_4_skeleton [2007/03/22 20:43]
vkuncak
Line 8: Line 8:
  
 We use weakest preconditions,​ although you could also use strongest postconditions or any other variants of the conversion from programs to formulas. We use weakest preconditions,​ although you could also use strongest postconditions or any other variants of the conversion from programs to formulas.
 +
  
 ===== More on wp ===== ===== More on wp =====
Line 64: Line 65:
  
 Benefit: if there is x_{n+1} that is not changed, we do not need to write its properties in the loop invariant. ​ This can make loop invariant shorter. Benefit: if there is x_{n+1} that is not changed, we do not need to write its properties in the loop invariant. ​ This can make loop invariant shorter.
 +
 +==== References about weakest precondition (in construction) ====
 +  * Back, Wright: Refinement Calculus
 +  * Dijkstra
 +  * Hoare, He
  
 ===== Modeling data structures ===== ===== Modeling data structures =====