
契約による設計(DbC )は、契約プログラミング、契約によるプログラミング、契約による設計プログラミングとも呼ばれ、ソフトウェアを設計するためのアプローチです。
この規定では、ソフトウェア設計者は、ソフトウェアコンポーネントに対して、事前条件、事後条件、および不変条件によって抽象データ型の通常の定義を拡張した、形式的で正確かつ検証可能なインターフェース仕様を定義する必要があるとされています。これらの仕様は、ビジネス契約の条件と義務という概念的なメタファーに従って、「契約」と呼ばれます。
DbCのアプローチでは、サーバーコンポーネント上で操作を呼び出すすべてのクライアントコンポーネントが、その操作に必要な前提条件を満たすことを前提としています。
この仮定がリスクが高すぎると考えられる場合(マルチチャネルや分散コンピューティングなど)、逆のアプローチが採用されます。つまり、サーバーコンポーネントは、クライアントコンポーネントのリクエストを処理する前、または処理中に、関連するすべての前提条件が満たされているかどうかをテストし、満たされていない場合は適切なエラーメッセージを返します。
この用語は、 Eiffel プログラミング言語の設計に関連してBertrand Meyerによって造語され、1986 年以降にさまざまな記事[ 1 ] [ 2 ] [ 3 ]および彼の著書『オブジェクト指向ソフトウェア構築』の 2 つの連続した版 (1988 年、1997 年)で初めて説明されました。Eiffel Software は 2003 年 12 月にDesign by Contract の商標登録を申請し、2004 年 12 月に登録されました。[ 4 ] [ 5 ]この商標の現在の所有者は Eiffel Software です。[ 6 ] [ 7 ]
契約による設計は、形式検証、形式仕様、およびホーア論理に関する研究にルーツを持つ。その独創的な貢献には以下が含まれる。
DbCの中心的な考え方は、ソフトウェアシステムの要素が相互の義務と利益に基づいてどのように連携するかというメタファーです。このメタファーはビジネスの世界から来ており、「顧客」と「サプライヤー」が「契約」に合意し、例えば次のようなことが定義されます。
同様に、オブジェクト指向プログラミングにおけるクラスのメソッドが特定の機能を提供する場合、それは以下のことを行う可能性があります。
この契約は、義務を形式化したホアの三つ組と意味的に同等である。これは、設計者が契約の中で繰り返し答えなければならない「三つの質問」に要約できる。
多くのプログラミング言語には、このようなアサーションを行うための機能が備わっています。しかし、DbCはこれらの契約がソフトウェアの正しさにとって非常に重要であるため、設計プロセスの一部として組み込むべきだと考えています。事実上、DbCはアサーションを最初に記述することを推奨しています。契約は、コードコメントで記述したり、テストスイートで強制したり、あるいはその両方を行うことで、契約のための特別な言語サポートがなくても実現可能です。
契約の概念は方法/手順レベルまで及び、各方法の契約には通常、以下の情報が含まれます。
継承階層におけるサブクラスは、前提条件を弱めることはできますが、強化することはできません。また、事後条件と不変条件を強化することはできますが、弱めることはできません。これらのルールは、振る舞いのサブタイピングに近似しています。
すべてのクラス間の関係は、クライアントクラスとサプライヤークラスの間で成立します。クライアントクラスは、サプライヤーの機能を呼び出す際に、クライアントの呼び出しによってサプライヤーの状態が損なわれないようにする義務があります。同様に、サプライヤーは、クライアントの状態要件に違反しない戻り状態とデータを提供する義務があります。
例えば、サプライヤーのデータバッファでは、削除機能が呼び出されたときにバッファ内にデータが存在することが要求される場合があります。その後、サプライヤーはクライアントに対し、削除機能の処理が完了したら、データ項目がバッファから確実に削除されることを保証します。その他の設計契約としては、クラス不変条件の概念があります。クラス不変条件は、(ローカルクラスに関して)各機能の実行終了時にクラスの状態が指定された許容範囲内に維持されることを保証します。
契約を利用する場合、供給者は契約条件が満たされていることを確認します。これは「攻撃的プログラミング」と呼ばれる手法で、一般的にはコードは「重大なエラー」を起こすべきであり、契約検証はそのための安全網となるという考え方です。
DbCの「完全失敗」特性により、各メソッドの意図された動作が明確に指定されるため、契約動作のデバッグが容易になります。
このアプローチは、前提条件が破られた場合にサプライヤーが対処方法を判断する防御的プログラミングとは大きく異なります。多くの場合、サプライヤーは例外をスローしてクライアントに前提条件が破られたことを通知し、DbCと防御的プログラミングのどちらの場合も、クライアントはそれに対する対応方法を判断しなければなりません。このような場合、DbCはサプライヤーの作業を容易にします。
契約による設計は、ソフトウェアモジュールの正確性に関する基準も規定する。
契約による設計は、各コードの契約が完全に文書化されているため、コードの再利用を促進する効果もあります。モジュールの契約は、そのモジュールの動作に関するソフトウェアドキュメントの一種とみなすことができます。
例えばC++における契約による設計は、次のようになります。[ 8 ] [ 9 ]
int f ( const int x ) pre ( x != 1 ) // 事前条件アサーションpost ( r : r == x && r != 2 ) // 事後条件アサーション。r は f の結果オブジェクトの名前です{ contract_assert ( x != 3 ); // アサーション文return x ; }バグのないプログラムの実行中は、契約条件に違反してはなりません。そのため、ソフトウェア開発中は通常、デバッグモードでのみ契約チェックが行われます。リリース時には、パフォーマンスを最大化するために契約チェックは無効になります。
多くのプログラミング言語では、契約はassertで実装されます。C/C++ ではリリースモードではデフォルトで assert がコンパイル時に削除され、C# [ 10 ]や Java でも同様に無効化されます。
Python インタープリタを引数として「 -O 」(「optimize」の略)を指定して起動すると、同様に Python コードジェネレーターは assert のバイトコードを出力しなくなります。 [ 11 ]
これにより、開発時に使用されるアサートの数や計算コストに関係なく、本番コードにおけるアサートの実行時コストが効果的に排除されます。なぜなら、コンパイラは本番コードにそのような命令を含めないからです。
契約による設計は、単体テスト、統合テスト、システムテストといった従来のテスト戦略に取って代わるものではありません。むしろ、テストフェーズ中に、個別のテストと本番コードの両方で有効化できる内部自己テストによって、外部テストを補完するものです。
内部自己テストの利点は、クライアントが不正な結果として認識する前にエラーを検出できる点です。これにより、より早期かつ具体的なエラー検出が可能になります。
アサーションの使用は、テストオラクルの一種、つまり契約の実装によって設計をテストする方法と考えることができる。
DbCのほとんどの機能をネイティブに実装している言語には、以下のようなものがあります。
さらに、 Common Lisp Object Systemの標準メソッドの組み合わせには、メソッド修飾子 、 があり:before、これらによって、補助メソッドとして契約を記述するなど、さまざまな用途に使用できます:after。:around