Lecturecise 2: Background
More on inductive invariants
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
- please contact Viktor Kuncak with questions and corrections, and feel free to discuss the solutions with colleagues