PROGRAM VERIFICATION
Handout #1
Write an iterative program (in Pascal, C, Java, or the like)
to perform a binary search for an element x of data type t
which may or may not appear in an array A[1:n] of type t,
n
> 0. The type t is equipped with a predicate
leq
which totally orders elements of the type and the array A is
ordered in non-decreasing order. That is, we are given that leq(A[i],A[i+1])
for all i = 1,...,n-1. If x does not appear
in
A, set the Boolean variable found to false; if it does,
set
found to true, and pos to the location of any one of
its occurrences. The program may only call the procedure leq
a maximum of log2n+k
times for some constant k.