契約による設計

契約による設計( 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 の中心的な考え方は、ソフトウェア システムの要素が相互の義務と利益に基づいてどのように連携するかについての比喩です。この比喩はビジネスの世界から来ており、「クライアント」と「サプライヤー」が「契約」に合意して、たとえば次のような定義を行います。

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

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

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

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

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

多くのプログラミング言語には、このようなアサーションを行う機能があります。しかし、DbC では、これらの契約はソフトウェアの正確性にとって非常に重要であるため、設計プロセスの一部にする必要があると考えています。実際、DbC では最初にアサーションを記述することを推奨しています。^{[要出典]契約は、}コード コメントで記述することも、テスト スイートで強制することも、その両方で行うこともできます。契約に対する特別な言語サポートがない場合でも同様です。

契約の概念は方法/手順レベルにまで及びます。各方法の契約には通常、以下の情報が含まれます。^{[引用が必要]}

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

継承階層内のサブクラスは、前提条件を弱める（強化することはできない）ことと、事後条件と不変条件を強化する（弱めることはできない）ことが許可されています。これらのルールは、動作サブタイプ化に近似しています。

すべてのクラス関係は、クライアント クラスとサプライヤ クラスの間にあります。クライアント クラスは、サプライヤの機能を呼び出す義務があり、その呼び出しによってサプライヤの状態がクライアントの呼び出しによって違反されることはありません。その後、サプライヤは、クライアントの状態要件に違反しない戻り状態とデータを提供する義務があります。

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

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

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

このアプローチは、防御的プログラミングのアプローチとは大きく異なります。防御的プログラミングでは、前提条件が破られた場合にどうするかをサプライヤーが判断する責任があります。多くの場合、サプライヤーは例外をスローして、前提条件が破られたことをクライアントに通知します。DbC と防御的プログラミングの両方のケースで、クライアントはそれにどのように対応するかを判断する必要があります。このような場合、DbC によってサプライヤーの仕事が楽になります。

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

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

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

バグのないプログラムの実行中に契約条件に違反することは決してありません。したがって、契約は通常、ソフトウェア開発中のデバッグ モードでのみチェックされます。リリース時には、パフォーマンスを最大化するために契約チェックは無効になります。

多くのプログラミング言語では、契約はassertで実装されています。C/C++では、リリースモードではデフォルトでアサートがコンパイルされ、C# ^[8]やJavaでも同様に非アクティブ化されています。

Pythonインタープリターを引数として「-O」（「最適化」の略）で起動すると、Pythonコードジェネレーターはアサート用のバイトコードを生成しなくなります。^[9]

これにより、開発時に使用されるアサートの数や計算コストに関係なく、コンパイラによって本番環境にそのような命令が組み込まれなくなるため、本番環境コードでのアサートの実行時コストが効果的に排除されます。

契約による設計は、ユニット テスト、統合テスト、システム テストなどの通常のテスト戦略に代わるものではありません。むしろ、テスト フェーズ中に分離されたテストと実稼働コードの両方でアクティブ化できる内部セルフテストによって外部テストを補完します。

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

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

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

• エイダ 2012
• チャオ
• クロージュア
• コブラ
• ド^[10]
• ダフニー
• エッフェル
• 要塞
• コトリン
• 水銀
• オキシジェン（旧称ChromeおよびDelphi Prism ^[11]）
• 詐欺（高次の契約を含み、契約違反は加害者を責めなければならず、正確な説明が必要であることを強調する^[12]）
• サザー
• スカラ座^{[13] [14]}
• SPARK ( Adaプログラムの静的解析経由)
• ヴァラ
• ＶＤＭ

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

• コンポーネントベースのソフトウェアエンジニアリング
• 正確性（コンピュータサイエンス）
• 防御プログラミング
• フェイルファストシステム
• 形式手法
• ホーア論理
• モジュールプログラミング
• プログラムの導出
• プログラムの改良
• 強力な型付け
• テスト駆動開発
• 型状態分析

• 契約による設計の力(TM) DbC のトップレベルの説明と、追加リソースへのリンク。
• バグのない OO ソフトウェアの構築: Design by Contract(TM) の紹介 DbC に関する古い資料。
• 利点と欠点、RPS-Obix での実装
• より安全なコードのためのコード契約の使用