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.

翻译：二分查找虽在概念上看似简单，但实现正确却以困难著称。本文对二分查找进行了统一论述：五种核心变体、六种派生查询函数，以及四种标准库实现（BSD、glibc、Java、C++ STL），每种均配以一致的符号表示、循环不变量及分析。我们引入bsearch_ultimate——一种通过单一调用涵盖所有变体的组合式搜索方法。每种算法均提供同步Python代码、Dafny形式化证明及伪代码。所有实现经由超过9500项测试及21次Dafny形式化验证；额外六种人为植入缺陷的实现则展示了常见错误类别及Dafny检测这些错误的能力。我们还提供了将边界选择与循环条件及更新公式相关联的易于记忆的规则。