(More teaching material for JML is available in JML sourceforge wiki. In particular, Cormac Flanagan's Quicksort homework exercise might be a nice follow-up exercise to give students.)

Exercises with JML and ESC/Java2

The exercises all involve making design decisions explicit by means of JML preconditions and invariants, in the Design-By-Contract style. The aim of the exercises is to experience how making implicit assumptions explicit as preconditions and invariants can help us to detect program bugs, in this case using the automated program verification tool ESC/Java2.

The specification language JML

• requires   for preconditions
• invariant   for invariants (by which we mean class invariants aka object invariants, not loop invariants)
• ensures   for postconditions

The program verification tool ESC/Java2

ESC/Java2 is an automated program verification tool (aka extended static checker) for Java programs. Information on downloading and installing it is available from the ESC/Java2 webpage. (Thanks to Joe Kiniry for keeping ESC/Java(2) alive!) Students here in Nijmegen can use ESC/Java2 on the department computers.

The exercises

• Bag and Amount
• Taxpayer

Some hints to keep you out of trouble with the tool:

• Only look at the first warning that ESC/Java2 produces, and ignore the others, until you've managed to get rid of this first one.
• The only JML keywords you'll need are requires, invariant, and ensures. If you want, you can also use non_null as an abbreviation and experiment with other features.
• Don't use the Java shorthand x+=10 for x = x+10.
• Whenever possible, split invariants than contain conjunctions into several smaller invariants. The tool then provides better feedback. So instead of
     //@ invariant A && B;
  write
     //@ invariant A;
     //@ invariant B;
  The same goes for preconditions (aka requires clauses).
• If the tool complains of invariant violations, it produces a lot of information that is hard to interpret. The crucial information to look at is
  • the line number saying which invariant is violated, and
  • the line number saying where this invariant is violated.
  NB beware that calling a method on some object may break the invariant of another object. For instance, in the taxpayer exercise, calling a method on a TaxPayer may break the invariant of his or her spouse.

Reflection

1. In the end, do you think that you found all problems? Are you certain now that the code is correct?
2. Can you think of ways in which the tool or the specification language could be improved?
3. Instead of the tool we used, can you think of other ways (formal or informal, tool-supported or not) to find the problems that the tool found? If so, would these alternatives
   • find fewer of the problems, the same, or more?
   • find problems sooner or later than the current approach?
   • require more work or less work?
   • provide you with more confidence or less confidence that the code is correct?