Lecture Notes on Binary Search 15 122 Principles of Imperative Computation Frank Pfenning Lecture 3 August 31 2010 1 Introduction One of the fundamental and recurring problems in computer science is to find elements in collections such as elements in sets An important algorithm for this problem is binary search We use binary search for an integer in a sorted array to exemplify it Binary search is the first time we see the fundamental principle of divideand conquer We will see many other examples of this important principle in future lectures It refers to the idea of subdividing a given problem into smaller components each of which can be solved separately We then combine the results to obtain a solution to the original problem We will also once again see the importance of loop invariants in writing correct code Here is a note by Jon Bentley about binary search I ve assigned binary search in courses at Bell Labs and IBM Professional programmers had a couple of hours to convert its description into a program in the language of their choice a high level pseudocode was fine At the end of the specified time almost all the programmers reported that they had correct code for the task We would then take thirty minutes to examine their code which the programmers did with test cases In several classes and with over a hundred programmers the results varied little ninety percent of the programmers found bugs in their programs and I wasn t always convinced of the correctness of the code in which no bugs were found I was amazed given ample time only about ten percent of professional programmers were able to get this small program right But L ECTURE N OTES A UGUST 31 2010 Binary Search L3 2 they aren t the only ones to find this task difficult in the history in Section 6 2 1 of his Sorting and Searching Knuth points out that while the first binary search was published in 1946 the first published binary search without bugs did not appear until 1962 Jon Bentley Programming Pearls 1st edition pp 35 36 I contend that what these programmers are missing is the understanding of how to use loop invariants in composing their programs They help us to make assumptions explicit and clarify the reasons why a particular program is correct Part of the magic of pre and post conditions as well as loop invariants and assertions is that they localize reasoning Rather than having to look at the whole program or the whole function we can focus on individual statements tracking properties via the loop invariants and assertions Before we introduce binary search we discuss linear search 2 Linear Search in an Unsorted Array If we are given an array of integers A without any further information and have to decide if an element x is in A we just have to search through it element by element We return true as soon as we find an element that equals x If we have gone through the whole array and still not found such an element we return false bool is in int x int A int n requires 0 n n length A int i for i 0 i n i loop invariant 0 i i n if A i x return true return false Could we strengthen the loop invariant or write a postcondition For the loop invariant we might want to express that x is not in A 0 A i 1 We would have to express this with something like loop invariant is in x A i where b is the negation of b However it is difficult to make sense of this because it uses is in which is the very function we are defining L ECTURE N OTES A UGUST 31 2010 Binary Search L3 3 This is small illustration of the general observation that some functions are basic specifications and are themselves not subject to further specification Because such basic specifications are generally very inefficient they are mostly used in other specifications that is pre or post conditions loop invariants general assertions rather than in code intended to be executed 3 Sorted Arrays A number of algorithms on arrays would like to assume that they are sorted We begin with a specification of this property The function is sorted A n traverses the array A from left to right checking that each element is smaller or equal to its right neighbor We need to be careful about the loop invariant to guarantee that there will be no attempt to access a memory element out of bounds bool is sorted int A int n requires 0 n n length A int i for i 0 i n 1 i loop invariant n 0 0 i i n 1 if A i A i 1 return false return true The loop invariant here is a disjunction either n 0 or i is between 0 and n 1 This is a simple or on boolean values true and false and not an exclusive or even though we will often pronounce it as either or Why is it necessary If we ask if a zero length array is sorted then before the check the exit condition of the loop the first time we have i 0 and n 0 so it is not the case that i n 1 Therefore the second part of the loop invariant does not hold We account for that explicitly by allowing n to be 0 For an example of reasoning with loop invariants we verify in some detail why this is valid loop invariant Loop Entry Upon loop entry i 0 We distinguish two cases If n 0 then the left disjunction n 0 holds If n 6 0 then n 0 because the precondition of the function requires n 0 But if n 0 and i 0 then i n 1 We also have 0 i so 0 i i n 1 holds L ECTURE N OTES A UGUST 31 2010 Binary Search L3 4 Loop Traversal Assume the loop invariant holds before the test so either n 0 or 0 i n 1 Because we do not exit the loop we also have i n 1 The step statement in the loop increments i so we have i0 i 1 Since i0 i 1 and 0 i we have 0 i0 Also since i n 1 and i0 i 1 we have i0 1 n 1 and so i0 n Therefore i n 1 So 0 i0 n 1 and the loop invariant is still satisfied because the right disjunct is true for the new value i0 of i One pedantic point and we do want to be pedantic in this class when assessing function correctness just like the machine is from 0 i and i0 i 1 we inferred 0 i0 This is only justified in modular arithmetic if we know that i 1 does not overflow Fortunately we also know i n 1 so i n and i is bounded from above by a positive integer Therefore incrementing i cannot overflow We …