JML Winter School 2008

The first JML Winter School was held in Orlando, Florida on 23-24 February 2008.

The first day of the tutorial was devoted to showing how to get the Jikes Parser Generator working with JML4 and a simple example of how to generate bytecode for runtime assertation checking (RAC) by extending the Eclipse JDT. The second day was a more in-depth example using loop variants and loop invariants.

JML4 will be based on the next version of Eclipse e.g. 3.4 and will support Java 1.5, unlike previous generation JML tools.