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

In article <YAS.04Sep9013211@kirk.is.tsukuba.ac.jp>, yas@is.tsukuba.ac.jp (Yasushi Shinjo) writes
> 昨日、FIT という全国大会があって、京都に行ってきました。そこ
> で、assert() を別スレッドでやって高速化するという発表があっ
> たのですが、precondition とか invariant という言葉が一瞬通じ
> ませんでした。

(FITは、なんとなくパス... 京都だったのか)

assert は、いいんだけど、「assert で失敗したらどうするの?」
っていう問題があるんですよね。もし、「失敗したら、これこれ、
こうする」っていうのがあるなら、

    お前、それは assert ではなくて、プログラムの一部だろう

と僕は思うし。

> Pascal verifier でしたっけ。そういうの書かないとプログラムを
> コンパイルしてくれないってのは。

これは知らなかった。Proof carrying code とかいう方が業界っぽい
かも。

> プログラムの検証も、今の技術だとトートロジーっぽくなっちゃう
> ですよね。検証をパスしたものを正しいと定義しているわけだし。

すべての定理はトートロジーという立場があったような気がする。
命題論理なんかはそうなんですね。

検証するには検証する命題を作らないといけないわけですけど、
それを作り溜めるのが大変とかいう話があるみたいです。例えば、

   電源が入っている間は、ボタンを押すと、何らかの反応がある

とかって検証できたらトートロジーだと思いますか?

(だから、論理学は知っていた方が....)

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