Lab for Automated Reasoning and Analysis LARA

Lecturecise 2: Background

Background review

More on inductive invariants

Code contracts

Fun with Spec#

Solutions

Example of the pen-and-paper proof for an invariant to be inductive. Note that the notation is slightly different from Scala's syntax.

SOME SOLVED EXERCISES

Exercises with Solutions

  • please contact Viktor Kuncak with questions and corrections, and feel free to discuss the solutions with colleagues

References

 
sav13/lecturecise_02.txt · Last modified: 2013/04/09 21:18 by vkuncak
 
© EPFL 2018 - Legal notice