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

Purposes of this assignment

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:

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.

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:

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]
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

Turn your assignment in to Blackboard before 6AM Thursday, February 3.