CSci 435/535: Homework 7

Software Verification

Due Friday, April 1st by 11am

Work alone on this assignment.

Summary

This homework has two parts. First, you will use the Grobo test coverage tool to assess the coverage of a test suite, then enhance the test suite to improve the statement and branch coverage. In the second part, you will use ESC/Java2 to automatically analyze a program for faults.

Be on the lookout for bugs in the code. There are several. As you find each bug, jot down what the bug is, what the fix is, and how you found it (ESC/Java2, test coverage, inspection, etc.) You will turn this report in later.

By the way, you are not allowed to just look up the right implementation of Quicksort to finish this assignment.

Setup

Here is information on getting the files and building the project. You can either work in Eclipse, or just use your favorite text editor. Download and unzip the files for this assignment, which are located here.

Eclipse

1. Start Eclipse. Create a new project and import the files for this homework.
2. Switch to the Java perspective.
3. Open the Ant view by going to Window → Show View →Ant.
4. In the Ant view, click on the icon to add buildfiles. It should look like an ant next to a plus sign. Select build.xml from the HW7 project and hit "Ok." code_coverage should now be listed in the Ant view.
5. Right click on code_coverage in the Ant view and go to "Run Ant..." Select "HW7 build.xml" and hit "Ok." Then go to the "Classpath" tab and click on "Add External JARs." (You may have to click on one of the entries already listed to get the "Add External JARs" button to become active.) Navigate to /usr/local/eclipse/plugins/org.junit_3.8.1/ and add junit.jar.
6. Click "Apply" and then "Run" to run the buildfile. This will build the code, run the tests, generate the coverage report, and run ESC/Java2. You may need to refresh the project to see all the new directories and files that were created.

Text Editor

1. You can just run ant in the <HW7 FILES DIR> that was created when you unpacked the hw7-files.zip file. You can run ant test or ant escj separately for the different parts of this homework.

Automated Verification

ESC/Java2 is a program verifier that attempts to find common run-time errors in Java programs by static analysis of the program text. Users can control the amount and kinds of checking that ESC/Java2 performs by annotating their program with specially formatted comments called pragmas. The goal of ESC/Java2 is not to provide formally rigorous program verification. Rather, it is to help programmers find some kinds of errors more quickly than they might be found by other methods, such as testing or code reviews. Like testing, it is neither sound nor complete, but it is easier to do.

Overview

ESC/Java2 pragmas must occur within pragma-containing comments. Pragma comments look like

//@ <PRAGMA_NAME> expression

/*@ <PRAGMA_NAME expression */

More information can be found in this summary. The user's manual is here. (You should read Chapter 0.) There are also more resources on the class homepage. Below are some example pragmas.

Assert

An assert pragma is a statement pragma. The pragma causes ESC/Java2 to issue a warning if it cannot establish that the expression is true whenever control reaches the pragma.

/*@ assert x < 10 && y < 10 */
int a[10]
a[x][y] = 0

Requires

A requires pragma is a routine modifier pragma. The pragma makes the expression a precondition of the routine the pragma modifies. When checking the body of the routine, ESC/Java2 assumes that that precondition holds initially. When checking a call to the routine, ESC/Java2 issues a warning if it cannot establish that the expression holds at the call site.

/*@ requires v!= null */
public void doSomething(Vector v) {
  ...
}

Non-null

A non_null pragma is a modifier pragma. It may modify the declaration of a variable of a reference type. The variable may be a static field, instance variable, local variable, or parameter. The pragma causes ESC/Java2 to check, at each assignment to the variable, that the value assigned is not null, and to assume at each use (except in one case, described below) that the value is not null. When a formal parameter declaration is annotated with a non_null pragma, ESC/Java2 checks at each call site that the corresponding actual is not null.

/*@ non_null */ char[] c;

public void doSomething(/*@ non_null */ Vector v) {
  ...
}

Invariant

An invariant pragma is a declaration pragma. The pragma declares the expression to be an object invariant of the class within whose declaration the pragma occurs.

int len;
//@ invariant 0 <= len && len <= a.length;

Assignment

1. Open a shell, and change to the directory that contains your project from the first part of this assignment.
2. Check Quicksort.java with ESC/Java2 by running the command ant escj You should get a number of warnings.
3. Add pragmas to Quicksort.java to eliminate the warnings. By doing this, you are giving ESC/Java2 more information so that it can do a better analysis of your code.
4. If you have problems resolving a pragma, keep in mind that the problem might be with the code. If you find a bug, log it and fix it.

Test Coverage

Test coverage is a proxy measurement for test quality. (It is assumed that high coverage corresponds to good quality, but this is not always the case, nor is it sufficient.) The code we provide has a small number of JUnit test cases that do not give complete code coverage. You will need to augment the test cases to give as much coverage as possible. The code contains an Ant build file that will run Grobo for you.

1. Open <HW7 FILES DIR>/code_coverage/coverage/complete/index.html in your favorite web browser to see your code coverage report. There are also reports for the individual classes that show the code that was not covered by the test cases under <HW7 FILES DIR>/code_coverage/coverage/complete/<NAME_OF_FILE_TESTED>.html.
2. As you can see, the current test cases give less than 10% coverage for all the types. Add additional test cases to achieve as much statement coverage as possible. You can run ant test to regenerate the coverage report.
3. At this point you may notice that the branch coverage is not as high as it could be. Add additional test cases as necessary to improve the branch coverage as much as possible.
4. There are several bugs in the code. If your test cases and automated verification did not already find them, find them now and fix them.

Submission

Email three files, the updated Quicksort.java and QuicksortTest.java, and the bug log, to csci435@coppit.org.

Grading

150 points total

If you have any questions, feel free to ask them in the discussion forum.