新城です。loop invariant は、けっこう厳しい。

In article <3990496news.pl@rananim.ie.u-ryukyu.ac.jp>
        kono@ie.u-ryukyu.ac.jp (Shinji KONO) writes:
> 例えば、ループインバリアントって、あんまり自明じゃないですよ
> ね。だけど、ループインバリアントをチェックするのは、トートロ
> ジーっぽいよね。でも、そのループの正しさって実は、ループイン
> バリアントで定義されるわけだよね。検証は、どっちかっていうと、
> インバリアントを見付ける作業です。

「ループの正しさがループインバリアントで定義される」というの
は、同意しません。まだ見つかってないかもしれませんが、もっと
まともな方法があると思います。

簡単なループです。data[0] から data[9] の和を求めるループです。

s=0;
for( i=0; i<10; i++ )
{
   s+= data[i];
}

これの loop invariant と言われても、あんまりパッとするものか
出てきません。

(1) bool式の i<10 
(2) ループの前にj=10、ループの中の最後に j--; を入れて数式 j+i が不変
(3) s の値が data[0..i] の和になっている。

どれとっても、せいぜいトートロジーです。もっと他に、何か役に
たちそうな loop invariant はありますか。

In article <3990496news.pl@rananim.ie.u-ryukyu.ac.jp>
        kono@ie.u-ryukyu.ac.jp (Shinji KONO) writes:
> 動くソフトと、ちゃんと動くソフトの差は結構大きい。

日本語でそう書いてしまうとそうなんだけど、問題は２つあります。

(1) 「ちゃんと動く」というのをプログラミング言語並に形式的に
    書くこと（仕様を記述すること）が大変。
(2) そう書いた仕様が、元々やりたかった事と一致している事を調
    べる方法が、存在しない。

> > この辺りに検証が使えないという問題の本質があるかもね。Ｃ言語
> > でプログラムを書く時と assert() のレベルは近い。けど、
> > validity とかsatisfiablity というのレベルとは違う。違うレベ
> > ルで書く事が難し。
> まったく違いますね。このあたりが、ハードウェアの信頼性とソフ
> トウェアの信頼性の差を生んでいる原因だと思います。僕は、ある
> 時点で、検証されないソフトウェアが受けいられなくなると思う。

ハードウェアの設計では、形式的な証明の技術を使っているのですか。

＼＼　新城　靖　（しんじょう　やすし）　＼＼
＼＼　筑波大学　電子・情報　　　　　　　＼＼