新城＠筑波大学情報です。こんにちは。

In article <3990493news.pl@rananim.ie.u-ryukyu.ac.jp>
        kono@ie.u-ryukyu.ac.jp (Shinji KONO) writes:
> あらゆる可能な実行の可能性に対してチェックするのが検証です。
> validity とか satisfiablity とか言う奴。( だから、その程度の
> 論理学は知らないと...)

この辺りに検証が使えないという問題の本質があるかもね。Ｃ言語
でプログラムを書く時と assert() のレベルは近い。けど、
validity とかsatisfiablity というのレベルとは違う。違うレベ
ルで書く事が難し。たとえると、高級言語とアセンブリ言語で同じ
プログラムを書くようなものです。今の場合、高級言語はＣ言語で、
アセンブリは、検証用の論理学です。

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

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

> 「反応がある」っていうのを定義して、それに対してチェック
> するみたいな感じ。
> 
> 例えば、反応があったら特定の変数をセットするような感じ
> にして、
>      [] (ボタンが押される -> <> 反応変数がセット)
>      常に                    いつか
> みたいなのを検証します。あらゆるボタンの押す順序に対して。

こんな感じにハンドアセンブルしないとだめなのね。今の段階では。
おまけに、このハンドアセンブルが正しいかどうかも不明です。
それで、最後は、この検証に通ったものを正しいとすると定義する
しかなくなって、トートロジーっぽくなるわけです。

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