Binary Search in an Array

Aug. 17, 2010 – 6 years, 7 months ago, by eifler

Short Description

Verify an operation that uses binary search to find a given entry in an array of entries that are in sorted order.

Code

Specification

Long Description

Arrays are the traditional first “collection” type, which may be a built-in type in the programming language or a user-defined abstract data type (ADT). A mathematical theory sophisticated enough to handle the array specification is an additional complication. Unless this theory contains special operators that hide them, quantifiers are involved in the specification; to simplify automated verification in the presence of existential quantifiers, ghost (or adjunct) variables may be needed in the specification and/or implementation.
This code also involves at least two types: the numerical index type and the array type, and possibly a separate entry type. A recommended candidate for the incorrect version of the code is any close cousin of the Java binary search function whose defect was pointed out recently in a Google blog “after lying in wait for nine years or so”. The numerical index type for the array must be considered bounded to manifest the defect in that code.

Variations: If the type of the array elements is not fixed but rather is a parameter to the specification(s) and code, then additional issues arise here. In particular, the actual entry type might be an ADT itself; the specification and computation of the ordering among entries and equality of entries become interesting.

Supplementary Materials

Here is the link to the aforementioned Google blog

The paper from which this benchmark is taken was published in may 2008 by various authors from Clemson University, Clemson and the Ohio State University, Columbus. It contains some more benchmarks which are also included on this site.

Submitted by

Timo Eifler verifythis@cost-ic0701.org