Back to the CSci 435/535 Homepage.
Work alone on this assignment.
In this homework you will use specifications written in JML to test and fix a simple bubble sort algorithm. In the first part you will use JML to specify the sort routine. In the second part you will use ESC/Java2 to check the code for errors against the specification. In the third part you will use the jmlc, jmlunit, and jmlrac tools to create a test harness and self-checking version of the sort routine. This will allow you to manually specify some test cases and find bugs in your specification or the code. Finally, you will use the yagg tool to exhaustively generate a large number test inputs for a more thorough verification of the code.
Download and unzip the files for this assignment, which are located at here. Start a command shell and an editor for the file called "report.txt".
When you look at the files in the distribution, you will see:
Open BuggleSort.java and add JML specifications for the informal specification given for buggleSort(). I have provided a pure method called isPermutation() that you can use in your JML specification.
ESC/Java2 is a static checker that uses a theorem prover to check Java code
against common errors and JML specifications. Run make
escj to run escj on the code. You will find a code bug and
perhaps some bugs in your specification.
Once you fix the errors that escj finds, you will still have a warning. In your report, explain what the warning is saying, and why you think that ESC/Java2 is issuing the warning. Don't worry about trying to remove the warning.
The JML toolset includes a number of useful programs. One is jmlc, which can compile your program, converting any JML specifications into run-time assertions that are checked when the program is run. jmlrac can run the resulting binary, checking the JML assertions as the program is run. jmlc and jmlrac are the JML equivalents of javac and java. Another useful tool is jmlunit, which can automatically create a test harness from your program.
Run make BuggleSort_JML_TestData.java. This
will run jmlunit to create a test harness. Next edit the file
BuggleSort_JML_TestData.java. Where it says "replace this comment"
insert some arrays with doubles like { 0, 2, 1 }. Each will be used
by the test harness to test the code.
Run make test. This will run jmlc to
build your code with JML run-time checks, then run javac to compile
the test harness, then run jmlrac to run the test harness.
Depending on your selection of test inputs, you may find that
jmlrac reports an error. If it does, diagnose and fix the bug that
causes the problem. (There are two bugs. You can fix them now or in the next
part.) There are some commented out debugging statements that you can use to
help find the problem. After modifying the sort code or the test data code
just run make test to automatically recompile and
retest the program.
In your report, explain what the two warnings about requires clauses mean.
yagg is a test input generator. It works by taking a user-specified specification of the structure of the input and generating a generator that enumerates all possible strings that meet the input specification. The input specification is designed to be similar to that of yacc, a parser generator.
Edit the file list.yg. This file is the input to yagg. It contains a grammar that defines the structure of lists of numbers that it generates. The first rule states that a number_list is either an empty string or a nonempty_number_list. The next rule says that a non-empty number list is either a number or a nonempty_number_list followed by a number. Finally, the last rule says that a number can be "1" or "2".
Using this grammar, one can start with the number_list nonterminal and replace/expand it with one of two alternatives. By continuing this expansion one can create an infinite number of lists of numbers. Of course one needs to be careful not to get in an infinite loop. yagg addresses this by creating a generator that takes as an argument a length for the string to be generated.
Run make datagenerator/progs/generate. This
will run yagg to generate and compile the test input generator. When
it is done, run datagenerator/progs/generate 3 to
generate all strings of 3 numbers. You will notice that some sequences like "1
2 3" are missing. This is due to a bug in the input grammar. Fix it by
modifying the list.yg file. Remake the data generator and rerun it to
check that you make the right change.
Run make testdata. This will run the generator
for lists of lengths 0, 1, 2, and 3, saving the lists into the file
testdata. Now run make exhaustivetest to
run a modified version of the test harness that takes its number arrays from
the testdata file. You should not see any failures. If you do, fix
either your specification or your code using the debugging techniques
described in the previous part of the assignment.
Explain in your report how this approach to testing, called "bounded exhaustive testing" is similar to the model checking approach taken by the Alloy Constraint Analyzer.
Run make dist. Email the resulting .tar.gz
file to coppit@cs.wm.edu.
150 points total
Back to the CSci 435/535 Homepage.
Last changed April 05 2007 16:27:42.
David Coppit,
coppit@cs.wm.edu
There have been 1232689 hits since Thu Jun 9 14:49:55 2005
