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

Last Modified: Fri Jan 14 10:34:24 UTC 2011

公理的意味論 (axiomatic semantics) の3回目。 今回は Python の組み込みモジュールである bisect を検証する。


まとめ:

Python の bisect関数 (厳密には bisect_left 関数)は、 与えられた配列 a に要素 x を挿入するさい、「どの位置に挿入すればよいか」を決定する。

配列 a はすでにソートされていると仮定する。 a中に x と同じ要素がすでに存在する場合は、 x がもっとも左側に挿入されるような位置を返す。 (これが bisect_left の意味である)

補足:

動画中では言及されていないが、 a[lo-1] < x and x <= a[lo] という仕様が使えるのは a があらかじめ昇順にソートされている場合のみである。 a がランダムな順列の場合は、このような境界の位置を見つけても正しい結果にはならない。

結論:

数理論理学は重要だ。


bisect.py

# bisect(a, x)
#   a の中に x を挿入すべき位置を返す。
#   x と同じ要素がすでに存在する場合は、x がもっとも左側に挿入されるような位置を返す。
def bisect(a, x):
    N = len(a)
    lo = 0
    hi = N

    while lo < hi:
        # x は lo...hi の範囲内か、その境界上にある。
        assert (lo == 0 or a[lo-1] < x)
        assert (hi == N or x <= a[hi])
        mid = (lo+hi)//2
        assert lo <= mid and mid < hi
        
        if a[mid] < x:
            assert (lo == 0 or a[mid] < x)
            lo = mid+1
            assert lo-1 == mid
            assert (lo == 0 or a[lo-1] < x)
            
        else:
            assert x <= a[mid]
            assert (hi == N or x <= a[mid])
            hi = mid
            assert (hi == N or x <= a[hi])
            
        assert (lo == 0 or a[lo-1] < x)
        assert (hi == N or x <= a[hi])
        assert lo <= hi

    assert lo == hi
    assert (lo == 0 or a[lo-1] < x)
    assert (lo == N or x <= a[lo])
    
    return lo

a = [ 0, 1, 4, 4, 9 ]
assert bisect(a, 4) == 2
assert bisect(a, 2) == 2
assert bisect(a, -5) == 0
assert bisect(a, 10) == 5

Yusuke Shinyama