太田です。
おおむらさん
>OSとマルチスレッドが外部表明でカバーできないのは、時間が主要な
>ファクターになるからでしょうか? 何かもっと本質的な問題が
>あるのかな??
>
>マルチスレッドに関しては、たとえば、スレッド間のタイミングに
>関するシナリオを書いて、それをシミュレーションしてくれる
>ツールみたいのがあればいいなあと思っているのですが、そういう
>ツールはないんでしょうか?
>
>すいません、最後はとりとめがなくなってしまいました…
>ううむ。全部か・・・
局部の反応ですが，アサーションとDbCの拡張として
時相論理
http://www-6.ibm.com/jp/developerworks/java/020927/j_j-diag0723.html
http://www-6.ibm.com/jp/developerworks/java/021101/j_j-diag0827.html
はどうでしょうか。時間の概念を絡めた形式仕様記述(といっても研究ベースのもの
ほど分かりにくくないです)の一種で，スレッドに対しても有効な模様です。「シ
ミュレーション」というわけにはいかないようですが。
おおた oota_ken@....com
_________________________________________________________________