契約プログラミング

契約による設計

契約プログラミング（けいやくプログラミング、英: Contract programming）または契約による設計（けいやくによるせっけい、英: Design by Contract; DbC）は、オブジェクト指向に基づくソフトウェア設計のための方法論である。

ソースコードに、入力の検証（validation）と出力への表明（assertion）とオブジェクトの不変条件（invariant）などを定義した仕様書式を導入して、各モジュールの特にバグ発生に対する責任の所在を明瞭にし、設計の安全性を高めることを目的にしている。DbC においてソフトウェア設計者は、形式的仕様を定義しつつ、抽象データ型に準拠したソフトウェアコンポーネントを構築することが求められる。その仕様が契約（contract）と称されている。

DbC はバートランド・メイヤーにより提唱された。プログラミング言語 Eiffel は、DbC に基づいた言語機能を備えている。

概要

契約による設計（DbC）における中心的な概念は、クライアントとサプライヤの契約 (contract) である。DbC における契約とは、クラスのインスタンスとそのメソッド を制約するための事前条件、事後条件、不変表明などで構成されるものであり、それらはプログラム的にはいわゆる表明（assertion）の集合体になるが、コンセプト的にはそれとイコールではないとされる。入力に対する表明を満たすためのプロセスは義務（oblication）と称され、出力に対する表明が満たされた状態遷移は利益（benefit）と称されている。

表明を予め記述しておくことで、実装者はその表明に従ってプログラムを記述することができる。また、プログラム実行時に表明を違反していないか監視することができる。実行時の表明違反の監視に関連して、例外機構を利用することにより、実行時の表明違反を例外としてクライアントに処理させることができる。

Aインスタンスが、Bインスタンスのメソッドを呼び出す場合、Aはクライアントになり、Bはサプライヤになる。クライアントとサプライヤは同一インスタンスであってもよく、例えば暗黙のThisメソッド呼び出しではそれになる。クライアントが任意のサプライヤのメソッドを呼び出した時に契約が照会される。契約は以下の項目からなる。

事前条件

事前条件 (precondition) は、メソッド開始時に保証されるべき状態の表明である。これはメソッド単位で表明される。具体的には以下になる。

1. クライアントがメソッドに渡すパラメータ値の有効範囲。
2. そのメソッドに関連したサプライヤ・インスタンスの特定フィールドの適正範囲。

事前条件を満たすことは、呼び出し側であるクライアントの責任となる。そうすることで、サプライヤはメソッドの実装部分（本体）で事前条件に違反している状況を考慮する必要がなくなる。

事後条件

事後条件 (postcondition) は、メソッド正常終了時に保証されるべき状態の表明である。これはメソッド単位で表明される。正常終了とは例外スロー終了やエラー発生終了ではない終了を指す。具体的には以下になる。

1. 渡されたパラメータ値に関連したサプライヤ・インスタンスの特定フィールドの適正範囲。
2. クライアントに渡すリターン値の有効範囲。

事後条件を満たすことは、呼び出された側であるサプライヤの責任となる。そうすることで、クライアントは呼び出したメソッドの実装部分（本体）で事後条件に違反している状況を考慮する必要がなくなる。

不変表明

クラス不変表明 (class invariant) は、各メソッドの開始時と正常終了時に共通して保証されるべき状態の表明である。これはクラス単位で表明される。不変表明は、creation用メソッド（コンストラクタと同義）の開始時には照会されない。具体的には以下になる。

1. サプライヤ・インスタンスの各フィールドの適正範囲。

事前条件 AND 不変表明が真であった後に、事後条件 AND 不変表明も真であったならば、メソッド呼び出しによる契約は全うされたことになる。

義務と利益

契約でのクライアントとサプライヤの、プロセス（process）およびステート（state）は、それぞれの義務と利益に例えられている。

• クライアントの義務：サプライヤ・インスタンスのフィールド値の審査と、有効なパラメータ値を渡すこと。これは事前条件を満たすプロセスとされる。
• サプライヤの義務　：メソッドの決められた働きと、正常終了時に決められた状態遷移を果たすこと。これは仮想メソッド向けであり、後述の契約の派生でのサプライヤ・サブクラスの実装メソッド向けと考えると分かりやすい。これは事後条件を満たすプロセスとされる。
• クライアントの利益：メソッド正常終了時の決められた状態遷移と、あるならばリターン値を受け取ること。これは事後条件からのステートとされる。
• サプライヤの利益　：必要なサプライヤ・インスタンスのフィールド値が不適正か、渡されるパラメータ値が無効ならば、メソッドを実行しなくてよいこと。これは事前条件からのステートとされる。

例外

契約の主要な目的は、各メソッドの実行（例外可能性）実行中止（例外未発生）正常終了（例外可能性）異常終了（例外スローとエラー発生）を特定して、バグ責任の所在を明らかにすることである。そこでは例外（exception）の操作が重視されている。正常終了には、途中の例外発生とその解決継続も含まれていることに注意する。無効なパラメータ値やフィールド値の不適正によるメソッドの実行中止は、同時に例外も未発生と解釈されることに注意する。 やや分かり難いサプライヤの利益の「メソッド未実行＝その時その範囲での例外未発生」は有効な責任特定材料になる。例外が解決できなかったら異常終了になる。異常終了は最も容易な責任特定材料になる。正常終了には例外発生の解決継続も含まれるのでやや複雑になる。例えば契約の入れ子で、内側契約の例外が外側契約で解決されていた場合などは見落とされがちなので要注意になる。

契約の派生

契約による設計ではクラスの継承がフォローされている。適切な継承は、スーパークラスの契約を保持しながら、そのサブクラスによる柔軟なパフォーマンスをもたらせる。スーパークラスの契約に対するそのサブクラスの適用は、動的バインディングと同義になる。これは開放閉鎖の原則に沿っている。

スーパークラスの契約と、そのサブクラスの契約の間には明確な整合性が要求される。サブクラスの契約の改変許容範囲は、以下のように定められており、この法則はbehavioral subtypingとも言われる。それに沿って派生された契約下のサブクラス・インスタンスは、スーパークラスの契約下でも安全に用いることが出来るとされる。

1. 事前条件は、サブクラスで弱める（weaken）ことはできるが、強めることはできない。
2. 事後条件は、サブクラスで強める（strengthen）ことはできるが、弱めることはできない。
3. 不変条件は、サブクラスでもそのまま維持されなければならない。
4. スーパークラスの例外から派生した例外を除いては、サブクラスで独自の例外を投げてはならない。

事前条件の弱めるは様々な意味を持つが、一例としてはパラメータ型の汎化である。事後条件の強めるも様々な意味を持つが、一例としてはリターン型の特化である。

メイヤーのオブジェクト指向入門

1988年第1版と1997年第2版の『Object-Oriented Software Construction- OOSC』は『オブジェクト指向入門』の邦題で知られているが、直訳すれば「オブジェクト指向ソフトウェア構築」である。入門というのはおそらく販売促進用の題名と考えた方が無難である。

OOSCのオブジェクト指向は、継承が有望視されていた古き良き時代のオブジェクト指向であることにも留意する必要がある。OOSCの継承は、実装継承による改訂モジュールの情報隠蔽と動的束縛を要点にしている。これは後年のSOLIDなどの界面継承による機能抽象インターフェースの動的ポリモーフィズムを要点にしたものとは異なっている。OOSCの開放/閉鎖原則と、2000年代に聞かれる開放/閉鎖原則の性格も異なるものである。

契約による設計の思想は、リファクタリング、テスト駆動開発、アジャイルソフトウェア開発などの対極的な位置にあることもそうである。

契約による設計のサポート言語

• Eiffel
• Ada
• D言語
• Spec#（C#のDbC拡張版）
• Kotlin
• Clojure

参考文献

• Meyer, Bertrand『オブジェクト指向入門』酒匂, 寛（訳）; 酒匂, 順子（訳）; 二木, 厚吉（監訳）、アスキー出版局、1990年11月21日（原著1988年）。ISBN 4-7561-0050-3。