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.

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:

Usual notation Meaning Suggested notation Example
∧, & and `& `or` AND` `i > 0 & i < n`
∨, | or `| `or` OR` `i < 0 | i > 100`
¬, ! not `NOT` `NOT i < 0`
implies `IMPLIES `or` IF...THEN`
(`=> `looks too much like` <=`)
`i < j IMPLIES a[i] <= a[j]`
`IF i < j THEN a[i] <= a[j]`
for every, for all `ALL` `ALL x, x2 >= 0`
there exists `EXISTS` `EXISTS x, x2 == 100`

 Firefox and Opera mess up the spacing below, and in the last half of the above table; I don't know why. Internet Explorer doesn't mess up the spacing, but also doesn't do syntax coloring on the insertionSort code below. Only Chrome gets everything right.

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]
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 `∃`.