[debian-users:12169] Re: historical info

["Ken N." <kenn@xxxxxxxxxxxxxxxxx>]

ついてくのが結構大変。いや、理論じゃなくて議論のペースに。


In <19990122013937A.oka@debian.or.jp>
[debian-users:12137] Re: historical info, Jan.22 '99 01:39 JST
oka@debian.or.jp says:
=   岡＠情報科学.高知大です。
=   
=   # 風呂に入ったら回復したのでもうひと頑張り。

＃やっぱり若者は回復が早いなぁ。きっと朝までダイジョーブなんで
　しょうね (『え、なにが？』とかって訊かないように B-)

それはさておき、今日の所は先に一点だけ確認させてください。続き
は明日。

=   僕はと言うと、以前は Ken N. さん寄りだったんですが、Debian
=   はそこまで完璧ではないことを知って、むしろ完全性を維持しよう
=   という行為がシステムを脆くする事に気がつきました。どんなにシ
=   ステムが正しさを維持しようとしても、アプリケーションレベルで
=   システムの状態破壊が起きる可能性が充分考えられるからです。

これは具体的にはどういう場合ですか？
いえ、別に反論のための反論をしようとするつもりはなくて、ただ、
そのような可能性については私は全く考察していなかったので、岡さ
んがどのような可能性に思い当たったのかを教えて頂きたいのです。


In <19990122023254N.oka@debian.or.jp>
[debian-users:12139] Re: historical info, Jan.22 '99 02:32 JST
oka@debian.or.jp says:
=   
=    {y > 0} x := y {x > 0}
=   
=   です。直感的には、あたりまえの事を説明しているだけです。関数
=   (もちろん純粋な関数です)の引数に与える制約条件が事前条件、得
=   られる返り値に与える制約条件が事後条件だと思えば、だいたい分
=   かると思います。
=   これと導出規則等を使えば、プログラムの正しさを証明する
=   ことさえある程度可能です(当然無限ループとかがネックになる)。

純粋な関数なので副作用は持たない、ループは末端再帰に帰結できる、
各再帰呼出で事前条件に再帰続行の条件を繰り込み、あとは上手に数
学的帰納法に持ち込んで証明終り、そんな感じですか。


 -.- . -. -.
Ken Nakagaki <kenn@xxxxxxxxxxxxxxxxx>
「会社は主にそれ自身の慣性によって前進している」-- Gerry Spence