契約による設計
契約による設計方式

契約による設計( DbC ) は、契約プログラミング、契約によるプログラミング、契約による設計プログラミングとも呼ばれ、ソフトウェアを設計するためのアプローチです。

ソフトウェア設計者は、ソフトウェアコンポーネントに対し、形式的、正確かつ検証可能なインターフェース仕様を定義する必要があります。インターフェース仕様は、抽象データ型の通常の定義を、前提条件、事後条件、不変条件によって拡張します。これらの仕様は、ビジネス契約の条件と義務の 概念的なメタファーに従って、「契約」と呼ばれます。

DbC アプローチでは、サーバー コンポーネントで操作を呼び出すすべてのクライアント コンポーネントが、その操作に必要な指定された前提条件を満たすものと 想定されます。

この仮定がリスクが高すぎると考えられる場合 (マルチチャネルや分散コンピューティングなど) は、逆のアプローチが取られます。つまり、サーバー コンポーネントは、関連するすべての前提条件が満たされていることを (クライアント コンポーネントの要求を処理する前または処理中に) テストし、満たされていない場合は適切なエラー メッセージで応答します。

歴史

この用語は、ベルトラン・マイヤーがEiffelプログラミング言語の設計に関連して作った造語で、1986年から様々な論文[ 1 ] [ 2 ] [ 3 ]や著書『オブジェクト指向ソフトウェア構築』の2版（1988年、1997年）で初めて説明されました。Eiffel Softwareは2003年12月にDesign by Contractの商標登録を申請し、2004年12月に認可されました。[ 4 ] [ 5 ]この商標の現在の所有者はEiffel Softwareです。[ 6 ] [ 7 ]

契約による設計は、形式検証、形式仕様、そしてホーア論理に関する研究に端を発しています。初期の貢献には以下のようなものがあります。

説明

DbCの中心的な考え方は、ソフトウェアシステムの要素が相互の義務と利益に基づいてどのように連携するかを示すメタファーです。このメタファーはビジネスシーンに由来しており、「クライアント」と「サプライヤー」が「契約」に合意し、例えば以下のようなことを定義しています。

  • サプライヤーは特定の製品を提供する義務（義務）があり、クライアントが料金（利益）を支払ったことを期待する権利があります。
  • 顧客は料金（義務）を支払う必要があり、製品（利益）を受け取る権利があります。
  • 両当事者は、すべての契約に適用される法律や規制などの特定の義務を満たす必要があります。

同様に、オブジェクト指向プログラミングのクラスのメソッドが特定の機能を提供する場合、次のようになります。

  • メソッドを呼び出すクライアント モジュールによって、エントリ時に特定の条件が保証されることを期待します。メソッドの前提条件は、クライアントにとっては義務であり、サプライヤ (メソッド自体) にとっては、前提条件外のケースを処理する必要がなくなるためメリットになります。
  • 終了時に特定のプロパティを保証します: メソッドの事後条件(サプライヤーにとっては義務であり、クライアントにとっては明らかに利点 (メソッドを呼び出す主な利点))。
  • 入口で想定され、出口で保証される特定のプロパティ（クラス不変量）を維持します。

この契約は、義務を形式化するホーア・トリプルと意味的に同等です。これは、設計者が契約の中で繰り返し答えなければならない「3つの質問」に要約できます。

  • 契約では何が期待されていますか?
  • 契約では何が保証されますか?
  • 契約では何が規定されますか?

多くのプログラミング言語には、このようなアサーションを行う機能が備わっています。しかし、DbCでは、これらの契約はソフトウェアの正当性にとって非常に重要であるため、設計プロセスの一部に組み込むべきだと考えています。実際、DbCは最初にアサーションを記述することを推奨しています。契約は、コードコメントで記述することも、テストスイートで強制することも、あるいはその両方で記述することも可能です。契約をサポートする特別な言語がない場合でも、この両方で 記述できます。

契約の概念はメソッド/手順レベルにまで拡張され、各メソッドの契約には通常、次の情報が含まれます。

  • 許容される入力値または型と許容されない入力値または型、およびその意味
  • 戻り値または型とその意味
  • 発生する可能性のあるエラーおよび例外条件の値または種類とその意味
  • 副作用
  • 前提条件
  • 事後条件
  • 不変量
  • （稀）パフォーマンス保証（例：時間や使用スペースなど）

継承階層内のサブクラスは、事前条件を弱める（強化することはできない）こと、および事後条件と不変条件を強化する（弱めることはできない）ことが許されています。これらの規則は、振る舞いに基づくサブタイプ化に近いものです。

すべてのクラス関係は、クライアントクラスとサプライヤクラスの間に存在します。クライアントクラスは、クライアントの呼び出しによってサプライヤの状態が侵害されないようなサプライヤ機能の呼び出しを行う義務があります。その後、サプライヤはクライアントの状態要件に違反しない状態とデータを返す義務があります。

例えば、サプライヤのデータバッファでは、削除機能が呼び出される際にバッファ内にデータが存在していることが求められる場合があります。その後、サプライヤはクライアントに対し、削除機能が処理を完了すると、データ項目がバッファから確実に削除されることを保証します。その他の設計規約として、クラス不変の概念があります。クラス不変は（ローカルクラスに対して）、各機能の実行終了時にクラスの状態が指定された許容範囲内に維持されることを保証します。

契約を使用する場合、サプライヤーは契約条件が満たされているかどうかを検証します。これは攻撃的プログラミングと呼ばれる手法です。一般的な考え方としては、コードは「確実に失敗」するべきであり、契約検証がセーフティ ネットとなるということです。

DbC の「フェイルハード」プロパティにより、各メソッドの意図された動作が明確に指定されるため、コントラクト動作のデバッグが簡素化されます。

このアプローチは、防御的プログラミングとは大きく異なります。防御的プログラミングでは、前提条件が破られた場合にどう対処するかはサプライヤー側の責任となります。多くの場合、サプライヤーはクライアントに前提条件が破られたことを通知するために例外をスローしますが、DbCでも防御的プログラミングでも、クライアント側はそれにどのように対応するかを考えなければなりません。このような場合、DbCはサプライヤー側の作業を容易にします。

契約による設計では、ソフトウェア モジュールの正確性の基準も定義されます。

  • サプライヤーがクライアントによって呼び出される前にクラスの不変条件と前提条件が真である場合、サービスが完了した後に不変条件と事後条件は真になります。
  • サプライヤーに電話する場合、ソフトウェア モジュールはサプライヤーの前提条件に違反してはなりません。

契約による設計は、各コード部分の契約が完全に文書化されているため、コードの再利用を容易にします。モジュールの契約は、そのモジュールの動作に関する ソフトウェアドキュメントの一種と見なすことができます。

契約による設計は次のようになります。[ 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 」（「最適化」の略）を付けて起動すると、Pythonコードジェネレーターはアサート用のバイトコードを出力しなくなります。 [ 11 ]

これにより、開発時に使用されるアサートの数と計算コストに関係なく、製品コードでのアサートの実行時のコストが実質的に排除されます。これは、そのような命令がコンパイラによって製品に含まれなくなるためです。

ソフトウェアテストとの関係

契約による設計は、ユニットテスト、統合テスト、システムテストといった通常のテスト戦略に取って代わるものではありません。むしろ、テストフェーズ中に、独立したテストと本番環境コードの両方で実行できる内部セルフテストによって外部テストを補完するものです。

内部セルフテストの利点は、クライアントが無効な結果を確認する前にエラーを検出できることです。これにより、より早期かつ具体的なエラー検出が可能になります。

アサーションの使用は、契約実装によって設計をテストする方法である テスト オラクルの一形式と考えることができます。

言語サポート

ネイティブサポートのある言語

ほとんどの DbC 機能をネイティブに実装する言語は次のとおりです。

さらに、 Common Lisp オブジェクト システムの標準メソッドの組み合わせには、、、などのメソッド修飾子があり:before、これらを使用すると、補助メソッドとしてコントラクトを記述し:afterたり:around、その他の用途に使用したりできます。

参照

注記

  1. ^マイヤー、ベルトラン：契約による設計、技術レポート TR-EI-12/CO、インタラクティブソフトウェアエンジニアリング社、1986年
  2. ^マイヤー、ベルトラン：「契約による設計」、オブジェクト指向ソフトウェア工学の進歩、D.マンドリオリとB.マイヤー編、プレンティス・ホール、1991年、1～50頁
  3. ^マイヤー、ベルトラン：「契約による設計の適用」、 Computer（IEEE）、25、10、1992年10月、pp.40-51。
  4. ^ 「米国特許商標庁による「契約によるデザイン」の登録」. 2016年12月21日時点のオリジナルよりアーカイブ。2009年6月22日閲覧。
  5. ^ 「米国特許商標庁による「契約によるデザイン」という文字を含むグラフィックデザインの登録」. 2016年12月21日時点のオリジナルよりアーカイブ。2009年6月22日閲覧。
  6. ^ 「商標ステータスと文書検索 - 78342277」 USPTO商標出願および登録検索。
  7. ^ 「商標ステータスと文書検索 - 78342308」。USPTO商標出願および登録検索。
  8. ^ Joshua Berne、Timur Doumler、Andrzej Krzemieński (2025 年 2 月 13 日)。「C++ の契約」(PDF)。open-std.org。 WG22。{{cite web}}: CS1 maint: 複数の名前: 著者リスト (リンク)
  9. ^ 「コントラクトアサーション（C++26以降）」 . cppreference.com . cppreference . 2025年11月9日閲覧。
  10. ^ 「マネージコードにおけるアサーション」。Microsoft Developer Network。2016年11月15日。2018年8月22日時点のオリジナルよりアーカイブ。
  11. ^公式 Python ドキュメント、assert ステートメント
  12. ^ Bright, Walter (2014年11月1日). 「Dプログラミング言語、契約プログラミング」 . Digital Mars . 2014年11月10日閲覧。
  13. ^ Hodges, Nick. 「Delphi Prismのクラスコントラクトを使用して、よりクリーンで高品質なコードを記述する」エンバカデロ・テクノロジーズ. 2021年4月26日時点のオリジナルよりアーカイブ。 2016年1月20日閲覧。
  14. ^ Findler, Felleisen高階関数の契約
  15. ^ 「Scala標準ライブラリドキュメント - アサーション」 . EPFL . 2019年5月24日閲覧。
  16. ^ Scala におけるもう 1 つの「契約の強制」としての強力な型付けについては、 scala-lang.org/での議論を参照してください。

参考文献

  • ミッチェル、リチャード、マッキム、ジム：契約によるデザイン：例による、アディソン・ウェスレー、2002
  • DBC を元のモデルに忠実に解説したウィキブック。
  • McNeile, Ashley:行動契約の意味論のためのフレームワーク. 第2回国際行動モデリングワークショップ：基礎と応用 (BM-FA '10) 議事録 . ACM, ニューヨーク, ニューヨーク州, 米国, 2010. この論文では、契約と代替可能性の一般化された概念について論じています。
「 https://en.wikipedia.org/w/index.php?title=Design_by_contract&oldid=1330547870」より取得