[ C++で開発 ]

契約による設計（Design by Contract）

契約による設計を行うと、クラス・メンバ関数の仕様が明確化し、また、クラスのインタフェースに絡むバグの検出が容易になります。しかし、慣れるまでは考え方が難しく、言語仕様ではない、よい例題もなかなか見当たらないので、広まってはいません。

このページは、契約による設計を理解する試みと例題の収集・整理を行います

契約による設計とは

「契約による設計」の概念は、書籍「オブジェクト指向入門 第2版 原則・コンセプト編」（バートランド・メイヤー著）の11章にて解説されています。信頼性の高いソフトウェアを構築するための考え方・設計方法です。以下は、同書籍の勉強ノートです。

「オブジェクト指向入門 第2版 11章 契約による設計」　の勉強ノート

プログラムが正しいか間違っているかは、プログラム自体を見ても判断できません。プログラムとプログラムの仕様とを照らしあわせてはじめて正しいか間違っているかを判断できます。

そこで、プログラムが正しいことを保証する最初の第一歩は、プログラムの仕様を表すことです。

正しさの公式　｛P｝A｛Q｝

　　P: 開始状態（事前条件）
　　A: 処理
　　Q: 終了状態（事後条件）
例）{ x >= 9 } x := x + 5 { x >= 13 }

この正しさの公式を、ルーチン（関数・メンバ関数）に適用します。ルーチンの処理が上述の正しさの公式のAであり、ルーチンが呼び出されるときに必ず保持されているべき性質が事前条件（precondition）、ルーチンが完了するときに保持されているべき性質が事後条件（postcondition）です。

スタックのデータ型（クラス）に対するput操作の事前・事後条件の例

事前条件
スタックは一杯ではない
事後条件
スタックは空ではない
スタックの一番上は今putされたもの
要素数は1増加している

ルーチンを呼び出す側は、ルーチンの事前条件を必ず満たしていなければなりません。もし、ルーチンの呼び出し側が、そのルーチンの事前条件を満たさなかった場合、ルーチンは事後条件には縛られる必要がありません。すなわちルーチンはどんな結果となってもよいのです（でたらめな値を返す、戻ってこない、実行を中断する、等）。

ルーチンは、事前条件が満たされて呼び出されたならば、事後条件を満たさなくてはなりません。

この事前条件、事後条件が破られたということは、プログラムのバグ（誤り）を意味します。事前条件違反は、ルーチンの呼び出し側のプログラムのバグを、事後条件違反はルーチンのバグを示します。

バグの明確化

エラー（error）
ソフトウェアシステム開発中になされた誤った決定
欠陥（defect）
意図した振る舞いからシステムが逸してしまう原因となるソフトウェアシステムの特性
フォールト（fault）
何らかの実行中に意図した振る舞いからシステムが逸してしまうソフトウェアシステムのイベント

事前条件は仕様の観点で定義する。
事前条件はルーチンの呼び出し側で保証する必要があるので、隠蔽されている特性を事前条件で使わない。ルーチンの呼び出し側で利用可能な特性で事前条件を定義する。

クラス不変表明（invariant）

クラスインスタンスに共通する特性。すべての安定した時点（インスタンス生成時、公開ルーチンの呼び出し前後）で、クラスのすべてのインスタンスが満たしていなければならない表明の集合。
すなわち、不変表明は、常に満たされる必要はない。例）ルーチンの処理過程は不変表明を満たさない状態がある
ルーチンの正しさ（の公式）　　｛ INV and PRE } body { INV and POST }
    INV: クラス不変表明
　　PRE: 事前条件
　　POST: 事後条件
　　body: ルーチン

表明は入力検査ではない

外部からの入力（ユーザ入力やセンサ入力）は、表明ではなく、実際の処理として検査を行うこと

開発段階と表明の監視レベル

デバッグおよびリリース前のテスト中：　最高レベルで表明を監視
効率重視のアプリケーション運用中：　すべての監視を除去
通常のアプリケーション運用中：　事前条件のみチェック
すべての監視を除去するのは、乾いた地面でライフジャケットを着て練習し、海に出たとたんライフジャケットを脱ぎ捨てるようなもの。

「オブジェクト指向入門 第2版 12章 契約が破られるとき」　の勉強ノート

例外とは、システムの実行を混乱させる異常なイベント。厳密に定義すると、ルーチン呼び出しの失敗を引き起こす可能性のある実行時イベント。

ルーチンが契約を満たす状態で実行を終えた場合、そのルーチン呼び出しは成功である。成功しなければ、失敗である。

例外によってルーチンは失敗することが多いが、例外を捕らえて計算の途中状態をリストアするようにルーチンを書くことで、場合によっては失敗を防ぐことができる。失敗と例外は別概念。

例外処理とは、失敗を避けるために例外を処理する方法

やってはいけない例外処理：　単にメッセージを出力して呼び出し元にリターン　→　呼び出し元は例外に気付かず実行を継続してしまう。

例外処理の原則

ルーチンの実行中に起きた例外を処理する正しい2つの方法
１） リトライ：　例外となる状態を変更し、ルーチンを最初から実行しなおす（条件を変えて実行、あるいは単に再実行）
２） 失敗：　環境をきれいにし（不変表明を満たす状態）、実行を終了して呼び出し側に失敗を報告する

例外の発生するケース

E1) a.fと修飾つきの特性呼び出しで、aがvoid（ヌル）であることが分かった場合
E2) 拡張されたターゲットにvoid（ヌル）の値をアタッチ（代入や引数渡し）しようとした場合
E3) ある操作の実行で起きた異常条件がハードウェアかオペレーティングシステムによって検出された場合
E4）失敗するルーチンを呼んだ
E5） ルーチンの事前条件が入り口で満たされていないことが分かった場合
E6） ルーチンの事後条件が出口で満たされていないことが分かった場合
E7） クラス不変表明が入り口か出口で満たされていないことが分かった場合
　　　：（以下略）

契約による設計の例

書籍「Design by Contract, by Examples」（R Mitchell、J McKimら著）にある例題から事前・事後条件の定義を抜き出します。

事前条件、事後条件の例

CustomerManagerクラス

顧客IDと顧客情報をひもづけして管理する機能を持つクラスCustomerManagerの各メソッドの事前／事後条件を以下に抜き出します。

CustomerManager
 
count(): int
id_active(an_id:CustomerID): bool
add(a_customer:Customer)
name_for(an_id:CustomerID): string
set_name(an_id:CustomerID, a_name:string)
...
add(a_customer)メソッド

引数で指定されたCustomerオブジェクトの属性idでそのオブジェクトをひも付けして保持する。

事前条件
そのidが有効ではない：　not id_active(a_customer.id)
事後条件
数が1つ増加する：　count = old count + 1
idが有効になる：　id_active(a_customer.id)
set_name(an_id, a_name)メソッド
事前条件
idが有効：　id_active(an_id)
事後条件
idで指定した名前が保持される：　name_for(an_id).is_equal(a_name)
name_for(an_id)メソッド
事前条件
idが有効：　id_active(an_id)
事後条件
なし（set_nameの事後条件でname_forについて定義されているから）
countメソッド
事前条件
なし
事後条件
なし（addの事後条件でcountについて定義されているから）
クラス不変条件

顧客数は負の値にはならない

※事前条件なしは、いつ呼んでもいいことを意味する
　事後条件なしは、他のメソッドの事後条件で定義されるものも含める。
　契約による設計は、クラスのメソッド毎に独立してるのではなく、クラスで１つのまとまった契約を持つ

Stackクラス

is_emptyメソッド
事前条件
なし
事後条件
countが一貫している：　Result = (count = 0)
put（g)メソッド
事前条件
なし
事後条件
countが増加する：　count = old count + 1
トップの要素がgとなる：　item_at(count) = g
initializeメソッド
事前条件
なし
事後条件
スタックの要素数は０：　count = 0
item_it(i)が定義可能なiは存在しない
itemメソッド
事前条件
スタックは空ではない：　count > 0
事後条件
Result = item_at(count)
removeメソッド
事前条件
スタックは空ではない：　count > 0
事後条件
数が１つ減少：　count = old count - 1
item_at(i)メソッド
事前条件
iは下限より大きい：　i >= 1
事後条件
iは上限より小さい：　i <= count

Dictionaryクラス

initializeメソッド
事前条件
なし
事後条件
辞書が空である：　count = 0
put(key, value)メソッド
事前条件
キーがユニーク：　not has(key)
キーがヌルでない： key != 0
事後条件
キーの値はvalue：　value_for(key) = value
キーが辞書に存在する： has(key)
count = old count + 1
remove(key)メソッド
事前条件
ｊｊ
事後条件
キーが辞書に存在しない： not has(key)
value_for(key)の事前条件が偽となる
count = old count - 1
has(key)メソッド
事前条件
なし
事後条件
count = 0なら、Resultは偽：　(count = 0) implies (not Result)
value_for(key)メソッド
事前条件
キーが辞書に存在する： has(key)
事後条件
なし（putの事後条件で定義済み）
クラス不変条件

数は常に0以上：　count >= 0

ImmutableListクラス

基本クエリは他のメソッドの事後条件で定義されるので、基本クエリ自身には事後条件を記述しないことが多い。

headメソッド
事前条件
空ではない： not is_empty
tailメソッド
事前条件
空ではない：　not is_empty
事後条件
なし（他のメソッドの事後条件で定義済み）
initializeメソッド
事前条件
なし
事後条件
is_empty
countメソッド
事前条件
なし
事後条件
is_empty implies (Result = 0)
(not is_empty) implies (Result = 1 + tail.count)
preceeded_byメソッド
事前条件
ｊｊ
事後条件
not Result.is_empty
Result.head = g
Result.tail.is_equal(Current)
is_equal(other)メソッド
事前条件
other != 0
事後条件
Result = (is_empty and other.is_empty)
さもなくば
(not is_empty) and (not other.is_empty)
のとき
(head = other.head and tail.is_equal(other.tail))
itemメソッド
事前条件
i >= 1
i <= count
事後条件
i = 1 かつ Result = head
さもなくば
Result = tail.item(i - 1)
sublistメソッド
事前条件
from_position >= 1
from_position <= to_position + 1
to_position <= count
事後条件
Result.is_empty = (from_position > to_position)
(from_position <= to_position) implies (Result.head = item(from_position))
(from_position <= to_position) implies (Result.head = item(from_position)
(from_position <= to_position) implies (Result.tail.is_equal(sublist (from_position + 1, to_position)))

SimpleQueueクラス

removeメソッド
事前条件
count > 0
事後条件
count = old count + 1
items.is_equal(old item.tail)
countメソッド
事前条件
なし
事後条件
Result = items.count
initialize(a_capacity)メソッド
事前条件
a_capacity >= 1
事後条件
capacity = a_capacity
count = 0
headメソッド
事前条件
count >= 1
事後条件
Result = items.head
putメソッド
事前条件
count < capacity
事後条件
count = old count + 1
items.item(count) = g
is_emptyメソッド
事前条件
なし
事後条件
Result = (items.count = 0)
is_fullメソッド
事前条件
なし
事後条件
Result = (items.count = capacity)
クラス不変条件

count = items.count

毎回items.countを評価するのはコスト大のため、属性countを設け、このcountが常にitems.countと等しい条件（不変条件）であるとし、それぞれの特性(メソッド）の事前条件／事後条件では、countを用いる。

原則・指針

原則

  1. メソッドは、コマンドとクエリとを分けるべき
    コマンド：　オブジェクトの状態を変更するが、結果は返さない。
    クエリ：　オブジェクトの状態は変更せずに、結果だけ返す。
  2. 派生したクエリを基になるクエリーと分けるべき
  3. 各派生クエリは基となるクエリを用いて結果を定義するよう事後条件を記述するべき
  4. それぞれのコマンドでは、すべての基本クエリの値を定義（制約）する事後条件を記述するべき
  5. クエリおよびコマンドは、すべて適切な事前条件を定めるべき
  6. オブジェクトについて、変化しない属性を定義し、不変条件として記述する

メモ

事後条件を定義するために、新たなクエリを導入することがある。ただし、新たなクエリを導入すると、既存のコマンド・クエリの事後条件を増やす必要が生じる。

契約による設計を実装するには

関数、メンバ関数は、「契約による設計」の考え方に基づき、事前条件・事後条件を明確に定義する。また、クラスについては、クラス不変条件を定義する。

契約による設計で定義する条件と違反時の原因箇所
条件 内容 条件違反発生時 条件を定義する場所
事前条件 ルーチン・メソッドを呼ぶ際、呼び出し側が真であることを保証する条件 部品呼び出し側のバグ 各ルーチン・メソッド
事後条件 ルーチン・メソッドが実行後に真となるべき条件 部品内部のバグ 各ルーチン・メソッド
クラス不変条件 クラスにおいて、変化しない属性の条件 部品内部のバグ クラス

事前条件は、ルーチン・メソッドの呼び出し側が保証しなくてはならないため、ルーチン・メソッド（クラス）の内部に隠蔽されている情報を用いてはいけない。事前条件に必要なものは呼び出し側に公開しなくてはならない。

そこで、メソッドを以下に分類して設計すると、契約による設計の当てはめが容易になる。

メソッド種類 オブジェクトの状態への作用 結果（戻り値） 関係 例
コマンド 状態を変更する 返さない 基本クエリを用いて事後条件を定義する put, remove
基本クエリ 状態を変更しない 返す 他のメソッドの事前／事後条件で振る舞いが定義されることがあり、その場合自身の事後条件は省略する count, item
派生クエリ 状態を変更しない 返す 派生クエリは、基本クエリを用いて定義する is_empty
生成コマンド ー ー オブジェクトを生成する initialize

実装の悩み

いざ、実際に事前条件・事後条件を書けといっても・・・と悩むのが大半のプログラマの本音かもしれません。

事前条件のパターン

事前条件は、処理実行前のプログラムの状態が、処理実行可能な条件であることを検査することです。プログラムの状態とは、ルーチン・メソッドに引数として渡された値、インスタンスのメンバ変数、スタティック変数、スレッドローカル変数、グローバル変数、外部リソース（ファイル、リソースファイル、ネットワーク、DB接続、など）といったものが該当します。

事前条件を満たすのは、ルーチン・メソッドの呼び出し側なので、上述の処理実行可能な条件を整えるのは呼び出し側の責務です。しかし、呼び出し側が条件を検査するために必要な手段が提供されていることが必要です。