新城＠筑波大学筑波です。こんにちは。

In article <cho5h1$27kh@utogw.gssm.otsuka.tsukuba.ac.jp>
        kuno@gssm.otsuka.tsukuba.ac.jp writes:
> 久野です。
>   assertは「検証」じゃないんですよ。抽象データ型なりをCで実現す
> るときに維持すべき条件も抽象データ型の上で考えて、それをCに翻訳
> したものをCの条件式として書くんじゃないかな。2重チェックという感
> じですかね。

検証と２重チェックか。違いがよくわかりません。
コンパイル時だと検証で、実行時だとチェックですか。

In article <3990477news.pl@rananim.ie.u-ryukyu.ac.jp>
        kono@ie.u-ryukyu.ac.jp (Shinji KONO) writes:
> (FITは、なんとなくパス... 京都だったのか)

同志社大学。京都の人は京都市ではないから京都とは言わないのか
もしれない。

> assert は、いいんだけど、「assert で失敗したらどうするの?」
> っていう問題があるんですよね。もし、「失敗したら、これこれ、
> こうする」っていうのがあるなら、
>     お前、それは assert ではなくて、プログラムの一部だろう
> と僕は思うし。

普通は、assert() はデバッグ時にしか働きません。デバッグが終っ
たら、消えます。

#ifdef  NDEBUG
#define assert(x) /**/
#else
...
#endif


> > Pascal verifier でしたっけ。そういうの書かないとプログラムを
> > コンパイルしてくれないってのは。
> 
> これは知らなかった。Proof carrying code とかいう方が業界っぽい
> かも。

Pascal verifier は、昔の話です。Pascal 全盛の時代。

Proof carrying code は、最近の話です。Ｃで書かれたプログラム
で、バイナリになっているので、まあ機械語になっているのですが、
それをカーネル・モジュールをロードする前に、「この範囲のアド
レスしかアクセスできません」ということを証明するという話を聞
いた時には、これは使えると思いました。

> 検証するには検証する命題を作らないといけないわけですけど、
> それを作り溜めるのが大変とかいう話があるみたいです。例えば、
>    電源が入っている間は、ボタンを押すと、何らかの反応がある
> とかって検証できたらトートロジーだと思いますか?

難しい。まず、電源切れているとプログラムが動いていないから関
係ない。すると、
        ボタンを押すと、何らかの反応がある
「反応がある」のは、実時間性まで言わないと意味がないので、
この時点であいまいだけど、たとえば、１秒としましょう。
        ボタンを押すと、１秒以内に何らかの反応がある
こういうシステムを作れと言われたら、作れそうな気がするけど、
証明しろと言われると、具体的にどこまで言えば証明になっている
のか、まだ曖昧で。割込みから足算して１秒以内でいいんですか。

＼＼　新城　靖　（しんじょう　やすし）　＼＼
＼＼　筑波大学　電子・情報　　　　　　　＼＼