[ 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クラス

• 基本クエリ
  • value_for(key)
• 生成コマンド
  • initialize
• 他のコマンド
  • put(key, value)
  • remove(key)
• 派生クエリ
  • has(key)

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
  • tail
  • is_empty
• 生成コマンド
  • initialize
• 派生クエリ
  • count
  • preceeded_by
  • is_equal
  • item
  • sublist

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

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. オブジェクトについて、変化しない属性を定義し、不変条件として記述する

メモ

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

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

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

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

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

実装の悩み

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

事前条件のパターン

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

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

• 引数で渡される値
  引数は呼び出し側がルーチン・メソッドの呼び出し時に設定するので、事前条件の検査は可能です。
• インスタンスのメンバ変数・スタティック変数
  オブジェクトの内部状態（メンバ変数）やルーチン側に隠蔽されるスタティック変数が事前条件に必要な場合、そのままでは呼び出し側が検査できないので、事前条件の成否を判定できるクエリ・メソッドを提供する必要があります（単なるGetter関数かもしれません）。
• スレッドローカル変数・グローバル変数
  オブジェクト指向プログラミングではほとんど使用することはありませんが、これらの事前条件の検査は呼び出し側で可能です。
• 外部リソース（ファイル・DB接続など）
  外部リソースを使用する処理の場合、事前条件の検査はやっかいです。リソースの確保が誰の責務かを検討し、その責務の持ち主が事前条件に入っていなくては検査ができません。色々な設計があるので、一概には言えませんが、いくつかパターン分けはできそうです。
  
  • 外部リソースの使用がオブジェクトのライフサイクルと一致している場合
    オブジェクトを生成したときに外部リソースの使用を開始し、そのリソースはオブジェクトが破棄されるまで継続して使用される場合、生成コマンドでリソースの使用が成功している必要があります。このときは、生成コマンドの事前条件と事後条件にリソースの使用が定義されていなければなりません。生成コマンドが成功していれば、個々のルーチンで検査する必要はありません。
  • 外部リソースの使用がそのルーチン・メソッドで毎回実施される場合
    ルーチンに渡した引数の値等からリソース使用の開始を行うような場合、事前条件でリソースの存在を検査する必要があります。
  • 外部リソースの使用が、オブジェクトのメソッドで制御される場合
    いい設計か疑う必要がありそうですが、この場合、リソースの使用可否を判定できるクエリを提供し、リソースを使用するメソッドの事前条件でリソース使用可否を検査する必要があります。