コンテンツにスキップ

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

出典: フリー百科事典『ウィキペディア（Wikipedia）』
履歴の双方向閲覧
← 古い編集新しい編集 →
削除された内容 追加された内容
ビジュアルウィキテキスト
タグ: モバイル編集 モバイルウェブ編集 改良版モバイル編集
タグ: モバイル編集 モバイルウェブ編集 改良版モバイル編集
127行目: 127行目:
=== 契約の継承 ===
=== 契約の継承 ===


[[クラス (コンピュータ)|クラス]]をモジュールと見た場合、クラスは[[開放/閉鎖原則]]にしたがって設計されるべきである。すなわち、クラスのインタフェースの仕様が安定していて、クライアントから見た振る舞いが変わらないようにしなければならない一方で、将来的な機能の追加や仕様の変更を受け入れられなければならない。後者のモジュールの開放性を実現するための方法の一つとして、クラスの[[継承 (プログラミング)|継承]]がある{{sfn|Meyer|1990|p=307}}。
契約による設計では、[[開放/閉鎖原則|開放閉鎖の原則]]に沿った[[クラス (コンピュータ)|クラス]]の[[継承 (プログラミング)|継承]]がフォローされている。これは[[スーパークラス (計算機科学)|スーパークラス]]の契約を維持しながら、その[[サブクラス (計算機科学)|サブクラス]]による柔軟なパフォーマンスをもたらす。スーパークラスの契約に対するそのサブクラスの適用は、[[ダイナミックバインディング|動的バインディング]]と同義になる。


「契約による設計」（DbC）では、クラスのインスタンスの振る舞い（公理）を[[#不変条件|不変条件]]と各メソッドの[[#事前条件|事前条件]]および[[#事後条件|事後条件]]として記述する。DbC に従ってプログラミングする際、クライアントは、事前条件を満たせば事後条件を満たす状態が得られること期待して、サプライヤクラスのエンティティを記述することになる。一方で、[[ポリモーフィズム]]（多相性）のため、クライアントが記述したサプライヤクラスそれ自身が常に実装を提供するとは限らず、プログラム実行時には[[ダイナミックバインディング|動的束縛]]された[[サブクラス (計算機科学)|サブクラス]]<ref>{{harvnb|Meyer|1990|p=296}} ではクラス自身とそれを継承するサブクラスを'''子孫''' ({{en|descendant}}) と定義し、クラス自身を除いた子孫を'''真の子孫''' ({{en|proper descendant}}) と定義しているが、本項では特に断りない限り、真の子孫の意味で「サブクラス」を用いる。</ref>のインスタンスの実装が利用され得る{{sfn|Meyer|1990|p=305}}。
スーパークラスの契約に対するサブクラスの契約の修正許容範囲は、以下のように定められており、この法則はbehavioral subtypingとも言われる。それに従って派生された契約下のサブクラス・インスタンスは、スーパークラスの契約下でも[[型安全]]に用いることが出来る。


サブクラスのインスタンスの振る舞いはサブクラス自身の不変条件および各メソッドの事前条件と事後条件によって定義されるが、一方でサブクラスのインスタンスはクライアントと継承元の[[スーパークラス (計算機科学)|スーパークラス]]<ref>{{harvnb|Meyer|1990|p=296}} ではクラス自身とそれが継承しているスーパークラスを'''祖先''' ({{en|ancestor}}) と定義し、クラス自身を除いた祖先を'''真の祖先''' ({{en|proper ancestor}}) と定義しているが、本項では特に断りない限り、真の祖先の意味で「スーパークラス」を用いる。</ref>の契約に拘束され、スーパークラスのインスタンスとしても振る舞えなければならない。
# 事前条件は、サブクラスで弱める（weaken）ことはできるが、強めることはできない。
したがって、クライアントと継承元のスーパークラスの間の契約を実現するため、サブクラスはスーパークラスの不変条件を常に満たさなければならず（したがってサブクラスの不変条件は自身の不変条件とすべてのスーパークラスの不変条件の論理積となる）{{sfn|Meyer|1990|p=344}}、またサブクラスの事前条件はスーパークラスの事前条件より弱く（または等しく）{{sfn|Meyer|1990|p=344}}、サブクラスの事後条件はスーパークラスの事後条件より強く（または等しく）なければならない{{sfn|Meyer|1990|p=344}}。
# 事後条件は、サブクラスで強める（strengthen）ことはできるが、弱めることはできない。

# 不変条件は、サブクラスでもそのまま引き継いで維持する。
ここで、「条件 {{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}}。
# スーパークラスの例外から派生した例外を除いては、サブクラスで独自の例外を投げてはならない。
事前条件の弱めるは様々な意味を持つが、例としてはパラメータ型の汎化や、フィールド値の有効範囲を広くすることである。事後条件の強めるも様々な意味を持つが、例としてはリターン型の特化や、フィールド値の有効範囲を狭くすることである。


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

2021年12月23日 (木) 09:11時点における版

契約による設計

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

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

契約とは

DbCでの各モジュールに備えられる契約は、端的に言うとアサートの集合体である。ただし一般的なアサートのように、ただアヴォート中断するためのものではない。事前条件のアサート違反では、中止用デフォルト処理に繋げられてそこで例外スローされることもあり、事後条件のアサート違反では、その前後で例外スローされて例外解決処理に繋げられることもある。反対にアサート順守は、サプライヤを事前条件までの関心から分離し、クライアントを事後条件までの関心から分離する。不変条件のアサートは、各オブジェクトの適正状態維持を情報隠蔽して他から分離する。これらが契約の効用になる。

クライアント・オブジェクトが、サプライヤ・オブジェクトのルーチンを呼び出した時に、そのサプライヤ・モジュール上の契約が発生する。

（モジュール＝クラス、オブジェクト＝インスタンス、ルーチン＝メソッド、属性＝フィールド）

事前条件[8][9]

ルーチン開始時に保証されるコンディション。ルーチン別に定義される。専らrequire構文でアサーションが列挙される。

  1. ルーチンに渡すパラメータ値の保証範囲
  2. ルーチンに関連するサプライヤ・オブジェクトの各属性値の保証範囲

事前条件満了はクライアントの義務になる。クライアントがサプライヤの属性をチェックする。クライアントには有効なパラメータ値を渡せないランタイム状況もある。事前条件を満たせなかったら、中止用デフォルト処理になる。

事後条件[8][9]

ルーチン正常終了時に保証されるコンディション。ルーチン別に定義される。専らensure構文でアサーションが列挙される。

  1. ルーチンに渡されたパラメータ値に関連するサプライヤ・オブジェクトの各属性値の保証範囲
  2. ルーチンのリターン値の保証範囲

事後条件満了はサプライヤの義務になる。クライアントはあるならばリターン値を渡される。ルーチン内の例外発生をサプライヤが解決出来なかったら例外スローされて正常終了されず、事後条件も満たされない。その例外解決はクライアントに委ねられる。

不変条件[8][9]

全公開ルーチンの開始時と正常終了時に共通して保証されるオブジェクトの状態。モジュール別に定義される。creation用ルーチン（コンストラクタ）開始時はスルーされる。専らinvariant構文でアサーションが列挙される。

  1. モジュール・オブジェクトの各属性値の保証範囲。

事前条件 AND 不変条件が真の後に、事後条件 AND 不変条件も真ならば、そのルーチンの契約は全うされたことになる。

義務と利益[8][9]

  • クライアントの義務：ルーチン開始への事前条件を満たすこと
  • サプライヤの利益　：事前条件が満たされなかったらルーチン開始中止のデフォルト処理で済ませてよいこと
  • サプライヤの義務　：ルーチン正常終了時の事後条件を満たすこと
  • クライアントの利益：ルーチン正常終了時の事後条件が満たされてリターン値を得ること

契約の継承[8][9]

親モジュールを継承した子モジュールの契約には、親に対しての以下の制約がある。

  1. 事前条件は、子モジュールで弱めることはできるが、強めることはできない。
  2. 事後条件は、子モジュール強めることはできるが、弱めることはできない。
  3. 不変条件は、子モジュールでもそのまま引き継いで維持する。
  4. 親モジュールの例外を継承している例外を除いては、子モジュールで独自の例外を投げてはならない。

事前条件の弱めるは、パラメータ型の汎化や属性値の有効範囲を広くするなど様々である。事後条件の強めるは、リターン型の特化や属性値の有効範囲を狭くするなど様々である。

説明

「契約による設計」（DbC）における中心的な概念は、クライアントとサプライヤ[10]の契約 (contract) である。DbC における契約とは、クラス[11]のインスタンス[12]とそのメソッド[13] の利用に関する条件を形式的に表明したものであり、クラス不変条件とメソッドの事前条件および事後条件で構成される。これらの表明が一般的な表明と異なる点は、クライアントに対して公開されていることで、クライアントとサプライヤの両者に表明を遵守する義務が生じることである。

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

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

事前条件

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

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

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

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

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

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

事後条件

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

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

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

不変条件

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

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

義務と利益

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

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

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

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

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

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

契約における例外の扱い

契約の継承

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

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

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

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

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

出典

  1. ^ Meyer 1990, p. 4 において、ソフトウェアの正確さはソフトウェア製品が要求および仕様によって定義されたとおりに確実に仕事を行う能力と定義されている。
  2. ^ Meyer 1990, p. 5 において、ソフトウェアの頑健さは異常な状態においても機能するソフトウェアシステムの能力と定義されている。ここで「異常な状態」とは仕様によって示されていない状態を指す。
  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. ^ a b c d e “ET: Design by Contract (tm), Assertions and Exceptions”. www.eiffel.org (2021年1月21日). 2021年1月閲覧。
  9. ^ a b c d e “Object-Oriented Software Construction”. 2021年1月閲覧。
  10. ^ クライアント（顧客）とサプライヤ（供給者）の用法については例えば Meyer 1990, pp. 30, 101 を参照。邦訳では顧客/供給者が用いられているが本項ではクライアント/サプライヤを用いる。
  11. ^ DbC の文脈における「クラス」の定義は例えば Meyer 1990, p. 85 を参照。この定義ではクラスは静的な型として表現され、それ自体はオブジェクトと見なされない。また同書ではしばしばクラスを「モジュール」と表現する。Smalltalk の流れを汲むクラスの扱いに関しては例えば Meyer 1990, p. 138 を参照。
  12. ^ Meyer 1990 では基本的に「オブジェクト」の語を用い、あらわにインスタンスとは呼んでいない。クラスを型と見なす場合、クラスのインスタンス以外にオブジェクトは存在しないため (Meyer 1990, pp. 85, 139) 混用しても問題はないが、一般的な文脈を優先して本項ではインスタンスの語を用いる。
  13. ^ Meyer 1990 では「メソッド」の代わりに「ルーチン」を用いているが、本項ではより一般的な前者を用いる。「メソッド」は Smalltalk 由来の同義語として Meyer 1990, p. 589 に示されている。
  14. ^ Meyer 1990, pp. 196–199.
  15. ^ Meyer 1990, pp. 155, 157, 218.
  16. ^ Meyer 1990, pp. 159–160.
  17. ^ Meyer 1990, pp. 163–164.
  18. ^ a b Meyer 1990, p. 161.
  19. ^ Meyer 1990, p. 168 では「（クラス）不変表明」と呼んでいる。
  20. ^ Meyer 1990, pp. 113, 170, 273–274 では「エクスポート」と表現している。
  21. ^ a b Meyer 1990, p. 170.
  22. ^ Meyer 1990, pp. 103, 170 では「Create プロシージャ」と表現している。プロシージャの定義は Meyer, pp. 109–110 を参照。
  23. ^ a b c Meyer 1990, p. 171.
  24. ^ a b c d Meyer 1990, p. 159.
  25. ^ Meyer 1990, p. 307.
  26. ^ Meyer 1990, p. 296 ではクラス自身とそれを継承するサブクラスを子孫 (descendant) と定義し、クラス自身を除いた子孫を真の子孫 (proper descendant) と定義しているが、本項では特に断りない限り、真の子孫の意味で「サブクラス」を用いる。
  27. ^ Meyer 1990, p. 305.
  28. ^ Meyer 1990, p. 296 ではクラス自身とそれが継承しているスーパークラスを祖先 (ancestor) と定義し、クラス自身を除いた祖先を真の祖先 (proper ancestor) と定義しているが、本項では特に断りない限り、真の祖先の意味で「スーパークラス」を用いる。
  29. ^ 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日閲覧。
「https://ja.wikipedia.org/w/index.php?title=契約プログラミング&oldid=87153776」から取得