「契約プログラミング」の版間の差分
削除された内容 追加された内容
→概要: 契約の項目 {{要出典 数点 |
全くの間違いと言っている方が間違っているので訂正。義務と利益については出典を確認されたし。 タグ: 差し戻し済み ビジュアルエディター: 中途切替 |
||
7行目:
==概要==
[[アラン・ケイ]]由来の[[オブジェクト指向プログラミング]]の理念は、[[オブジェクト (プログラミング)|オブジェクト]]のコミュニケーションとされている。それを[[バートランド・メイヤー|メイヤー]]は、クライアントとサプライヤの契約（contract）であるべきとした
プログラムでは、クライアントがサプライヤの[[メソッド (計算機科学)|メソッド]]を呼び出した時に、そのサプライヤのクラスの契約が照会されることになる。契約の目的は、各メソッドの実行（例外可能性）未実行（例外未発生）正常終了（例外可能性）異常終了（エラー発生）を特定して、バグ責任の所在を明らかにすることである。そこでは例外の取り扱いが重視されている。契約は以下の項目からなる。
:事前条件とは、サプライヤがメソッドを正しく実装していることと、クライアントがメソッドを正しく実行することを保証する。メソッド実行、正常終了、例外発生の各論理値が用意される。両者に事前条件を全うする義務（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" /> ：メソッドの決められた働きと、メソッド終了時に決められた状態遷移を果たすこと。
# '''クラス[[不変条件]]'''（class invariants）▼
#* オブジェクトで<!--常時 ←メソッドの途中では不成立でもいいので語弊あり-->維持されるべき、状態についての条件。個別条件とその対照状態のペアで定義される{{要出典|date=2021年11月}}。これは各メソッドの開始時と終了時に照会されることになる。▼
# '''事後条件'''（postcondition）▼
不変条件は好ましくない状態遷移を抑止し、事前条件、事後条件と合わせてプログラムのテスト精度を高める。<code>事前条件 AND 不変条件</code>が真であった後に、<code>事後条件 AND 不変条件</code>も真であったならば、メソッド呼出しによる契約は全うされたことになる。例外の操作も重視されており、プログラムの堅牢性を高める。▼
▲
上記の項目は、[[ホーア論理]]をモチーフにした専用の論理式の構成要素になることも想定されていたようで、これはプログラムの[[形式的検証]]に向けた試みでもあった。▼
:事後条件とは、メソッドが実行されたことと、メソッドが正常終了して決められた状態遷移を果たしたことを保証する。正常終了には、途中の例外発生とその解決継続も含まれていることに注意する。クライアントの不正パラメータによるメソッド未実行は、例外も未発生と解釈されることに注意する。メソッド実行、正常終了、例外発生の各論理値が確定される。両者に事後条件からの利益（benefit）が出される<ref name=":0" />。
:* クライアントの利益<ref name=":0" />：決められた状態遷移と、あるならばリターン値を受け取ること。メソッド実行は真に、正常終了は真になる。
:* サプライヤの利益<ref name=":0" /> ：パラメータ値が不正ならば、メソッドを実行しなくてよいこと。メソッド実行は偽に、例外発生は偽になる。
'''その他'''
:例外型、エラー型、パラメータ型、リターン型、[[副作用 (プログラム)|副作用]]などは、契約の注釈として扱われることがある。
やや分かり難いサプライヤの利益の「メソッド未実行＝そこでの確実な例外未発生」は責任特定要素になる。異常終了は最も容易な責任特定要素になる。正常終了には例外発生の解決継続も含まれるのでやや複雑になる。例えば契約の入れ子で内側契約の例外が外側契約で解決されていた場合などは見落とされがちなので要注意になる。
▲不変条件は好ましくない状態遷移を
=== 契約の派生 ===
| |||