「契約プログラミング」の版間の差分
→概要: 契約の項目 {{要出典 数点 |
全くの間違いと言っている方が間違っているので訂正。義務と利益については出典を確認されたし。 タグ: 差し戻し済み ビジュアルエディター: 中途切替 |
||
| 7行目: | 7行目: | ||
==概要== |
==概要== |
||
[[アラン・ケイ]]由来の[[オブジェクト指向プログラミング]]の理念は、[[オブジェクト (プログラミング)|オブジェクト]]のコミュニケーションとされている。それをクライアントとサプライヤの契約（contract）であるべきとした |
[[アラン・ケイ]]由来の[[オブジェクト指向プログラミング]]の理念は、[[オブジェクト (プログラミング)|オブジェクト]]のコミュニケーションとされている。それを[[バートランド・メイヤー|メイヤー]]は、クライアントとサプライヤの契約（contract）であるべきとした。契約とは具体的には[[クラス (コンピュータ)|クラス]]の仕様（specification）になる。オブジェクト間の呼び出しにおいて、呼ぶ側はクライアントの立場、呼ばれる側はサプライヤの立場になる。[[This (プログラミング)|This]]メソッド呼出しでは、クライアントとサプライヤは同一オブジェクトになる。 |
||
プログラムでは、クライアントがサプライヤの[[メソッド (計算機科学)|メソッド]]を呼び出した時に、そのサプライヤのクラスの契約が照会されることになる。契約は以下の項目からなる。 |
プログラムでは、クライアントがサプライヤの[[メソッド (計算機科学)|メソッド]]を呼び出した時に、そのサプライヤのクラスの契約が照会されることになる。契約の目的は、各メソッドの実行（例外可能性）未実行（例外未発生）正常終了（例外可能性）異常終了（エラー発生）を特定して、バグ責任の所在を明らかにすることである。そこでは例外の取り扱いが重視されている。契約は以下の項目からなる。 |
||
'''事前条件'''（precondition） |
|||
:事前条件とは、サプライヤがメソッドを正しく実装していることと、クライアントがメソッドを正しく実行することを保証する。メソッド実行、正常終了、例外発生の各論理値が用意される。両者に事前条件を全うする義務（obligation）が課される<ref name=":0">{{Cite web|title=ET: Design by Contract (tm), Assertions and Exceptions|url=https://www.eiffel.org/doc/eiffel/ET-_Design_by_Contract_%28tm%29%2C_Assertions_and_Exceptions|website=www.eiffel.org|date=2021-01|accessdate=2021-1}}</ref>。 |
|||
#*クライアントの義務：メソッド開始に必要な事前条件を保証し、あるならば渡すパラメータ値の正当性を保証する。 |
|||
:* クライアントの義務<ref name=":0" />：メソッドの開始と、あるならば正当なパラメータ値を渡すこと。 |
|||
:* サプライヤの義務<ref name=":0" /> ：メソッドの決められた働きと、メソッド終了時に決められた状態遷移を果たすこと。 |
|||
| ⚫ | |||
| ⚫ | |||
| ⚫ | |||
#*サプライヤの義務 ：メソッド終了で事後条件を満たすことを保証し、その働きと効用を保証する。 |
|||
#* サプライヤが保証していた事後条件の完遂を確認し、あるならば取得するリターン値を確認する。<!-- ←「クライアントが確認する」に見えるとおかしい。（条件を確認するのは 言語システムや検証ツール）--> |
|||
#パラメータ型 {{要出典|date=2021年11月}} |
|||
#リターン型 {{要出典|date=2021年11月}} |
|||
#エラー型と例外型 {{要出典|date=2021年11月}} - この発生はメソッドの中断による契約の破棄を意味する。 |
|||
#[[副作用 (プログラム)|副作用]] {{要出典|date=2021年11月}} |
|||
| ⚫ | |||
| ⚫ | |||
| ⚫ | |||
| ⚫ | |||
| ⚫ | |||
:事後条件とは、メソッドが実行されたことと、メソッドが正常終了して決められた状態遷移を果たしたことを保証する。正常終了には、途中の例外発生とその解決継続も含まれていることに注意する。クライアントの不正パラメータによるメソッド未実行は、例外も未発生と解釈されることに注意する。メソッド実行、正常終了、例外発生の各論理値が確定される。両者に事後条件からの利益（benefit）が出される<ref name=":0" />。 |
|||
:* クライアントの利益<ref name=":0" />：決められた状態遷移と、あるならばリターン値を受け取ること。メソッド実行は真に、正常終了は真になる。 |
|||
:* サプライヤの利益<ref name=":0" /> ：パラメータ値が不正ならば、メソッドを実行しなくてよいこと。メソッド実行は偽に、例外発生は偽になる。 |
|||
'''その他''' |
|||
:例外型、エラー型、パラメータ型、リターン型、[[副作用 (プログラム)|副作用]]などは、契約の注釈として扱われることがある。 |
|||
やや分かり難いサプライヤの利益の「メソッド未実行＝そこでの確実な例外未発生」は責任特定要素になる。異常終了は最も容易な責任特定要素になる。正常終了には例外発生の解決継続も含まれるのでやや複雑になる。例えば契約の入れ子で内側契約の例外が外側契約で解決されていた場合などは見落とされがちなので要注意になる。 |
|||
| ⚫ | |||
| ⚫ | |||
=== 契約の派生 === |
=== 契約の派生 === |
||
2021年11月11日 (木) 06:06時点における版
契約による設計（Design by Contract、DbC）は、契約プログラミング（Contract programming）などとも呼ばれている、ソフトウェア設計のための方法論である。1990年代の主要なオブジェクト指向方法論であり、DbCと略称されている。ソースコードに、外部作用の検証（validation）および内部作用の条件（condition）を形式的に表明（declaration）した仕様記述（specification）を導入して各モジュールの責務（responsibility）の所在を明らかにし、設計の安全性を高めることを目的にしている。
DbCでのソフトウェア設計者は、形式的仕様を定義して、主に抽象データ型に沿ったソフトウェアコンポーネントを構築することが求められている。仕様とは、クライアント・コンポーネントとサプライヤ・コンポーネントの義務および利益における事前条件・事後条件・不変条件などを定義しているインターフェース書式である。これをビジネスの契約書に見立てている。
1988年のバートランド・メイヤーの著書『邦題：オブジェクト指向入門』で提唱され、オブジェクト指向言語「Eiffel」は、DbCに沿った言語機能を備えている[1][2][3]。
概要
アラン・ケイ由来のオブジェクト指向プログラミングの理念は、オブジェクトのコミュニケーションとされている。それをメイヤーは、クライアントとサプライヤの契約（contract）であるべきとした。契約とは具体的にはクラスの仕様（specification）になる。オブジェクト間の呼び出しにおいて、呼ぶ側はクライアントの立場、呼ばれる側はサプライヤの立場になる。Thisメソッド呼出しでは、クライアントとサプライヤは同一オブジェクトになる。
プログラムでは、クライアントがサプライヤのメソッドを呼び出した時に、そのサプライヤのクラスの契約が照会されることになる。契約の目的は、各メソッドの実行（例外可能性）未実行（例外未発生）正常終了（例外可能性）異常終了（エラー発生）を特定して、バグ責任の所在を明らかにすることである。そこでは例外の取り扱いが重視されている。契約は以下の項目からなる。
事前条件（precondition）
- 事前条件とは、サプライヤがメソッドを正しく実装していることと、クライアントがメソッドを正しく実行することを保証する。メソッド実行、正常終了、例外発生の各論理値が用意される。両者に事前条件を全うする義務（obligation）が課される[4]。
クラス不変条件（class invariants）
- オブジェクトの生成破棄間で維持されるべき状態。言語では個別条件と照応状態のペアで定義されることが多い。これは各メソッドの開始時と終了時に照会される。
事後条件（postcondition）
- 事後条件とは、メソッドが実行されたことと、メソッドが正常終了して決められた状態遷移を果たしたことを保証する。正常終了には、途中の例外発生とその解決継続も含まれていることに注意する。クライアントの不正パラメータによるメソッド未実行は、例外も未発生と解釈されることに注意する。メソッド実行、正常終了、例外発生の各論理値が確定される。両者に事後条件からの利益（benefit）が出される[4]。
その他
- 例外型、エラー型、パラメータ型、リターン型、副作用などは、契約の注釈として扱われることがある。
やや分かり難いサプライヤの利益の「メソッド未実行＝そこでの確実な例外未発生」は責任特定要素になる。異常終了は最も容易な責任特定要素になる。正常終了には例外発生の解決継続も含まれるのでやや複雑になる。例えば契約の入れ子で内側契約の例外が外側契約で解決されていた場合などは見落とされがちなので要注意になる。
不変条件は好ましくない状態遷移を防止して、バグ責任特定とプログラムテストの助けになる。事前条件 AND 不変条件が真であった後に、事後条件 AND 不変条件も真であったならば、メソッド呼出しによる契約は全うされたことになる。
契約項目は、ホーア論理をモチーフにした専用の論理式の構成要素になることも想定されていたようで、これはプログラムの形式的検証に向けた試みでもあった。
契約の派生
契約による設計ではクラスの継承がフォローされている。適切な継承は、スーパークラスの契約を保持しながら、そのサブクラスによる柔軟なパフォーマンスをもたらせる。スーパークラスの契約に対するそのサブクラスの適用は、動的バインディングと同義になる。これは開放閉鎖の原則に沿っている。
スーパークラスの契約と、そのサブクラスの契約の間には明確な整合性が要求される。サブクラスの契約の改変許容範囲は、以下のように定められており、この法則はbehavioral subtypingとも言われる。それに沿って派生された契約下のサブクラス・インスタンスは、スーパークラスの契約下でも安全に用いることが出来るとされる。
- 事前条件（precondition）は、サブクラスで弱める（weaken）ことはできるが、強めることはできない。
- 事後条件（postcondition）は、サブクラスで強める（strengthen）ことはできるが、弱めることはできない。
- 不変条件（invariants）は、サブクラスでもそのまま維持されなければならない。
- スーパークラスの例外から派生した例外を除いては、サブクラスで独自の例外を投げてはならない。
事前条件の弱めるは様々な意味を持つが、一例としてはパラメータ型の汎化である。事後条件の強めるも様々な意味を持つが、一例としてはリターン型の特化である。
メイヤーのオブジェクト指向入門
1988年第1版と1997年第2版の『Object-Oriented Software Construction- OOSC』は『オブジェクト指向入門』の邦題で知られているが、直訳すれば「オブジェクト指向ソフトウェア構築」である。入門というのはおそらく販売促進用の題名と考えた方が無難である。
OOSCのオブジェクト指向は、継承が有望視されていた古き良き時代のオブジェクト指向であることにも留意する必要がある。OOSCの継承は、実装継承による改訂モジュールの情報隠蔽と動的束縛を要点にしている。これは後年のSOLIDなどの界面継承による機能抽象インターフェースの動的ポリモーフィズムを要点にしたものとは異なっている。OOSCの開放/閉鎖原則と、2000年代に聞かれる開放/閉鎖原則の性格も異なるものである。
契約による設計の思想は、リファクタリング、テスト駆動開発、アジャイルソフトウェア開発などの対極的な位置にあることもそうである。
契約による設計のサポート言語
脚注
- ^ 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
- ^ a b c d e f “ET: Design by Contract (tm), Assertions and Exceptions”. www.eiffel.org (2021年1月). 2021年1月閲覧。