Cmpt 340-t1 - using our rules for hoare logic show the

Question

Part -1:

Using our rules for Hoare logic, prove the correctness of the following program that computes the integer n^th power of integer x. Although you might want to figure out the proof using tree layout, give your solution in linear form similar to the proofs of division given in the textbook.

We give the initial assumption

{n ≥ 0}

and final goal

{ y = xⁿ }

in the program below:

// Slow Exponentiation

{ n ≥ 0 }
y := 1
k := n

while (k > 0) do

y := y ×

k := k - 1

done
{ y = xⁿ }

{y = xⁿ }

Bonus points Why is this called slow exponentiation? To get one bonus point, give code that is exponentially faster in n, and to get the second bonus point, argue convincingly that your speedup is exponential.

Part -2:

Using our rules for Hoare logic, show the correctness of the following program that computes the index of the largest element in an array of integers, A; again present your proof in linear form. Assume that arrays are indexed from 1 to n and n > 0, as in the first tutorial.

// Find Maximum
{ length(A) = n ∧ n > 0 }

maxI .= 1

for j from 2 upto n do

if A [j ]>A [maxI ]

then maxI .= j

else skip

done

{ ∀j ∈[1,n] A[maxI] ≥ A[j] }

Programming Part - 1

P1 Alice believes that the following Java function correctly copies a range of elements in an array to a new location (overwriting what is there).

static void rangeCopy (int A [],
int from , int endWith , int to ) {
for (; from <=endWith ; from +=1, to +=1) {
A [to ] = A [from ];
}
}
So, if
A = [ 0, 1, 2, 3, 4]
initially, then rangeCopy (A, 0, 1, 3) would change A to become
A = [ 0, 1, 2, 0, 1]
This is useful in many places: from copying ranges of cells in Excel to the memcpy(1) system-library function.

Although the function works for the above example, there are a number of situations where it will do the wrong thing. Identify as many distinct ones of these that you can, explaining the problem and giving a counter-example where the function does the wrong thing. One important case will require you to reason about some kind of separation property. Finally, give a correct Java function, embedded in a class that tests for the various problematic cases you've identified.