Back to CSci 420/520 Homepage.
In this problem, you will be given parts of a Java program that implements a simple-minded academia system. You are to apply ESC/Java to this program and resolve any error warnings that are presented by the tool.
Make sure you have ESC/Java 2 running as described in the tools setup document.
Download academia.java. You will need to add a variety of annotation in order for ESC/Java to give it a "clean bill of health". You are to use checked annotations only (i.e., you cannot use "assume" or "axiom" annotations). You may not alter the code itself.
The program is not intended to be "realistic" and several numeric literals are introduced to simplify the problem (i.e., reduce the number of ESC/Java warning messages).
There are two approaches one could take in solving this problem:
If executed perfectly, the first approach requires a single run of the tool to confirm that the annotations are sufficient. Lacking perfection in anticipating possible errors one would have to iterate the process of running the tool, analyzing the diagnostic error reports, and adding annotations. Furthermore, using the first strategy may result in your adding annotations to your program that, while useful, may not be used by the tool in reasoning about the possibility of runtime exceptions occurring.
The second strategy usually requires multiple iterations. It is possible to iterate 5 times, producing a Java program annotated with 12 invariants and 5 preconditions. Of these, two use quantifiers and several of the invariants enforce the same constraints on different program data.
100 points total. Email your annotated version of academia.java to meghan@cs.wm.edu.
Back to CSci 420/520 Homepage.
Last changed May 21 2008 15:31:40.
David Coppit,
coppit@cs.wm.edu
There have been 1323589 hits since Thu Jun 9 14:49:55 2005
