アルゴリズムの正当性について

質問

線形探索法のアルゴリズムの擬似コードを書いて、そのアルゴリズムの正当性をループ不変式を用いて証明するという課題があります。

擬似コードは以下のような流れにしようと思いますが、この場合成り立つループ不変はどのようなことになりますか？

配列A[a1..an]に対してv=A[i]ならば添字iを、vがAの中になければNILを出力するアルゴリズムです。

for i ←1 to N
if A[i] = v
return i
return NIL

回答No.1

PRFRD · ベストアンサー

ループ開始時にて　A[j] ≠ v (j = 1, ..., i-1) 　でどうでしょう．

回答No.2

stomachman

えとですね、「配列A[a1..an]に対してv=A[i]ならば添字iを、vがAの中になければNILを出力する」では（a1およびanとは何者か、という話は別にしても、）何をやりたいんだか曖昧です。というのは、v=A[i]となるiが複数個ある場合にどうしたいのかが明示されていない。
　つまり、ご質問はやりたい事、すなわち仕様（output assertion）をきちんと記述出来ていないという所に問題があるんです。これが書けないと、証明すべき命題が定まりません。

　仮に、お書きの「疑似コード」こそがまさしくやりたい事なのだとすれば、その意味は「もし(1≦i≦Nかつv=A[i])となるiがあるならばv=A[i]となるiのうち最小のものを出力し、さもなければNILを出力する」ということ。言い換えれば、出力をkとするとき、
(∃j(1≦j∧j＜N∧A[j]=v)→(∀j(1≦j∧j＜k → A[j]≠v)∧A[k]=v)) ∧ (∀j(1≦j∧j＜N→A[j]≠v)→k=NIL)

　また、もしも　「配列A[1..N]に対してv=A[i]となるiがあるならばそのようなiのうちのどれかひとつを出力し、vがAの中になければNILを出力する」という話であるならば、
(∃j(1≦j∧j＜N∧A[j]=v)→A[k]=v) ∧ (∀j(1≦j∧j＜N→A[j]≠v)→k=NIL)
というのが仕様です。

　いずれの場合もinvariant assertionとして、ANo.1すなわち
∀j(1≦j∧j＜i → A[j]≠v)
を選ぶのが良さそう。
　けれども、その心配をする以前に、証明したい命題がまだ決まっていないんです。