Com S 362 --- Object-Oriented Analysis and Design

	   HOMEWORK 9: JUNIT AND DESIGN BY CONTRACT IN JML
		 (File $Date: 2003/04/08 03:50:36 $)

Due: Problem 1, April 16, 2003, at 11AM.

This is an individual homework; it should *not* be done in teams.

1. [JUnit and JML]

Readings for JML: A Notation for Detailed Design by Leavens, Baker,
and Ruby, April 2001. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds
(editors), Behavioral Specifications of Businesses and Systems,
chapter 12, pages 175-188. Copyright Kluwer, 1999. Available from
http://www.jmlspecs.org.
For a JML reference, see the "Preliminary Design of JML: A Behavioral
Interface Specification Language for Java", by Leavens, Baker, and
Ruby, April 2003.  This is also availble from http://www.jmlspecs.org.

For this individual problem first make a copy, in your own directory,
of the file HistoricalData.java which is in
/home/course/cs362/public/homework/hw9/ on the department Linux machines.
For example:

    $ cp /home/course/cs362/public/homework/hw9/HistoricalData.java .

This file is also available from the course web page.

a. (30 points)
Write a JUnit test class, named HistoricalDataTest,
which does unit testing on the class HistoricalData.
(Hint: you can use Eclipse to generate a skeleton test file that has a
main method with the "text ui" interface to get started on this.)
You should write a test that has a test method for each method
of HistoricalDataTest. (You don't have to write a separate test for
HistoricalData's constructor or for the toString method if you don't
want to.  Note that a subclass of TestCase should have a public
constructor as follows
	    public HistoricalDataTest(String name) { super(name); }
that takes a single string as an argument, and calls the constructor
of TestCase with that string.) We will grade your work on the clarity
and completeness of your test.

Run your test with the JUnit textual interface on the supplied version
of HistoricalDataTest.  It should find failures on all the methods.

Hand in a printout of your HistoricalDataTest class and the output
from this test run.

b. (15 points)
Implement the class HistoricalData by replacing each of the lines
indicated in the file.  Your code should pass the JUnit test you wrote
for it.  It should also follow good Java style.  Furthermore, use
the minimum possible amount of run-time space for objects of type
HistoricalData.  (Hint, you may find it convenient to use
Double.NEGATIVE_INFINITY in your code.)

Make a printout of the code for HistoricalData to hand in at this
point.

c. (10 points)
Write a design class diagram for your implementation of HistoricalData
that includes its fields and methods.  This can be handwritten.

Hand in your design class diagram.

d. (30 points)
Write, in JML, a specification for each of the methods in the class
HistoricalData.  These should appear as annotations in your code.
Your specification should include at least 
(i) a normal postcondition (ensures clause) for each method (including
toString) and for the constructor,
(ii) any necessary preconditions (requires clauses, also see below),
and (iii) an invariant.  Except in the specification of the toString
and hashCode methods, you are not allowed to use any informal descriptions,
written (* ... *), in the JML specifications.  The invariant can
be a private invariant.  You should write pre- and postconditions for any
new methods you wish to add as well.

Whatever data fields you declare in your implementation should
probably be declared to be spec_public in JML.

About the preconditions -- Java's type double has three special values:
NaN (not a number), and positive and negative infinity.
We don't want to allow these as measurements added to the HistoricalData.
Thus your specification should require that these special values are
never given as measurements.  Note that NaN is quite special when used
in comparisons in Java; to reliably test for it, use the static method
Double.isNaN, which takes a double as an argument.

You don't have to write heavyweight specifications in JML.
You should instead use lightweight specifications as discussed in
class; that is for methods, just "requires" and "ensures" clauses.
The preconditions you write should be enough to guarantee that no
exceptions are thrown, unless you want to use more sophisticated
features of JML.

Note that for the equals, hashCode, clone, and toString methods,
any specifications you write have to start with the JML keyword "also".

Hint: JML has operators \sum and \max which you may find convenient to
use to specify the method addAll.  For example, 
   (\sum int i; 0 <= i && i < 3; i + 4.0)
    == 0+4.0 + 1+4.0 + 2+4.0
    == 15.0
See section 3.1 of the "Preliminary Design of JML" for details on these.  

Compile your code and its specification using the JML runtime
assertion checking compiler, jmlc, as follows.  First change
directories into the Eclipse workspace subdirectory containing your
file (c:\eclipse\workspace\hw9 or some such on Windows), or export
the files HistoricalData.java and HistoricalDataTest.java from Eclipse
into a directory you can find.  Then from that directory, execute:

          $ javac HistoricalDataTest.java
	  $ jmlc -p HistoricalData.java

Then (without recompiling HistoricalData.java!) run your JUnit tests
again, as follows.

          $ jmlrac HistoricalDataTest

(If you run the tests from within Eclipse, be sure that the
jmlruntime.jar file is in the project build path.  It's found in the
JML/bin directory, e.g., in /opt/JML/bin/jmlruntime.jar on Linux.)
Fix any errors in your specifications (or in your code) as
pointed out by the runtime assertion checker, until your code passes
the tests without assertion violations or failures.

Hand in a printout of your code for HistoricalData.java with the JML
annotations. 

e. (5 points)
Did you find any errors in your code from using JML (either during the
writing of the specifications or the testing) that were not found
just by using the JUnit tests?  If so, briefly describe them.