CIS575-Assignment 1 Solved

Description

We want to write an algorithm that expects an array A[1..n] and a number x, and returns a number q, and that implements the specification precondition the array A[1..n] is non-decreasing, and we know that x occurs in A[1..n] postcondition q ∈ 1..n and A[q] = x.

1          2          3          4          5          6

12

15

17

17

26

30

For example, if A[1..6] is given bythen

• if x = 26 then q = 5 must be returned
• if x = 17 then either q = 3 or q = 4 must be returned (the specification is non-deterministic)
• if x = 10 then (as the precondition is not fulfilled) the algorithm could behave in any way; it may return 1, never terminate, or crash…

To implement this specification we shall use the binary search principle, and develop an iterative algorithm of the form

Find(x,A,n) P q ← (lo + hi) div 2 while A[q] 6= x

if A[q] < x

T

else

E q ← (lo + hi) div 2

return q

which uses variables lo, hi, and q, and where the loop invariant Φ has various parts:

• A is non-decreasing
• 1 ≤ lo ≤ hi ≤ n
• lo ≤ q ≤ hi
• x occurs in A[.hi]

In this exercise, we shall develop P so as to complete the preamble, and develop T and E so as to complete the loop body.

1. Specification Translate the precondition into a formula in predicate logic (which must contain quantifiers, universal ∀ and/or existential ∃).
2. Preamble We shall find a suitable P.
   1. Give an example that shows that letting P be lo ← 1; hi ← n − 1 may not establish Φ.
   2. Now define P (as a sequence of assignments) so that Φ will always be established (you don’t need to argue for that).
3. Loop body We shall find suitable T and E.
   1. First consider the case where T is given by hi ← q and E is given by lo ← q.

It is quite obvious that this choice will maintain parts (0)–(2) of Φ. But give an example that shows that this may not maintain part (3) of Φ.

2. Next consider the case where T is given by lo ← q and E is given by hi ← q.
   • Argue that this choice will maintain part (3) of Φ.
   • Give an example that shows that with this choice, the loop may not
3. Write T and E such that Φ is maintained and termination is ensured (you do not need to argue for these properties).

4. Recursion (Translate your completed iterative algorithm into a recursive algorithm that is equivalent, in that it always examines the same array elements.

Specifically, you must write a function Find that calls itself (but contains no while loop) and which as argument takes at least lo and hi, and perhaps also q, but you may omit the “global” A and x.

Remember also to state how to call Find at “top-level” so as to implement the specification.