契約による設計

契約による設計（Design By Contract、でざいん・ばい・こんとらくと）とは、ソースコードの中にプログラムが満たすべき仕様（契約）についての記述を盛り込み、設計の安全性を高めるプログラミングの技法のひとつである。契約プログラミング（Programming By Contract）や、Design by Contract の頭文字であるDbC (でぃーびーしー) とよばれることもある。

たとえば、あるサブルーチンの引数があるとして、ぬるぽやぬるりを防ぐために引数のnullチェックや境界チェックを行う、などというコーディング規約に近いものを、プログラミング言語の仕様として半ば強制することで、静的コード解析やドキュメント生成などを的確に行えるようにし、プログラムの品質を向上させようというものである。

条件の種類

契約は、コードの利用条件が満たされることによって成立する。 それら条件は、満たすべきタイミングと主体によって、以下の3種類に分けられる。

事前条件 (precondition) 

サブルーチンの開始時に、これを呼ぶ側で保証すべき性質。

事後条件 (postcondition) 

サブルーチンが、終了時に保証すべき性質。たとえば「戻り値は絶対にnullを返さない」などを決めておくことを言う。

不変条件 (invariant) 

クラスなどのオブジェクトがその外部に公開しているすべての操作の開始時と終了時に保証されるべき、オブジェクト毎に共通した性質。

コードを呼ぶ側が事前条件と不変条件を満たす義務を負うことで、呼ばれたコードはその条件が恒真であるとの前提を利益として得る。

引き換えに、呼ばれたコードは事後条件と不変条件を義務として負い、呼ぶ側の利益としてこれを保証する。

契約による設計をサポートする主な言語

ここに記載するプログラミング言語はあくまで一例でありすべてではない。

.NET Framework 4.0

.NET Framework 4.0では、コードコントラクト（Code Contracts）という名前の機能が追加され、プログラミング言語レベルではなく、ランタイムレベルで「契約による設計」に対応した。これにより.NET Framework系のすべてのプログラミング言語が対応することとなった。

また、Visual Studio用のアドオンも提供されており、契約による設計のキモである静的チェックやドキュメントの自動生成も行いえる。とくに静的チェックはとても重要な要素であり、これが使えないとただのコーディング規約程度の話で終わってしまい、契約による設計の魅力の99.9999%が失われる。

なおアドオンが使えないVisual Studio Expressではツール群が使えないので、ただの実行時のエラーチェックと化し、前述のように契約による設計の魅力の99.9999%が失われる。

コードコントラクトを利用するためのライブラリはSystem.Diagnostics.Contracts 名前空間にあり、事前条件、事後条件、不変条件などの表すための静的クラスが用意されている。

• http://msdn.microsoft.com/en-us/devlabs/dd491992

Eiffel

Eiffelは契約による設計を提唱・サポートした一番最初のプログラミング言語だそうだ。まったく知らない。

Sather

Eiffelから派生したサブセットで独自の進化を遂げてものらしい。 まったく知らない。

関連項目

• バートランド・メイヤー（仏：Bertrand Meyer） - 契約による設計の提唱者、Eiffelを作ったプログラマー
• リスコフの置換原則（Liskov substitution principle）
• 正当性（Correctness）
• 表明（Assertion）
• コーディング規約
• デザインパターン
• 設計
• 実装
• 仕様