Exercises 01

Logistic Remarks (pdf)

We'll use the web-interface of Spec# and try a couple of examples.



A readable Spec# tutorial can be found here (pdf, examples archive), it also includes a detailed explanation of object invariants, for those interested.

A set of tutorial slides, that contain many examples clarifying the use and syntax of many of Spec#'s features can be found here (pdf).

  • Jahob: another verification system for Java