形式検証
Prologのキーワードをたどって下のエントリを見つけました。
[id:bonotake:20051125]
そういえば、Concurrent Cleanにも定理証明系がくっついていたような。
Sparkle : http://www.cs.ru.nl/Sparkle/
ここっすね・・・って、重いよこのページ。
-
-
- -
-
ところで、「正しさ」の証明って、何をどう証明する気なんだろう？
と[id:sumii:20051125]で紹介されているVaultのプレゼンを見てみた。
http://research.microsoft.com/vault/
-
-
- -
-
えっと、下のようなところをきちんとできているかを検証したいと。
- 全てのメモリが正しく解放されているか？（２重に解放していないか？）
- 全ての場合わけをチェックできているか？
- 全てのスレッドの干渉を考慮に入れているか？
- 範囲チェックやらNullチェックやらなんやらかんやら
今までテストケースを工夫して作って検証してきたところを、コードそのものを解析して検証したいということかな？
-
-
- -
-
あれですね、Javaの例外。最後まで追いかけて、コンパイラが文句を言ってくれる。あれを強力にして、もっといろいろなことに使えるようにしようということですかね。
なんか、それっぽいことができればいいのに、みたいなことを、前につぶやいていたような気が・・・
-
-
- -
-
あった、あった。これだ。
[id:lethevert:20050720:p1]
これみたいなことを、もっと洗練した形でやりたいということなのかな？
どうも、Unit Testは気が乗らないと思っている（スマートじゃないように感じる）ので、こっちの線はかなり期待だ。
