契約プログラミング

契約プログラミング（けいやくプログラミング、英: Contract programming）または契約による設計（けいやくによるせっけい、英: Design by Contract; DbC）は、ソフトウェアの正確性^{[注 1]}と頑健性^{[注 2]}を高めるためのソフトウェア設計の方法論である。DbC はロバート・フロイド、アントニー・ホーア、エドガー・ダイクストラらの形式的検証の仕事を基礎にしている^[1]。DbC は（抽象データ型に基づく）オブジェクト指向プログラミングにおける表明の利用や、継承に伴う表明の再定義の原理的規則、例外処理の原理的規則などを提供する^[2]。

DbC は、バートランド・メイヤーによって提案された^[3]^[4]^[5]。

概要編集

「契約による設計」（DbC）における中心的な概念は、クライアントとサプライヤ^[6]の契約 (contract) である。DbC における契約とは、クラス^[7]のインスタンス^{[注 3]}とそのメソッド^{[注 4]} の利用に関する条件を形式的に表明したものであり、クラス不変条件とメソッドの事前条件および事後条件で構成される。

不変条件、事前条件、事後条件はそれぞれ、クラスの振る舞いを定義するものであり、クライアントに対して公開された（コンストラクタを含む）メソッドに対して適用される。

契約はまたクライアントとサプライヤに生じる義務と利益によって特徴付けられる。クライアントの設計者にはクラスのインタフェースとして示された事前条件を遵守する義務が生じる一方、事後条件が満たされること期待してよく、反対にサプライヤの設計者はクライアントが事前条件を満たしてクラスを利用することを期待してよい一方、事後条件を遵守する義務が生じる。このクライアントとサプライヤの双方に生じる義務と、義務を守った際に保証された状態を得られる利益とが現れる点で、プログラミングにおける「契約」と一般的な意味での契約の類似を見出せる。

表明を予め記述しておくことで、実装者はその表明に従ってプログラムを記述することができる。一般に表明は静的な記述であり、必ずしもプログラム動作時に意味を持つものではないが、DbC をサポートするプログラミング言語では、プログラム実行時に表明を違反していないか監視することができる^[8]。実行時の表明違反の監視に関連して、例外機構を利用することにより、実行時の表明違反を例外としてクライアントに処理させることができる。

クラス A が、クラス B に関するエンティティ（ローカル変数の定義やメソッド呼び出し）の記述を含む場合、B は A に対するサプライヤ、A は B に対するクライアントとなる。クライアントとサプライヤは同一クラスであってもよく、例えば this を介したメソッド呼び出しが相当する。

事前条件編集

事前条件 (precondition) は、メソッド開始時に保証されるべき条件の表明である^[9]。事前条件はメソッドごとに定義され、以下に関する制約を与える：

メソッドの引数
メソッド開始時のサプライヤクラスのインスタンスの状態

メソッド引数に関する事前条件の例として、配列の要素を添字から参照する際、クライアントは指定した添字が配列の範囲に含まれることを保証する必要があることが挙げられる。

インスタンスの状態に関する事前条件の例として、スタックから要素を取り出す操作（pop）に関して、クライアントは対象のスタックが空でないことを保証する必要があることが挙げられる（スタックが空の場合に何らかの値を返すことを認めない場合）。

事前条件をクライアントとサプライヤの間の契約と見なせば、事前条件を満たすことはクライアントの義務に相当し、事前条件が満たされている前提でメソッド本体を設計できることはサプライヤが受ける利益に相当する^[10]。またクライアントに事前条件を提示することは、クライアントとサプライヤの間で責任の所在がどちらにあるのかを明らかにすることつながる^[11]。事前条件に対する検査をクライアントが行うよう責任分担することで、サプライヤ側で冗長な検査を行うことや、逆に全く検査が行われないことを避けることができる^[12]。

事前条件は表明の一種であり、コンパイル時やプログラム実行時に検査することが可能である（詳細な仕様はプログラミング言語ごとに異なる）。

事後条件編集

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

メソッド開始時のサプライヤクラスのインスタンスの状態
メソッド正常終了時のサプライヤクラスのインスタンスの状態
クライアントに渡す返り値

事後条件を満たすことはサプライヤの義務になり、もし満たされた場合は事前に決められた状態遷移が果たされて、これはクライアントの利益になる。クライアントは事後条件への作業から解放される。

不変条件編集

クラス不変条件^{[注 5]} (class invariant) は、クラスが持つ公開^{[注 6]}された各メソッドの開始時と正常終了時に共通して保証されるべき状態についての条件である^[13]。ただしコンストラクタ^{[注 7]}の呼び出しに関しては、事後条件としてのみ適用され事前条件として保証する必要はない^[13]。（引数や返り値などを制約するメソッド個別の事前/事後条件と異なり）不変条件はインスタンスの状態にのみに対する表明である^[14]。インスタンスの「状態」はそのインスタンスのすべてフィールドの値によって決まるため、より具体的には、不変条件はフィールドの値に関する表明となる^[14]。

不変条件は公開メソッドの事前条件および事後条件として暗黙的に追加される^[14]。不変条件を持つクラスに関して、そのクラスの公開メソッドの呼び出しの際、クライアントはメソッドの事前条件とサプライヤ・クラスの不変条件の両方を満たす義務がある。またサプライヤは、事前条件（と不変条件）を満たしたメソッド呼び出しに対して、メソッド終了時にそのメソッドの事後条件と不変条件の両方を満たす義務がある。

義務と利益編集

「契約による設計」（DbC）において、クライアントとサプライヤに課されるメソッド呼び出しの事前条件および事後条件は、クライアントとサプライヤとの間の契約に喩えられる^[15]。一般の契約と同様に DbC における契約は、クライアントとサプライヤの遵守すべき義務 (obligation) と義務を遵守することで得られる利益 (benefit) を記述したものと捉えられる^[15]。

クライアントの義務と利益は^[15]：

クライアントの義務：メソッド呼び出し時に事前条件を満たすこと
クライアントの利益：メソッド終了時に事後条件を満たした状態が得られること

一方、サプライヤの義務と利益は^[15]：

サプライヤの義務：メソッド終了時に事後条件を満たすこと
サプライヤの利益：事前条件を満たした状態でメソッドが呼び出されること

である。サプライヤは事前条件を満たすことをクライアントに課すことで、メソッド本体に冗長な検査を記述することを避けられる^[12]。

契約における例外の扱い編集

メソッドの表明違反（事前条件、事後条件、不変条件のいずれかを満たさない状況）が生じた際や、OSが異常を検出した際には、それらを例外として処理しなければならない^[16]。

例外処理はメソッドを失敗させるか成功させるかいずれかの形で行わなれなければならない^[16]。

メソッドを成功させる場合、定義より、不変条件を含むメソッドの事後条件を満たして呼び出し元に制御を返す必要がある。

失敗させる場合、システムの状態をメソッド実行前の状態に戻し、クライアントへ例外の発生を伝えなければならない。例えばデータベース（DB）のトランザクションでエラーが生じた場合、サプライヤはトランザクションを巻き戻した上で DB 操作の失敗をクライアントに伝える必要がある。

メソッド内で定義された例外ハンドラでは、メソッド本体の実行を再開するか、クライアントへ例外を通知して終了するかのいずれかを行う。例外ハンドラからクライアントへ制御を戻す場合、クラスの不変条件に違反してはならない^[17]。

契約プログラミングにおいて、形式的には、数値計算におけるオーバーフローやゼロ除算や、メモリ領域の確保失敗、ファイルへのアクセスや書き込みの失敗などは、システムとクライアントとの間の暗黙の契約違反と見なせる^[18]。

契約の継承編集

クラスをモジュールと見た場合、クラスは開放/閉鎖原則にしたがって設計されるべきである。すなわち、クラスのインタフェースの仕様が安定していて、クライアントから見た振る舞いが変わらないようにしなければならない一方で、将来的な機能の追加や仕様の変更を受け入れられなければならない。後者のモジュールの開放性を実現するための方法の一つとして、クラスの継承がある^[19]。

「契約による設計」（DbC）では、クラスのインスタンスの抽象的な振る舞い (behaviour) を不変条件と各メソッドの事前条件および事後条件として定義する^{[注 8]}。DbC に従ってプログラミングする際、クライアントは、事前条件を満たせば事後条件を満たす状態が得られること期待して、サプライヤクラスのエンティティを記述することになる。一方で、ポリモーフィズム（多相性）のため、クライアントが記述したサプライヤクラスそれ自身が常に実装を提供するとは限らず、プログラム実行時には動的束縛されたサブクラス^{[注 9]}のインスタンスの実装が利用され得る^[20]。

サブクラスのインスタンスの振る舞いは前述の通りサブクラス自身の不変条件および各メソッドの事前条件と事後条件によって定義されるが、一方でサブクラスのインスタンスはクライアントと継承元のスーパークラス^{[注 10]}の契約に拘束され、スーパークラスのインスタンスとしても振る舞えなければならない（リスコフの置換原則）。したがって、クライアントと継承元のスーパークラスの間の契約を実現するため、サブクラスはスーパークラスの不変条件を常に満たさなければならず（したがってサブクラスの不変条件は自身の不変条件とすべてのスーパークラスの不変条件の論理積となる）^[21]、またサブクラスの事前条件はスーパークラスの事前条件より弱く（または等しく）^[21]、サブクラスの事後条件はスーパークラスの事後条件より強く（または等しく）なければならない^[21]。

ここで、「条件 $A$ が条件 $B$ より強い」とは、 $A$ が成り立つなら $B$ も必ず成り立ち、逆は成り立たないことを言う^[21]。例えば、実数 $x$ に対して $x > 2$ が成り立つなら常に $x > 0$ が成り立つが、逆は成り立たない。この場合、実数 $x$ に対する条件 $x > 2$ は条件 $x > 0$ より強い、と言える。他方「条件 $A$ が条件 $B$ より弱い」とは、 $B$ が $A$ より強いことを指す^[21]。