Home
Syllabus
Assignments
Tests
Describe the two properties (as discussed in class) that a loop invariant must possess in order to be a valid invariant for a loop.
Give an invariant for the following loop that allows us to
argue that, following the loop, all values in the array
nums will be positive.
for(int i = 0; i != nums.length; i++) {
if(nums[i] <= 0) nums[i] = 100;
}
Write an invariant for the following loop that allows us to
conclude that flag indicates whether
n is even upon completing the loop. You need not
justify your answer.
boolean flag = true;
for(int i = 0; i < n; i++) {
flag = !flag;
}
Erathosthenes' Sieve is an ancient algorithm for finding a list of primes. The following is an implementation of his technique in Java.
public static int[] primesUpTo(int n) {
boolean isPrime = new boolean[n + 1];
// Begin by assuming all numbers are prime.
for(int i = 2; i <= n; i++) isPrime[i] = true; // Loop A
// Starting from 2, going up to sqrt(n), eliminate all
// multiples of prime numbers.
for(int i = 2; i * i <= n; i++) { // Loop B
if(isPrime[i]) {
// Aha. We have a prime number. Mark out all its multiples.
for(int j = 2 * i; j <= n; j += i) isPrime[j] = false; // Loop C
}
}
// Finally, we create the array of primes.
// (First, we determine how long the array should be.)
int numPrimes = 0;
for(int i = 2; i <= n; i++) { // Loop D
if(isPrime[i]) numPrimes++;
}
// (And then we create and fill it up with primes.)
int[] ret = new int[numPrimes];
int j = 0;
for(int i = 2; i <= n; i++) { // Loop E
if(isPrime[i]) { ret[j] = i; j++; }
}
return ret;
}
Give an invariant for each of the following loops. You do not need to argue that your invariant is correct.
a. Loop A, leading to the conclusion that all values of
isPrime, beyond index 2, are
true.
b. Loop B, leading to the conclusion that for each number
divisible by a prime up to sqrt(n), but which is
not itself a prime, isPrime at that index will be
false.
c. Loop D, leading to the conclusion that numPrimes
contains the number of entries of isPrime, beyond
index 2, which are true.
d. Loop E, leading to the conclusion that ret
contains all the indices, beyond 2, for which isPrime
contains true.
Consider the following method using insertion sort to sort an array.
public static void sort(double[] nums) {
for(int i = 1; i < nums.length; i++) {
double t = nums[i];
int j = i - 1;
while(j >= 0 && nums[j] > t) {
nums[j + 1] = nums[j];
j--;
}
nums[j + 1] = t;
}
}
What invariant for the outer loop would allow us
to prove that the array nums is sorted
by the end of the method.
Consider the following method using selection sort to sort an array.
public static void sort(double[] nums) {
for(int i = 0; i < nums.length; i++) {
int min = i;
for(int j = i + 1; j < nums.length; j++) {
if(nums[j] < nums[min]) min = j;
}
double t = nums[i];
nums[i] = nums[min];
nums[min] = t;
}
}
What invariant for the outer loop would allow us
to prove that the array nums is sorted
by the end of the method?
Consider the following code to compute the mode
(i.e., the most commonly occurring value) for an array
scores of integers between 0 and 100.
int[] tally = new int[101];
for(int i = 0; i < scores.length; i++) {
tally[scores[i]]++;
}
int mode = 0;
for(int k = 0; k < tally.length; k++) {
if(tally[k] > tally[mode]) mode = k;
}
Identify an invariant for the first for loop (over
i).
Given an array of values, a contiguous subsequence
is a segment of the array including all numbers between the two
endpoints of the segment. The following code is meant to
identify the largest possible sum for any contiguous subsequence
of the array of doubles referenced by nums
(some of which may be negative).
double m = 0;
double n = 0;
for(int i = 0; i != nums.length; i++) {
n += nums[i];
if(n > m) {
m = n;
} else if(n < 0) {
n = 0;
}
}
Identify an invariant for the above loop leading to the conclusion that it finds the largest contiguous subsequence sum.
Define what a data structure invariant is, and give an example based on the LinkedList class.
The invariant must hold at the beginning of the first iteration.
At the beginning of each subsequent iteration, the invariant most continue to hold based on the assumption that it held at the beginning of the previous iteration.
The first i values in the array nums are
positive.
flag indicates whether i is
even.
a. Loop A:
isPrime is true at indices 2 to
i − 1.
b. Loop B:
For all primes p between 2 and
i − 1,
all the numbers with p as a factor
(excepting p itself) have been marked out of
the isPrime array.
c. Loop D:
numPrimes contains the number of true entries
of isPrime within indices 2 to
i − 1.
d. Loop E:
ret contains the indices between 2 and
i − 1
for which isPrime contains
true.
The first i elements of nums are in increasing
order. [Technically, the invariant would also need something
saying essentially that no numbers of the original nums
are destroyed.]
The first i elements of nums contain the
smallest i elements of the original array, in increasing
order.
For each k between 0 and 100,
tally[k] represents the number of
times that k appears in scores between
indices 0 and i − 1.
n is the maximum sum of any subsegment ending at
element i - 1 of the array, and
m is the maximum sum of any subsegment of the first
i values of the array.
A data structure invariant is a condition concerning it that holds true
after each operation on it is completed. For example, in our
LinkedList implementation, each method maintained the invariant
that the number in curSize corresponds to the number of
nodes found in the list referred to by head.
Also, it maintains the invariant that for each node n
(except for the tail node),
n.getNext().getPrevious() refers to n.
[There are several other invariants one could cite based on the
LinkedList class.]