河野真治 @ 琉球大学情報工学です。

In article <YAS.04Sep11171406@kirk.is.tsukuba.ac.jp>, yas@is.tsukuba.ac.jp (Yasushi Shinjo) writes
> この辺りに検証が使えないという問題の本質があるかもね。Ｃ言語
> でプログラムを書く時と assert() のレベルは近い。けど、
> validity とかsatisfiablity というのレベルとは違う。違うレベ
> ルで書く事が難し。

まったく違いますね。このあたりが、ハードウェアの信頼性とソフ
トウェアの信頼性の差を生んでいる原因だと思います。僕は、ある
時点で、検証されないソフトウェアが受けいられなくなると思う。

動くソフトと、ちゃんと動くソフトの差は結構大きい。

> assert() の記述から検証用の条件を自動生成できれば、いいんじゃ
> ないですか。

それはあったと思います。つうか、最近はそういうのが主流かも。
なんだけど、自動生成したものが検証可能かどうかはわからないと
思う。なんかの制限が必要ですね。

> 昔、「実行可能な仕様」というのがあったけど、あれはどうなった
> んだろう。

> >      [] (ボタンが押される -> <> 反応変数がセット)
> こんな感じにハンドアセンブルしないとだめなのね。今の段階では。
> おまけに、このハンドアセンブルが正しいかどうかも不明です。

そういう言い方するのか。この作業は、

   プログラムがちゃんと動くということはどういうことなのか

っていうのを定義していく作業なんです。それが仕様を書く、ある
いは、検証可能なプロパティを決める、あるいは、十分なテストを
書くってことですよね。

僕は、それができないプログラマは、もう役に立たないと思う。

> それで、最後は、この検証に通ったものを正しいとすると定義する
> しかなくなって、トートロジーっぽくなるわけです。

例えば、ループインバリアントって、あんまり自明じゃないですよ
ね。だけど、ループインバリアントをチェックするのは、トートロ
ジーっぽいよね。でも、そのループの正しさって実は、ループイン
バリアントで定義されるわけだよね。検証は、どっちかっていうと、
インバリアントを見付ける作業です。

---
Shinji KONO @ Information Engineering, University of the Ryukyus
河野真治 @ 琉球大学工学部情報工学科