Exercises with JML and ESC/Java3

Bag and Amount exercises

For these exercises, you should specify the two classes

with JML and run ESC/Java2 to verify these specifications. Simply put, you run ESC/Java2 on these files and if the tool produces some warning, you

either add annotation to the code (eg to document invariants, preconditions, or postconditions)
or fix bugs in the code

to make the warning go away. You have to use your own best judgement to choose between these two options, but there are some deliberate bugs in the code for you to detect, with the help of the tool. Note that there are some deliberate errors in the code for you to find.

For Amount.java you must also try to formalise the informal invariant that is discussed in the file as a JML invariant, which should reveal some more problems in the code.

In the end, ESC/Java2 should run without any complaints on the annotated code. ESC/Java2 complains (among other things) if it thinks a runtime exception may occur, say a NullPointerException, so if ESC/Java2 runs without complaints this means it has verified that no runtime exceptions can occur.

More detailed instructions are given in the Java files. Read these!