CSci 420/520: Homework 9

Java PathFinder

Due Friday, November 11th by 1pm.

Summary

Java PathFinder is a model checking tool for source code, developed by the formal methods group at NASA. You will use JPF to find a fault in two simple Java programs, Quicksort and MergeSort.

Make sure you have JPF running as described in the tools setup document.

Assignment

In this assignment, you are given a piece of Java code. Download the Quicksort.java into your work directory. After you compiled the code, execute it using

java -ea Quicksort

to check that the code actually implements the quicksort algorithm correctly. You can modify the code to change the different array values if you wish to test the code.

Now, how sure are we that this quicksort algorithm performs under all circumstances? Now comment out Part I and uncomment Part II and recompile. Now run the following command.

jpf Quicksort

You will get a (long) error message. This assignment asks you to do the following:

1. Using the messages output by JPF as a guide, find out where the problem lies. You may use other methods to determine the error if you wish. For example, if you want to know what the state of the variables are for the error path that JPF generates, you should print them out.
2. Briefly explain in English what the problem is, how to solve it, and why the Part I appears to work perfectly. This portion the bulk of the grades for this assignment.
3. Implement your solution in the code. Running JPF will result in no error messages.

Now download the MergeSortArray.java into your work directory. Follow the instructions above and do the same thing for this code.

Important: Do NOT rewrite the quicksort or mergesort algorithm. The purpose of this assignment is not to test your ability to code a sorting algorithm. It is show how using a tool like JPF can help to catch potential problems in your code. You solution should follow your analysis of what the problem is, how to fix it, and why the fix makes sense. A java implementation that clears JPF but lacks a good explanation will not receive full credit.

Grading

Turn in your version of Quicksort.java, MergeSortArray.java and writeup. Please indicate clearly in your writeup the answers for Quicksort and MergeSortArray. Write your name on everything you turn in.

100 points total. 70% for the writeup, 30% for the correct java implementation.

Email Quicksort.java, MergeSortArray.java and the writeup to meghan@cs.wm.edu.