course-web-page-fall-2022

Course web page for Data Structures H343 Fall 2022

View the Project on GitHub IUDataStructuresCourse/course-web-page-fall-2022

Lecture: Arrays, Rotation, and Correctness Proofs

Arrays in Java

Create an array of length n

int n = 10;
int[] A = new int[n];

Set the element at a given position:

A[0] = 0;
A[1] = 1;
A[2] = 4;

for (int i = 3; i != n; ++i)
  A[i] = i * i;

Now we have an array that looks like the following

elements: 0, 1, 4, 9, 16, 25, 36, 49, 64, 81
position: 0, 1, 2, 3,  4,  5,  6,  7,  8,  9

Get the element at a given position:

assert A[2] == 4;

Loop over all the elements of an array, front to back

int total = 0;
for (int y : A) {
  total += y;
}
System.out.println(total);

Def. a half-open interval, written [i,k), is a contiguous subarray that starts at position i and finishes one place before k.

The interval [3, 7) of our example array is

elements: 9, 16, 25, 36
position: 3,  4,  5,  6

Loop over a half-open interval of the subarray:

static int sum(int[] A, int begin, int end) {
  int total = 0;
  for (int i = begin; i != end; ++i) {
      total += A[i];
  }
  return total;
}

assert total == sum(A, 0, 5) + sum(A, 5, 10);

Rotate the elements of an array by 1 to the right, with wrap around.

    [1,2,3,4,5]
--> [5,1,2,3,4]

Rotation is used in

Correctness

We’ll focus on the swap-backwards algorithm, expressed below as a while loop.

static void rotate_1_swap_bkwd(int[] A) {
	if (A.length > 1) {
		int i = A.length - 1;
		while (i != 0) {
			swap(A, i, i-1);
			--i;
		}
	} else {
		// Nothing to do here
	}
}

We’re going to prove that this algorithm is correct and document the proof by adding comments and assert statements to the code.

What does it mean exactly for an array to be rotated by 1 to the right The following is_rotated function makes this idea precise. If the array has zero or one element, then rotating it does not change the array. Otherwise, the last element becomes the first element and all the other elements are moved by one to the right.

static boolean is_rotated(int[] A_orig, int[] A_new) {
	if (A_orig.length < 2) {
        return Arrays.equals(A_orig, A_new);
	} else {
		boolean result = A_new[0] == A_orig[A_orig.length - 1];
		for (int i = 0; i != A_orig.length - 1; ++i) {
			result &= A_orig[i] == A_new[i + 1];
		}
		return result;
	}
}

Most of the work of the algorithm is in a while loop, which means we need to come up with a loop invariant to prove that it is correct. A loop invariant is a statement about the current state of affairs that it true at the beginning of each loop iteration.

The tricky thing about a loop invariant is that the state of affairs is changing, so it must be abstract enough to capture some property that stays the same.

Let’s watch the algorithm in action to see if we can see some patterns from which we can create the loop invariant. The while loop is controled by variable i, so let’s draw a vertical line just before the element at the index i. The loop invariant will need to relate the current state of the array to it’s original state, so we’ll write down both at each iteration of the loop:

A_orig: 1 2 3 4 | 5
A:      1 2 3 4 | 5

A_orig: 1 2 3 | 4 5
A:      1 2 3 | 5 4

A_orig: 1 2 | 3 4 5
A:      1 2 | 5 3 4

A_orig: 1 | 2 3 4 5
A:      1 | 5 2 3 4

A_orig: | 1 2 3 4 5
A_:     | 5 1 2 3 4

Looking at the above, let’s focus on the front part of the array, the elements before the line. There’s an easy pattern: the elements in the front part of A are the same as those in the front part of A_orig.

What about the back part, i.e. the elements after the line? The back part of A is the rotated version of the back part of A_orig!

We write down the loop invariant as another function:

static boolean loop_invariant_rotate_bkwd(int[] A_orig, int[] A, int i) {
    return is_rotated(copyOfRange(A_orig, i, A.length), 
                      copyOfRange(A, i, A.length))
        && Arrays.equals(copyOfRange(A_orig, 0, i), 
                         copyOfRange(A, 0, i));
}

Now that we’ve identified a loop invariant, we need to check that it really is an appropriate loop invariant for this algorithm.

  1. show that the loop invariant is true before the start of the loop
  2. show that the loop invariant is true at the end of the loop body, assuming that it started out true at the beginning of the loop. (For a hypothetical iteration of the loop.)
  3. show that the loop invariant combined with the loop condition being false logically implies the correctness criteria for the algorithm.

Student Exercise

write down arguments for 1, 2, and 3.

Rotate with annotations

static void rotate_1_swap_bkwd_short_proof(int[] A) {
	int[] A_orig = copyOf(A, A.length);
	assert Arrays.equals(A_orig, A);
	if (A.length > 1) {
		int i = A.length - 1;
		// The subarrays [A.length-1, A.length) of A_orig and A have length 1,
		//     and are equal, so they satisfy first branch of is_rotated.
		// The subarrays [0, A.length-1) of A_orig and A are equal.
		assert loop_invariant_rotate_bkwd(A_orig, A, i);
		while (i != 0) {
			assert loop_invariant_rotate_bkwd(A_orig, A, i);
			// A_orig: ... V W | X Y Z
			// A:      ... V W | Z X Y
			//                   i
			swap(A, i, i-1);
			// A_orig: ... V W | X Y Z
			// A:      ... V Z | W X Y
			assert loop_invariant_rotate_bkwd(A_orig, A, i - 1);
			--i;
			// A_orig: ... V | W X Y Z
			// A:      ... V | Z W X Y
		}
		assert loop_invariant_rotate_bkwd(A_orig, A, i) && i == 0;
		// The subarrays [0, A.length) of A and A_orig are rotated, and
		// they are equal to the entire arrays.
		assert is_rotated(A_orig, A);
	} else {
		// Nothing to do here
		assert is_rotated(A_orig, A);
	}
	assert is_rotated(A_orig, A);
}