公理的意味論を使ってプログラムの正しさを証明する (2)公理的意味論 (axiomatic semantics) の2回目。 今回は二分探索をおこなうプログラムを検証する。 まとめ: 二分探索 (binary search) とは、 ソートされた数値の順列から目的の要素をすばやく検索するアルゴリズムである。 以下のような n個の要素をもつ数列 a = [ 0, ..., i0, ..., i, ..., i1, ... n-1 ] があるとき、2つの点 i0, i1 にはさまれた中点 i を考える。ここで、 目的の要素が [i0,i) の間にあれば、i よりも左側にある範囲を探索する。 目的の要素が [i,i1) の間にあれば、i よりも右側にある範囲を探索する。 以上の操作で、毎回、探索する要素の個数は半分になっていく。 これを繰り返すと、最終的に約 log2(n) の繰り返しで目的の要素を発見できる。 これは n個の要素を左から順に調べる
