契約プログラミング

契約プログラミング（Design by Contract; DbC）とは

契約プログラミング（Design by Contract; DbC）は、ソフトウェアの正確性と堅牢性を向上させるための設計手法です。この手法は、クラスとそのメソッドの利用に関する「契約」を形式的に定義することで、プログラムの信頼性を高めることを目指します。DbCは、ロバート・フロイド、アントニー・ホーア、エドガー・ダイクストラらの形式的検証の研究を基盤としています。

契約の概念

DbCの中心的な概念は、クライアント（メソッドの呼び出し側）とサプライヤ（メソッドを提供する側）の間の契約です。この契約は、以下の3つの要素で構成されます。

クラス不変条件：クラスのインスタンスが常に満たすべき条件。オブジェクトの状態が常に正しく保たれるようにするための制約。
事前条件：メソッドが実行される前にクライアントが満たすべき条件。メソッドの入力に関する制約。
事後条件：メソッドが正常に終了した後に満たされるべき条件。メソッドの出力と副作用に関する制約。

これらの条件は、クラスの振る舞いを定義し、クライアントに公開されたメソッドに適用されます。契約は、クライアントとサプライヤの間で、義務と利益を明確にします。クライアントは事前条件を満たす義務を負い、事後条件が満たされることを期待できます。一方、サプライヤは事前条件が満たされた状態でメソッドが呼び出されることを期待し、事後条件を満たす義務を負います。

具体例

例えば、配列の要素を参照するメソッドを考えてみましょう。事前条件として、クライアントは指定する添字が配列の範囲内であることを保証する必要があります。一方、事後条件として、メソッドは指定された添字の要素を返すことが期待されます。このように契約を明示することで、エラーが発生する可能性を減らすことができます。

事前条件

事前条件は、メソッド開始時に満たされるべき条件を表明したものです。これにより、メソッドの引数やサプライヤクラスのインスタンスの状態に制約が課されます。

引数に関する制約: 例えば、配列の要素にアクセスする際に、クライアントは指定する添字が有効な範囲内であることを保証する必要があります。
インスタンスの状態に関する制約: スタックから要素を取り出すpop操作の場合、クライアントはスタックが空でないことを保証する必要があります。

事前条件を契約と見なすと、クライアントの義務は事前条件を満たすことであり、サプライヤの利益は事前条件が満たされた状態でメソッドが実行されることです。

事後条件

事後条件は、メソッドが正常に終了した時に満たされるべき条件の表明です。メソッドの実行結果や、サプライヤクラスのインスタンスの状態、返り値などが対象となります。事後条件を満たすことはサプライヤの義務であり、クライアントは事後条件を満たした状態を期待できます。

不変条件

クラス不変条件は、クラスの各公開メソッドの開始時と正常終了時に共通して保証されるべき状態についての条件です。コンストラクタに関しては、事後条件としてのみ適用されます。不変条件はインスタンスの状態に関する制約であり、クラスのライフサイクル全体を通じて一貫性を保つためのものです。

義務と利益

DbCにおける契約は、クライアントとサプライヤの義務と利益を明確にします。

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

例外の扱い

メソッドの表明違反が発生した場合や、OSが異常を検出した場合は、例外として処理する必要があります。例外処理は、メソッドを成功させるか失敗させるかのいずれかです。成功させる場合は事後条件を満たし、失敗させる場合はシステムの状態をメソッド実行前に戻し、例外をクライアントに通知する必要があります。

契約の継承

クラスの継承関係において、サブクラスはスーパークラスの契約を尊重する必要があります。具体的には、サブクラスの不変条件はスーパークラスの不変条件を常に満たし、サブクラスの事前条件はスーパークラスの事前条件よりも弱く、サブクラスの事後条件はスーパークラスの事後条件よりも強くなければなりません。これはリスコフの置換原則に従うためです。

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

契約プログラミングをサポートする言語には、以下のようなものがあります。

Eiffel
Ada
D言語
Spec#
Kotlin
* Clojure

DbCは、ソフトウェア開発におけるエラーを早期に発見し、プログラムの信頼性を向上させるための強力なツールです。

もう一度検索