LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav07_lecture_4 [2007/03/28 14:49]
cedric.jeanneret
sav07_lecture_4 [2007/03/28 18:14] (current)
vkuncak
Line 99: Line 99:
  
 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 (under construction) ==== ==== References about weakest precondition (under construction) ====
-  * (some online references will come here)+  * [[http://​www.soe.ucsc.edu/​%7Ecormac/​papers/​popl01.ps|Avoiding Exponential Explosion: Generating Compact Verification Conditions]]
   * Back, Wright: Refinement Calculus   * Back, Wright: Refinement Calculus
   * Edsger W. Dijkstra: A Discipline of Programming   * Edsger W. Dijkstra: A Discipline of Programming
   * C. A. R. Hoare, He Jifeng: Unifying Theories of Programming   * C. A. R. Hoare, He Jifeng: Unifying Theories of Programming
- 
- 
- 
- 
  
 ===== Modeling data structures ===== ===== Modeling data structures =====