Homework 1

Homework 1
Document last modified:

Text 2.1-3.

From text:

Consider the searching problem:

Input: A sequence of n numbers A=<a₁,a₂,...,a_n> and a value v.

Output: An index i such that v=A[i] or the special value NIL if v does not appear in A.

The following linear search, scans through the sequence, looking for v. Using a loop invariant, prove that the algorithm is correct. Make sure your loop invariant fulfills the three necessary properties.

The algorithm below uses the following simplifying precondition: v is in A or in logic notation:

∃i where 0 ≤ i < A.length, A[i] == v

class LinearSearch {

//@ pre A != null;
//@ pre (\exists int i; 0 <= i && i < A.length; A[i] == v);
//@ post A[\result]==v;

int linearsearch(int A[], int v) {

int i = 0;

         //@ loop_invariant (\forall int j; 0<=j && j < i; A[j] != v);
         while(A[i] != v)
              i = i + 1;
         return i;
    }
}

Consider the loop condition and the loop invariant. The loop condition is:

A[i] != v

The loop invariant must state that is true before, during and after the loop execution. To be useful, the loop invariant must also produce the desired result, in this case, determining the indices of i where A[i] != v.

The loop invariant must then define the elements of array A that v is not equal to, similar to the loop condition. The key insight is that A[i]!=v for all indices less than i.

a. State the loop invariant in English using the terms from the text of the three properties: initialization, maintenance and termination. This is not a formal proof but should provide sufficient details to convince the reader of its validity.

Initialization: The invariant property must hold in the state just before the first test of the while condition.

Maintenance: The invariant property must hold in the state at the very end of the sequence of statements in the loop body.

Termination: When the loop terminates, the invariant gives a useful property that helps show the algorithm is correct.

b. Prove using induction the correctness of the loop invariant.

The loop invariant is:

∀j: 1 ≤ j < i, a_j ≠ v

-- Precondition: ∃a₁^∃i: 1 ≤ i ≤ n, a_i = v
procedure P_n( v, a₁, a₂, a₃, ..., a_n : integers)

i ← 1

{ invariant ∀j: 1 ≤ j < i, a_j ≠ v }

while a_i ≠ v

i ← i + 1

-- Postcondition: a_i = v

Show ∀j: 1 ≤ j < i, a_j ≠ v is always true

1. Base Step:

before the loop,

Hint:
   Vacuous proof, see example.

2. Inductive Step: P_k → P_k+1

at the end of each loop execution,



Hint:
   Show P_k+1

   Assume invariant, P_k, true when loop executes.

3. and after the loop completes

c. Copy the above Java code and validate using ESCjava.

Complete the Java program to add values at corresponding indices of two int arrays; A[0]+B[0], A[1]+B[1], .... You'll need to state preconditions and loop-invariant. Reasonable preconditions are that A and B are the same length. Validate using ESCjava.

class Add {
//@ post (\forall int i; 0 <= i && i < A.length; \result[i] == A[i]+B[i]);

int[] add( int A[], int B[] ) {

Hint and warning

Generally, aliases of parameters should be avoided because allow side-effects.

ESCJava complains about parameter aliases used to return a result as "Post-conditions may not be established".

For example, the following aliases parameter A as the result, eliciting ESCJava complains about establishing the post-condition.

public class Times2 {

//@ pre A != null;
//@ post(\forall int i; 0 <= i && i < A.length; \result[i] == 2*A[i]);

   public static int[] times2(int A[]) {
        int i = 0;

        //@ loop_invariant (\forall int j; 0<=j && j < i; A[j] == 2*\old(A[j]));
       while(i < A.length){
           A[i] = 2*A[i];
           i++;
       }
       return A;
   }
}

The following results in A == B == C == { 4, 8, 12 } because A, B and C reference the same array object.

int [] A = {1, 2, 3};
int [] B = Times2.times2( A );
int [] C = Times2.times2( B );

While the following establishes the post-condition:

public class Times2 {

//@ pre A != null;
//@ post(\forall int i; 0 <= i && i < A.length; \result[i] == 2*A[i]);

   public static int[] times2(int A[]) {
        int i = 0;
        int R[] = new int[ A.length ];

        //@ loop_invariant (\forall int j; 0<=j && j < i; R[j] == 2*A[j] );
       while(i < A.length){
           R[i] = 2*A[i];
           i++;
       }
       return R;
   }
}

Text 2.2-2.

From text:

Consider sorting n number stored in array A by first finding the smallest element of A and exchanging it with the element in A[1]. Then find the second smallest element of A and exchange it with A[2]. Continue in this manner for the first n-1 elements of A. Write pseudocode for this algorithm, which is known as the selection sort. What loop invariant does the algorithm maintain? Why does it need to run for only the first n-1 elements, rather than for all n elements? Give the best-case and worst-case running times of selection sort in Θ-notation. Justify your answers.

Define a Java algorithm that returns a reference to the sorted array.
Validate using ESCjava. Give preconditions, postconditions and loop invariants for each of the two loops.

Test using the following or similar.

Use two separate Java files, one named SelectionSortEx.java with the following, the second SelectionSort.java with your solution.

public class SelectionSortEx {

public static void main(String a[]) {
    double A[]={2,4,5,7,1,2,3,6};
    double B[]=(new SelectionSort()).selectionSort(A);
    for(int i=0;i<B.length;i++) System.out.println(B[i]);
}
}

Give a reasonable best and worst case running times in Θ-notation. Justify your answers.

Turn in

Cover sheet with your name, C455, date, and Homework 1,
Typed answer to Question 1a, 1b and 3d,
Print out of Add.java and SelectionSort.java,
Print out of validation results for LinearSearch, Add and SelectionSort using ESCjava,
Execution results of Question 3c.