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

In article <YAS.04Sep11201327@kirk.is.tsukuba.ac.jp>, yas@is.tsukuba.ac.jp (Yasushi Shinjo) writes
> 新城です。loop invariant は、けっこう厳しい。

これは、その通りで、実際の検証に使うには難しすぎるみたいですね。
そういう難しすぎる手法もたくさんあります。ポリヘドラ系とか。

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

まず、作成したLSIの歩止まりを判定しなければならないので、一
通り(回路毎)のテストを生成する必要があります。LSI設計の限界
は、それで決まると言われているようですね。

もう一つは、ハードは修正が高く付くことが多いので、ハードは修
正せずにソフトで対処する... じゃなくて、モデル検証などを使っ
ても元が取れます。Intel はPentinumの乗算器のミスで痛い目にあ
ったので力を入れているようですね。

例えば、
    main() {
        while() { main_loop: if (event = event()) hoge(event); }
    }
みたいなメインループを持つシステムは多いですよね。(Operating System
とかもそう) この時に、

    常にメインループに戻って来る

あるいは、

    メインループに5msec以内に戻って来る
 
ってのを保証したいでしょ? これは自然だと思うんだ。で、

    [] <5msec> main_loop
        常に、5msec 以内に、main_loop に到達する

みたいなプロパティを検証するわけです。これはトートロジーっぽく
ないんじゃないかな。

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