公理的意味論を使ってプログラムの正しさを証明する (2)

Last Modified: Tue Jan 11 13:59:36 UTC 2011

公理的意味論 (axiomatic semantics) の2回目。 今回は二分探索をおこなうプログラムを検証する。


まとめ:

二分探索 (binary search) とは、 ソートされた数値の順列から目的の要素をすばやく検索するアルゴリズムである。

以下のような n個の要素をもつ数列

a = [ 0, ..., i0, ..., i, ..., i1, ... n-1 ]
があるとき、2つの点 i0, i1 にはさまれた中点 i を考える。ここで、 以上の操作で、毎回、探索する要素の個数は半分になっていく。 これを繰り返すと、最終的に約 log2(n) の繰り返しで目的の要素を発見できる。 これは n個の要素を左から順に調べる (逐次検索) よりも格段に速い。

Kunth もいっているように [1]、 二分探索は単純だがバグが入りやすい構造をしている。 そのため、その正当性を証明するための条件を知っていることは バグの少ないソフトウェアの構築に役立つ。


bsearch.py

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

Yusuke Shinyama