DOC PREVIEW
CMU CS 15122 - Lecture Notes on Binary Search

This preview shows page 1-2-3-4-5 out of 16 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 16 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 16 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 16 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 16 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 16 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 16 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

IntroductionLinear Search in an Unsorted ArraySorted ArraysLinear Search in a Sorted ArrayAnalyzing the Number of OperationsBinary SearchImplementing Binary SearchOne More BugSome MeasurementsLecture Notes onBinary Search15-122: Principles of Imperative ComputationFrank PfenningLecture 3August 31, 20101 IntroductionOne of the fundamental and recurring problems in computer science is tofind elements in collections, such as elements in sets. An important algo-rithm for this problem is binary search. We use binary search for an integerin a sorted array to exemplify it.Binary search is the first time we see the fundamental principle of divide-and-conquer. We will see many other examples of this important principlein future lectures. It refers to the idea of subdividing a given problem intosmaller components, each of which can be solved separately. We then com-bine the results to obtain a solution to the original problem.We will also once again see the importance of loop invariants in writingcorrect code. Here is a note by Jon Bentley about binary search:I’ve assigned [binary search] in courses at Bell Labs and IBM. Profes-sional programmers had a couple of hours to convert [its] descriptioninto a program in the language of their choice; a high-level pseudocodewas fine. At the end of the specified time, almost all the programmersreported that they had correct code for the task. We would then takethirty minutes to examine their code, which the programmers did withtest cases. In several classes and with over a hundred programmers,the results varied little: ninety percent of the programmers found bugsin their programs (and I wasn’t always convinced of the correctness ofthe code in which no bugs were found).I was amazed: given ample time, only about ten percent of profes-sional programmers were able to get this small program right. ButLECTURE NOTES AUGUST 31, 2010Binary Search L3.2they aren’t the only ones to find this task difficult: in the history inSection 6.2.1 of his Sorting and Searching, Knuth points out thatwhile the first binary search was published in 1946, the first publishedbinary search without bugs did not appear until 1962.—Jon Bentley, Programming Pearls (1st edition), pp.35–36I contend that what these programmers are missing is the understandingof how to use loop invariants in composing their programs. They helpus to make assumptions explicit and clarify the reasons why a particularprogram is correct. Part of the magic of pre- and post-conditions as well asloop invariants and assertions is that they localize reasoning. Rather thanhaving to look at the whole program, or the whole function, we can focuson individual statements tracking properties via the loop invariants andassertions.Before we introduce binary search, we discuss linear search.2 Linear Search in an Unsorted ArrayIf we are given an array of integers A without any further information andhave 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 thatequals x. If we have gone through the whole array and still not found suchan 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? Forthe 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 thisbecause it uses is_in, which is the very function we are defining!LECTURE NOTES AUGUST 31, 2010Binary Search L3.3This is small illustration of the general observation that some functionsare basic specifications and are themselves not subject to further specifica-tion. Because such basic specifications are generally very inefficient, theyare mostly used in other specifications (that is, pre- or post-conditions, loopinvariants, general assertions) rather than in code intended to be executed.3 Sorted ArraysA 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 smalleror equal to its right neighbor. We need to be careful about the loop invari-ant to guarantee that there will be no attempt to access a memory elementout 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 andn − 1. This is a simple or on boolean values (true and false) and not anexclusive 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, thenbefore the check the exit condition of the loop the first time we have i = 0and n = 0, so it is not the case that i ≤ n − 1. Therefore the second part ofthe loop invariant does not hold. We account for that explicitly by allowingn to be 0.For an example of reasoning with loop invariants, we verify in somedetail 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 becausethe precondition of the function requires n ≥ 0. But if n > 0 and i = 0then i ≤ n − 1. We also have 0 ≤ i so 0 <= i && i <= n-1 holds.LECTURE NOTES AUGUST 31, 2010Binary Search L3.4Loop Traversal: Assume the loop invariant holds before the test, so eithern = 0 or 0 ≤ i ≤ n − 1. Because we do not exit the loop, we also havei < n − 1. The step statement in the loop increments i so we havei0= i + 1.Since i0= i + 1 and 0 ≤ i we have 0 ≤ i0. Also, since i < n − 1 andi0= 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 theright disjunct is true for the new value i0of i.One pedantic point (and we do want to be pedantic in this class whenassessing function correctness, just like the machine is): from 0 ≤ i andi0= i + 1 we inferred 0 ≤ i0. This is only justified in modular arithmetic ifwe know that i + 1 does not overflow. Fortunately,


View Full Document

CMU CS 15122 - Lecture Notes on Binary Search

Download Lecture Notes on Binary Search
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture Notes on Binary Search and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture Notes on Binary Search 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?