CIT 594 Assignment 3 : “Newsort”
Spring 2011, David Matuszek

Purposes of this assignment

• Familiarize you with the notions of precondition, postcondition, and loop invariant
• Give you some practice with determining Big-O
• Give you some practice with proving programs correct

The programming part of this assignment should be pretty simple--you've already done 90% of the work in your first assignment. The emphasis here is on theory. (Don't worry, this won't happen often!)

General idea of the assignment

People have invented a lot of sorting algorithms, so for this assignment I thought I'd do the same. I'll describe the algorithm informally; your job is to:

• JUnit test the algorithm.
• Implement the algorithm.
• Figure out and write down (in comments) the pre- and post-conditions, and the loop invariant, for every loop in the algorithm.
• Determine the Big-O time of the algorithm, and explain your reasoning (in a readme.txt file).
• Run some timing tests on the algorithm (include them in the readme.txt file) and comment on how well they agree with your Big-O determination.
• "Prove" (in readme.txt) that your program is correct (if it is!). This has two parts:
  • Prove that when your program terminates, the array is sorted.
  • Prove that your program terminates.
• If you can find some simple optimizations to perform, do them, test them, and describe them in the readme.txt file.

By the way, I'm sure other people have also invented this algorithm, and it probably has a name. I don't know (or care about) that. I'm calling it “newsort.”

The algorithm

1. Set a variable step to one less than the array size.
2. For every location i in the array, make it true that, if i + step is also in the array, then array[i] ≤ array[i + step]. (Hint: This is an informal statement of a loop invariant.)
3. Set step to step - 1.
4. If step > 0, go back to step 2; otherwise stop.

What to do

Testing, implementing, and timing the algorithm

You know how to do this. Remember TDD: Test-Driven Design. Since you've already done the first assignment, it should be pretty easy to start with the JUnit tests.

Determining the Big-O running time of the algorithm

This is mostly a matter of figuring out how many times the code in the innermost loop gets executed. You can be pretty informal.

Writing pre- and post-conditions and invariants for each loop

A precondition is just what needs to be true, in order for the loop (or other code) to do its job correctly.

A loop invariant is a statement of some fact that is true, whenever that point in the loop in reached. It is almost always placed right at the beginning of the loop, so that it is true initially, and is true again whenever that point in the loop is reached. (For another explanation, see http://en.wikipedia.org/wiki/Loop_invariant.)

A postcondition is what is true when the loop is finished. It is a consequence of two facts: the loop invariant, and whatever caused the loop to terminate.

• A while loop terminates when its condition becomes false. Thus, ((NOT precondition) AND loop invariant) IMPLIES postcondition.
• A for loop terminates when its loop index (typically i) has gone through all its values. Thus, ((loop index out of range) AND loop invariant) IMPLIES postcondition.

Some comments on notation

Since I'm asking you to write these logical statements in comments in your program, that limits the characters you can use. Here's what I recommend:

A statement using the ∀ operator usually looks something like this:
     ∀ (some variable/s), (some restriction on the variable/s) ⇒ (some conclusion)
For example,
     ∀ x,y ≤ i, x < y ⇒ array[x] ≤ array[y]
can be read as
     For all x and y less than or equal to i, if x is less than y, then array[x] is less than or equal to array[y].

The same comments apply to using the ∃ operator.

Example: Insertion sort

public static void insertionSort(int[] array) {
    // Pre: TRUE (nothing really needs to be said here)
    for (int i = 1; i < array.length; i++) {
        // Inv: ALL x,y <= i, x < y IMPLIES array[x] <= array[y]
        int toIndex = findInsertionPoint(array[i], array, 0, i);
        insert(i, toIndex, array);
    }
    // FROM  i == array.length AND Inv   CONCLUDE:
    //     (ALL x,y < array.length, x < y IMPLIES array[x] <= array[y])
    // (which is basically the definition of "sorted")
}
    

Note: It would be nice to put our logical statements in Java's assert statements, rather than in comments. Unfortunately, the Java language only has simple Boolean operators &&, ||, !; it doesn't have anything resembling ∀ or ∃.

Grading

This assignment still requires programming, so all the requirements in Assignment 1 still apply.

Due date