linear searchのloop不変式について考えてみた。

algorithm

リニアサーチは配列arrayからある値valueのある位置(インデックス)の最小値を返します。もしarrayの中にvalueが無ければNoneを返します。このときのloop不変式としては、loopをlower <- 0 to upper (upper=len(array))の範囲で回した時に「array[lower:upper+1]の範囲にvalueがあるか、arrayにはvalueが含まれない」をとれると思います。なぜならば


  • [ループ前]
    array[lower:upper+1]=array[0:len(array)+1]=arrayなので、成り立ちます。

  • [ループ中]
    array[:lower]にはvalueがないことが分かっているので、もしvalueがarrayにあれば(0<=lower<= upper, 0<= upper <= len(array))array[lower:upper+1]にvalueが含まれることになります。なので不変式に従っています。

  • [ループ後]
    ループ後はarray[lower:upper+1]==[value]かarray[lower:upper+1]==[ ]になっています。なので、不変式に従っています。あとループ後は上に書いたアルゴリズムの出力を作れている必要があるのですが、array[lower:upper+1]==[value]はarray[lower]==valueだと絞れていることを意味するので、それはできていることになります。あとarrayにvalueが無いこともarray[lower:upper+1]==[ ]となって、候補が0になっていることを示しているので、これはこれで良いんだと思います。「array[lower:upper+1]はvalueに等しくなり得る要素の集合で、もしこれが空になればvalueはarrayに含まれないことを意味する」と言ったほうがスッキリするかもしれません。


これで、下に書いたコードの正当性がある程度示されたってことになるんだと思います。よくはわからないですが、なんとなく自信がついた気がします。

#!/usr/bin/env python2.6
def linear_search(array, value):
    length = upper = len(array)
    lower = 0
    while lower < upper:
        if array[lower] == value:
            upper = lower
            continue
        lower += 1
    ta = array[lower:upper+1]
    if ta == []:
        return None
    else:
        assert([value] == ta)
        return lower
if __name__ == '__main__':
    assert(linear_search([2,4,6,8,10], 3) is None)
    assert(2 == linear_search([2,4,6,8,10], 6))
    assert(0 == linear_search([2,4,6,8,10], 2))
    assert(4 == linear_search([2,4,6,8,10], 10))