公理的意味論 (axiomatic semantics) の2回目。 今回は二分探索をおこなうプログラムを検証する。
まとめ:
二分探索 (binary search) とは、 ソートされた数値の順列から目的の要素をすばやく検索するアルゴリズムである。
以下のような n個の要素をもつ数列
a = [ 0, ..., i0, ..., i, ..., i1, ... n-1 ]があるとき、2つの点 i0, i1 にはさまれた中点 i を考える。ここで、
n
個の要素を左から順に調べる (逐次検索) よりも格段に速い。
Kunth もいっているように [1]、 二分探索は単純だがバグが入りやすい構造をしている。 そのため、その正当性を証明するための条件を知っていることは バグの少ないソフトウェアの構築に役立つ。
NONE = -1 # bsearch(a, x) # a[i] == x であるような i を返す。 # x が a の中に存在しない場合は NONE を返す。 def bsearch(a, x): i0 = 0 i1 = len(a) found = NONE while found == NONE and i0 < i1: # found はまだ見つかっていないか、あるいは正しい位置を指している。 assert found == NONE or a[found] == x # invariant # x は a の中に存在しないか、存在するとしたら i0...i1 の範囲内にある。 assert (x not in a) or (x in a[i0:i1]) # invariant i = (i0+i1)//2 assert i0 <= i and i < i1 if a[i] == x: found = i elif a[i] < x: # x は a[i] の右側にある。 # a = [ ... i0 ... i ... i1 ... ] # a[i] x # i0 .... i1 assert (x not in a) or (x in a[i+1:i1]) i0 = i+1 else: assert x < a[i] # x は a[i] の左側にある。 # a = [ ... i0 ... i ... i1 ... ] # x a[i] # i0 ... i1 assert (x not in a) or x in a[i0:i] i1 = i assert i0 <= i1 assert found == NONE or a[found] == x # invariant assert (x not in a) or (x in a[i0:i1]) # invariant assert (found != NONE) or (i0 == i1) assert ((found != NONE and a[found] == x) or (found == NONE and x not in a)) return found