契約プログラミング

"契約" は、大きなプロジェクトのプログラミングの手間を減らす、 画期的な技術です。契約は、事前条件・事後条件・エラー・不変条件、 からなる概念です。 C++でも言語の変更無しに契約は実現できますが、 扱いにくく、 一貫性のないものになります。

言語レベルで契約のサポートを組み込むことには、こんな利点があります：

1. 契約の記述の一貫性
2. ツールのサポート
3. 契約の記述に基づく、 コンパイラによるよりよいコード生成
4. 契約の管理や強制の簡単化
5. 契約の継承

"契約"は、考え方は簡単で、常にtrueにならなくてはいけない式、のことです。 trueでなければ契約が破られていて、つまり定義から、プログラムにバグがあることがわかります。 契約はプログラムの仕様の一部分で、それをドキュメントではなくコード自身に書くようにした、 とも言えます。プログラマの皆さんはご存じのように、ドキュメントというのは不完全で、 古かったり間違っていたり、時にはどこにも存在しなかったりします。 契約をコードの中に持ってくることで、プログラムによる検証が可能になります。

表明契約

一番基本的な契約は、 AssertExpression. です。assert は、コードにチェック可能な式を埋め込み、 その式がtrueでなくてはならない、という条件を課します：

assert(expression);

C プログラマにはお馴染みでしょう。 しかし、C とは違い、関数本体での assert AssertError を投げる働きをします。 これはcatchして対応することができます。 契約違反をcatchするのは、 絶対にフェイルプルーフでなくてはならないコードから他の動作の怪しいコードを 使う必要があるときや、デバッグ時には役に立ちます。

事前・事後条件

前契約では、文が実行される前に成立していなければならない事前条件を記述します。 もっとも典型的な使い方は、関数の入力引数の検査でしょう。後契約は、 文の実行結果を検査します。もっとも典型的な使い方は、 関数の返値と副作用の検査でしょう。 構文は次のようになります：

in
{
    ...事前条件...
}
out (result)
{
    ...事後条件...
}
body
{
    ...コード...
}

定義から、前契約違反であれば、 bodyは間違った引数を渡されていることになります。 そこで AssertError 例外が投げられます。後契約に対する違反があれば、body にバグがあったことになります。このときは AssertError 例外が投げられます。

in と out 節のどちらかを省略することもできます。 関数本体のための out 節では、 変数 result が宣言され、関数の返値が代入されます。 例えば、平方根の関数を実装してみましょう：

long square_root(long x)
  in
  {
    assert(x >= 0);
  }
  out (result)
  {
    assert((result * result) <= x && (result+1) * (result+1) >= x);
  }
  body
  {
    return cast(long)std.math.sqrt(cast(real)x);
  }

in, out, body の中の assert は 契約 (contract) と呼ばれます。 assert以外の任意のDの文や式も 記述することができますが、 そのコードに副作用が無いように注意することが重要です。 リリース版のコードは契約のコードに依存してはいけません。 リリースビルドでは、 in と out 用のコードは生成されません。

関数の返値型がvoidの時は、返値がないので、out節で変数 result を宣言するのは不可能です。 この場合は、次の形式を使います：

void func()
  out
  {
	...契約...
  }
  body
  {
    ...
  }

out節では、result は関数の返値で初期化されます。

in, out と、継承

I関数が基底クラスの関数をオーバーライドしたものである時は、 その関数自身かまたは基底クラス達の in 契約のうち、 どれか一つが満たされればよいことになります。 関数のオーバーライドは、 in 契約を より緩く していることになります。

in 契約を持たない関数は、 関数の引数として任意の値を許すという意味になります。これはつまり in 契約を持たない関数が継承階層の中にあると、 その関数をオーバーライドした関数の in 契約は何も効果を持たないことになります。

逆に、out 契約は全て満たされる必要がありますから、 関数のオーバーライドは、 out 契約を より厳しく していることになります。

クラス不変条件

クラス不変条件は、 常に成り立っているクラスの性質を記述するものです。 （ただしメンバ関数の実行途中は除く。） クラス の項で説明しています。

参考資料

• Contracts Reading List
• Adding Contracts to Java