Homework: Applying Esc/Java to quicksort

For this assignment, you will use Escjava to help develop a correct implementation of the quicksort algorithm. Quicksort is based on a simple idea, but it has a lot of subtle corner cases, such as when the chosen pivot element is the maximum element in the array. If you're not careful, one of the resulting partitions can be empty, resulting in infinite recursion.

Just hacking could quickly lead to a nightmare debugging scenario, and even after your tests run correctly, how would you know if your code was really correct?

A better way to proceed is to think carefully about what invariants hold at what points in the program code: what is true on entry to the partition method, for example, and what does partition guarantee when it exists? What is the central loop invariant for that loop inside partition? Carefully documenting these invariants helps produce correct code, and Escjava is a good tool to help verify these invariants.

The key top-level specification that you will need to verify is that:

  • your quicksort does not crash due to, for example, null dereferences or array bounds errors
  • your (in-place) quicksort routine returns a sorted array

Thus, the specification for your sorting routine should be:

 //@ requires a != null;
//@ ensures (\forall int i; 0 <= i && i < a.length-1 ==> a[i] <= a[i+1]);
static void sort(int[] a) {

Escjava has different ways to handle loops. For this assignment, you will use the -LoopSafe switch, which requires loop invariants. For example

//@ loop_invariant 0<=i && i<=a.length;
for(int i=0; i<a.length; i++) {
... a[i] ...

You are to submit:

  • a correct version of quicksort
  • that has a separate partition method
  • that is production-quality code (ie a pleasure for subsequent developers to work on, with helpful comments where necessary. Escjava annotations, as trusted documentation, may reduce the number of comments you need to properly document your code.)
  • with at least four test cases
  • that passes escjava with the -LoopSafe switch (only partial credit will be given if you do not use the -LoopSafe switch)
  • that does not use “assume” statements

Please upload your implementation to Moodle. As usual, you should state whom you worked with on the homework, if appropriate.

Running EscJava

You can either install EscJava on your own computer, following the install instructions (see EscJava), or it is pre-installed on the raindance.cse.ucsc.edu server. For example:

flanaganlt:~ cormac$ ssh raindance
Last login: Wed Oct 17 12:10:26 2007 from raindance.cse.u
Welcome to Darwin!
raindance.cse.ucsc.edu 7> ~cormac/ESC/escj ~cormac/ESC/examples/0.0/Bag.java
Warning: Guessing SIMPLIFY = Simplify-1.5.4.macosx
ESC/Java version ESCJava-2.0b2
/cse/faculty/cormac/ESC/examples/0.0/Bag.java: Caution: Using given file as the .java file, even though it is not the java file for Bag on the classpath
[0.273 s 10561392 bytes]

Bag ...
Prover started:0.061 s 14751128 bytes
[2.639 s 15213504 bytes]

Bag: Bag(int[]) ...
/cse/faculty/cormac/ESC/examples/0.0/Bag.java:6: Warning: Possible null dereference (Null)
n = input.length;

A good source of documentation is the EscJava User's Manual.

Due date: Monday, 16 February 2009, 11:55 PM