CSSE 373 Formal Methods in Specification and Design

HW10

Purpose: experiment with specifying classes using JML and checking specifications using JMLUnitNG

This is a team homework assignment. All work must be done by the team members together. All team members should understand all work submitted. If you have concerns about your own understanding or that of your teammates, please let me know. I want everyone to learn all they can in this course!

Please note: The JML tool chain is very much research quality. A much improved version is in development, but has complex installation requirements. So, we’re using a simpler subset of the tools. 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 by committing an Eclipse project.

2. Make sure your Eclipse environment is set up correctly:

   1. Install Java 1.6 JDK or newer
   2. Install Eclipse 3.5 or newer
   3. Install Subclipse
   4. Install the TestNG framework as described in the slides for session 28.

3. Check out the HW10/HW10 project from your homework team SVN repository. That is, within your repo navigate to HW10, then check out the HW10 Eclipse project inside that first-level folder. In that project you’ll find two Java class declarations:

   • 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, then set up appropriate and run JMLUnitNG tests to tests the classes. 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.

   Notes:

   • Get the tests passing using the default data generation strategies first.
   • Once the tests pass with the default strategies, edit the data generation strategies to try some values beyond -1, 0, and 1. See this usage page for more information on how to do that.
   • Stick with basic specifications like we used in the Stack and JMLUnitTestExample projects in class.
5. Commit your Eclipse project back to your team SVN repository when done, and more often as needed. 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.