こんにちは、小室です。
XPも Eiffelも実践しているわけではないので
はずしているかもしれませんが。
firo wrote:
> > 私もこの点が気になってJPLoPの友野さんにお聞きしたのですが、XPでいう
> > テストはMeyerの契約主導設計の実現の一種であるというお話でした。「表
> > 明」というのでしょうか。「表明」は「こうなっているべきだ」というのを事
> > 前条件、事後条件、不変条件で通常そのプログラムの内部で記述するものです
> > (というのは平鍋さんのほうが詳しいと思います)が、それを外側にもってきた
> > のが、XPのテストということでしょうか。
> 私は、表明とXPのテストは、レベルが１段階異なると思います。
表明はもともとプログラム意味論（のひとつである公理的意味論）で
提案された概念ですよね。Eiffelの表明がもともとのプログラム意味論でいう
表明のどこまでをサポートしているのか正確には知りませんが、
理論的には、サポートするプログラミング言語に一定の制限を置いておけば
表明によってプログラムの意味が記述でき、
したがって検証もできるはずです。
ただし、このやり方で現実のプログラムの正当性を検証するのは
（すべてのステートメントに論理式で厳密なコメントをつけるような
ものですから）
大変な作業なので、行われた例はほとんどないと思います。
私の持っている感じでは、表明によるプログラム検証と
テストによる検証の違いは次のような方向性の違いのように思います：
・表明によるプログラム検証は、
そのプログラムがどういうものであるべきか、その性質を記述して行く
トップダウン方向のアプローチ。
・テストによる検証は
そのプログラムが実際具体的なデータを与えたときどう振舞うかを確かめる
ボトムアップ方向のアプローチ。
このように方向性が違って、いわば相補的になっていますから
両者をうまく組み合わせれば、単独でやるより効果をあげられる
可能性はあるのではないかと私は思っています。
例えば、自分の書いたプログラムに証明をつけてみると
普通にテストしたのでは見つからないような（根本的な）バグを
見つけられることがあります。（そもそも仕様にそっていないとか
採用したデータ型に不備があるとか etc）
ただ、証明を与えるのは相当の労力がいるので、自分で書いた
プログラムといえども、いつでもやるというわけにはいきません。
（この辺、非常に強力な定理証明系とかあれば、プログラム的に
賢く補助できるのかも
知れませんが、私はその辺の最近の発展については知りません。）
> 次にEiffelの場合、
>
> Eiffelの場合は、表明をプログラムの中に書けるのですが、
> 私はあまり詳しくなくて、仮定的にいいます。
> もし、仮にEiffelがコンパイルレベルで表明が正しく実現できることを
> チェックできるとすれば、テストは不要になるでしょう。つまり、コンパイル
> の中でロジックの意味的な解析まで行うということです。
静的な解析には限界があり、一般に、チェックできないことが残ります。
Eiffelの場合も実行時チェックをやっているはずだと思います。
小室