なつたん

この章は面白い。分析が終わって、実際に検証をする時の方法についていろいろと書いてあります。

Formal verificationについて。

Most tool vendors will tell you that formal verification provides a 100% proof of correctness. Although this is true in theory, we are still unable to answer the question, "When have I done enough verification?" The formal proof is only as good as the set of properties provided, and there are no tools that can tell you how good or complete the set of properties is, or which behaviors are not described bye those properies.

この本の中ではfomal 検証とrule baseは同じ意味ととらえてよさそう。
解きたい問題にたいして、正しい制約(ルール)を与えられたかがわからないんだよね。逆に考えるとルールで記述できるアプリケーションにのみ有効という事？
いやいや、そうじゃない。ルールで記述できる部分についてのみ有効だ。O-inのクロック検証のようにアプリケーションと独立して、設計ルールのチェックはできる。

エキスパートシステムそのものにも見えるし、ただのLintじゃねとも思う僕ガイル。

DAFCAなる会社を発見。
日本語の記事はここ。
http://techon.nikkeibp.co.jp/article/NEWS/20060706/118923/
むう、3年前 DACに行かせてもらったとき、BluespecもDAFCAも無かったのに・・・・。

複雑な思いはあるが、今は自分の仕事を頑張ろう。