Binary Search Variants: A Comprehensive Analysis
For developers and educators, this work offers a systematic, verified reference for correct binary search implementations, but it is an incremental synthesis of known techniques.
This paper provides a comprehensive analysis of binary search variants, introducing a unified framework with five core variants and a combined search function, validated by over 9,500 tests and 21 Dafny formal verifications.
Binary search is deceptively simple in concept yet notoriously difficult to implement correctly. This paper presents a unified treatment of binary search: five core variants, six derived query functions, and four standard library implementations (BSD, glibc, Java, C++ STL), each with consistent notation, loop invariants, and analysis. We introduce bsearch_ultimate, a combined search that subsumes all variants in a single call. Every algorithm is provided as synchronized Python code, Dafny formal proof, and pseudocode. All implementations are validated by over 9,500 tests and 21 Dafny formal verifications; an additional six deliberately faulty implementations demonstrate common bug categories and Dafny's ability to detect them. We also provide memorable rules linking boundary choices to loop conditions and update formulas.