Logistic Remarks (pdf)

We'll use the web-interface of Spec# http://rise4fun.com/SpecSharp and try a couple of examples.

Examples.pdf

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).

• Spec# uses the Boogie intermediate language and verification tool, which is also used by
  • VCC (for C)
  • Chalice (concurrency)
  • Dafny (experimental language)

• A specification language for Java is the Java Modelling Language (JML) which is used by e.g.
• KeY Project
• ESC/Java2
• …

• Jahob: another verification system for Java