契約プログラミング - 暇つぶしWikipedia

契約プログラミング

契約による設計

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

この節は検証可能な参考文献や出典が全く示されていないか、不十分です。出典を追加して記事の信頼性向上にご協力ください。（このテンプレートの使い方）
出典検索?: "契約プログラミング" ? ニュース・書籍・スカラー・ CiNii ・ J-STAGE ・ NDL ・ dlib.jp ・ジャパンサーチ・ TWL（2021年12月）

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

メソッド正常終了時のサプライヤクラスのインスタンスの状態

クライアントに渡す返り値

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

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

Size:42 KB
出典: フリー百科事典『ウィキペディア（Wikipedia）』
担当:undef