久野です。

yas@is.tsukuba.ac.jpさん:
> たのですが、precondition とか invariant という言葉が一瞬通じ
> ませんでした。

  なるほど…確かにそういうことは習わないかもorz

> まあ、precondition とか invariant はわからなくてもassert() 

  それは…使えはするだろうけど効果半減じゃないすかね? ^_^;

> は使えます。大学のカリキュラムのどこかで教えているかというと、

  教えていないかも知れない。Hoare Logicとか私は結局ゼミとかで
始めて接したような気がする。

> どっかでは教えてるんだろうけど、assert() ととは結び付いてい
> ないのでしょう。Ｃ言語でそういうのを使ってプログラムの検証す
> るのは難しいから。

  assertは「検証」じゃないんですよ。抽象データ型なりをCで実現す
るときに維持すべき条件も抽象データ型の上で考えて、それをCに翻訳
したものをCの条件式として書くんじゃないかな。2重チェックという感
じですかね。

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

              …そうじゃないと思うけどなあ。              久野