^ back

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

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

まとめ:

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

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

a = [ 0, ..., i0, ..., i, ..., i1, ... n-1 ]

• 目的の要素が [i0,i) の間にあれば、i よりも左側にある範囲を探索する。
• 目的の要素が [i,i1) の間にあれば、i よりも右側にある範囲を探索する。

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