Problem Description

proving program correctness

Consider the following program specification:

Input: An integer n > 0 and an array A[0..(n - 1)] of n integers.

Output: The smallest index s such that A[s] is the largest value in A[0..(n - 1)].

For example, if n = 9 and A = [ 4, 8, 1, 3, 8, 5, 4, 7, 2 ] (so A[0] = 4, A[1] = 8, etc.), then the program would return 1, since the largest value in A is 8 and the smallest index at which 8 appears is index 1.

Consider the following implementation:

		indexOfMax(n, A)
(1)		i n - 2
(2)		m A[n - 1]
(3)		s n - 1
(4)		while i 0
(5)			if A[i] m then
(6)				m A[i]
(7)				s i
(8)			end
(9)			i i - 1
(10)		end
(11)		return s

In the implementation above, line numbers are given so you can refer to specific lines in your answers and is used to indicate assignment.

Part A

Use induction to establish the following loop invariant right before the while test in line (4) is executed:

i. -1 i < n - 1

ii. m = A[s]

iii. m = max A[(i + 1) .. (n - 1)] (i.e., m is the maximum value in that appears in the array A between indices i + 1 and n - 1, inclusive)

iv. s is the smallest index at which max A[(i + 1) .. (n - 1)] appears

Hints and tips:

Use only one induction proof and prove each of the four parts of the invariant in your base case and inductive step.

You may assume that i and s will always be integers (i.e., you don't have to prove this).

Part B

Prove the correctness of the implementation by arguing partial correctness and termination.