CSSE 373 Formal Methods in Specification and Design

HW10

Purpose: practice specifying classes using JML and checking specifications using ESC/Java2

Please note: The JML tool chain is very much research quality. There are improved versions of the tools, but they have complex installation requirements. So, we’re using a simpler, older version of the tools, even though they are less robust. I hope that this will minimize installation pain while still letting us get a feel for what the future may hold as the tools improve.

1. Keep track of how much time you spend on this assignment. Please put in your best effort, but don’t spend too much time battling the tools. Unlike previous assignments you will submit your answers by committing annotated Java files at the end of the homework.
2. Install the Mobius PVE, create a new workspace, and a new project (with ESC/Java nature) by carefully following these instructions.

3. Copy the following two Java class declarations into your new project:

   • Amount.java—a class representing amounts in euros and cents
   • Bag.java—a class representing a “multiset”) of ints

4. In general terms, your task is to annotate the two classes with JML specifications using the Design-by-Contract style. You’ll add:

   • invariant clauses to specify facts that must always be true about the classes
   • requires and ensures clauses to specify method pre- and post-conditions

   For this assignment, you do not need to specify assignable clauses, though you certainly may.

   1. Specify and fix the Amount class first. There are additional instructions in the comments at the beginning of that file. Note that the code has some subtle bugs in it. Part of your challenge is to determine whether your specification is wrong or the code is wrong. Your final solution should be concisely specified and correctly implemented.
   2. Next specify and fix the Bag class. Like Amount, there are additional instructions in the comments. Unlike Amount, I give you less information about what invariants should hold for the class. Use the method names and the general idea of a multi-set to come up with an appropriate specification.

   Some crucial hints:

   • ESC/Java2 detects possible null pointer dereferences. If it indicates that a field access or method call on a parameter—say x—might involve a null pointer, you can add a pre-condition that says x != null. Now the checker will be happy with the field access or method call, but will check that you never pass null as the value for parameter x.
   • ESC/Java2 detects possible violations of JML pre-conditions, post-conditions, and class invariants. It places an error marker in the side bar. Hover the mouse over the side bar to see a description of the problem.
   • ESC/Java2 deals poorly with assignment operators. Don’t use x += 10, instead use x = x + 10.
   • ESC/Java2 does not support Java 5 generics. An on-going NSF grant is working to remedy this.

   • Break up invariants and pre-conditions to get better warning messages. Instead of

     //@ invariant A && B;

     write

     //@ invariant A;
//@ invariant B;

   • Use JML → Go to associated declaration. If you select a red-underlined ESC/Java2 warning in the code, this menu item will take you to the pre-condition or invariant that may be violated at the site of the warning. An easy way to select the red-underlined bit is to click on the red warning marker in the left margin.
   • Warnings may change without warning. As you change your specifications, save the file to force ESC/Java2 to run. Note that a warning may change after a run, even though the warning marker is in the same place. For example, you might have a ”possible negative array index” warning on a line of code. You add a pre-condition to force the index to be non-negative. The negative-index warning might disappear, but be replaced with a ”possible too large array index” warning at the same location.
5. Copy your annotated Amount.java and Bag.java files to the appropriate HW folder in your individual subversion repository for this course. Add and commit them. You do not need to turn in a pdf for this assignment.

This assignment is based on one by Erik Poll at Radboud University Nijmegen.