メイヤー（Bertrand Meyer）の意味の契約とは、関数や手続きを機能の提供者（業者）、機能を利用する側を顧客とみなしての責務に関する約束事です。契約のあいだには、より強い（きびしい）契約、より弱い（ゆるい）契約という順序関係があります。この強弱の関係は、直感的に明らかなように見えても、誤解されがちな難しい概念です。
内容：
- メイヤー流の契約とは
- 契約が守られること＝妥当性
- 契約条件を集合で表現しておく
- 入出力に関する契約条件と責務
- 契約条件に関する推論
- 契約条件の強弱に関する注意
メイヤー流の契約とは
契約はソフトウェアの仕様記述の一部なので、曖昧性があっては困ります。契約は自然言語ではなくて論理式で書かれます。しかしとりあえず、インフォーマルな説明を先にすると； 機能の提供者が主語（私）となる契約の内容は次のようになります。
- 私が作業をする前に、コレコレの条件が満たされることを要求します。これらの条件が揃っているならば、私はちゃんと仕事を完了することをお約束します。一方もし、これらの条件にちょっとでも不備があるなら、私が何をしようとあなた（顧客）は文句を言えません。
- 私が作業を終えたときは、ナニナニの条件が満たされることを保証します。
よって、利用者（顧客）は「コレコレの条件」を満たしてあげる義務が発生します。利用者が義務を果たしたにも関わらず「ナニナニの条件」がクリアされないときは、提供者に落ち度があります。訴えて糾弾しましょう。
「コレコレの条件」を論理式として書いたものをP、「ナニナニの条件」の論理式をQとします。提供者が行う作業をfとします。すると契約は、require P do f ensure Q と書けます。
契約はホーア（Tony Hoare）の表明 P{f}Q と似てます。似てますが違いもあるので注意してください。契約には提供者と顧客の別があるので、契約が破られたときの責任の所在が云々できます。ホーアの表明にはそのような複数の利害関係者は想定してないので、表明が失敗しても「誰のせいだ？」という話は出てきません。ホーアの表明では、Pが偽になっても契約違反だとか失敗だとか騒がないで、通常は成功として穏便に(?)済ませます。ホーアの表明は例外に関しても寛容で、「不測の事態はしょうがないよね」と責めたりはしません。
提供者が行う作業fを、関数の評価計算だとしましょう。引数xから関数値 y = f(x) が計算されます。このときの条件Pは、集合Aを使って x∈A と書けて、同様に条件Qは y∈B と書けるとしましょう。このケースでの契約の内容は次のようになります。
- 私がfの計算をする前に、x∈A であることを要求します。x∈A ならば、私はちゃんと f(x) の値を計算することをお約束します。一方もし、x∈A でないなら、私が何をしようとあなた（顧客）は文句を言えません。
- 私がfの計算を終えたときは、y∈B （y = f(x)）であることを保証します。
契約が守られること＝妥当性
関数と、その関数により計算を行う提供者を同一視して、f, g, h などは提供者を表すとします。契約はα, βなどギリシャ文字で表します。提供者（＝関数）fが契約αを守ることを f |= α と書くことにします。記号「|=」はダブルターンスタイルと呼ばれる記号で、その意味と使い方は「論理：証明可能性と普遍妥当性」に書いてあります。「論理を身に付けるには」も参考になるかもしれません。より詳しくは、4回シリーズの「論理とはなにか？」をどうぞ。
f |= α は、妥当性を主張したメタな命題です。この妥当性をもとに、2つの契約αとβに関して次のようなメタな関係を考えます。
- f |= α であるようなfは、必ず f |= β となる。
別な言い方をすると、
- どんなfであれ、fが契約αを守れるならば、fは契約βも守れる。
論理記号を使って書けば、
- ∀f.(f |= α ⇒ f |= β)
個別のfとαに関する「f |= α」の判定も難しいのに、すべてのfを調べる必要があるので、「∀f.(f |= α ⇒ f |= β)」の判定は現実的には難しいでしょう。しかし、αとβを構文的に比べる手続きで「∀f.(f |= α ⇒ f |= β)」かどうかが分かる場合もあります。以下、記法を簡略化するために、「∀f.(f |= α ⇒ f |= β)」を「α |⇒ β」と書きます。
関数計算の場合の契約αは、require (x∈A) ensure (f(x)∈B) と書けるのでした。契約βは require (x∈C) ensure (f(x)∈D) だとします。A, B, C, Dという4つの集合が出てきます。これらの集合の“大きさ”を比べて、α |⇒ β を結論できる場合があります。以下、その方法の説明をします。
契約条件を集合で表現しておく
require (x∈A) ensure (f(x)∈B) をもう少し操作しやすい形に書き換えておきましょう。
関数fは十分に広いデータ領域U上の部分関数 f:U→U だとして、その定義域をDef(f)とします。x∈Def(f) とは、f(x) の計算が正常に終了して確定した値を出すことです。Def(f) の外では f(x) は未定義になります。集合B（B⊆U）に対して、fによる逆像を f-1(B) と書きます。x∈f-1(B) ⇔ f(x)∈B です。
require (x∈A) の意味は、A⊆Def(f) のことです。require (x∈A) を主張する背景として、提供者側には、「x∈A ならば、f(x) を確実に計算できる」自信が必要です。逆に言えば、
- x∈A でないなら、f(x) を計算できない可能性がある、どうなっても知らねーぞ。
となります。
ensure (f(x)∈B) は、「x∈A ならば f(x)∈B」のことです。x∈A は既にrequireで仮定した命題なので、これは f(x)∈B が成立することを主張しています。fの逆像を使って書けば A⊆f-1(B) となります。
requireとensureの命題を合わせると、
- A⊆Def(f) ∧ A⊆f-1(B)
となります。
ちなみにホーアの表明は、
- x∈(A∩Def(f)) ならば、f(x)∈B
なので、
- (A∩Def(f))⊆f-1(B)
です。ホーアの表明は、A⊆Def(f) をまったく主張してないことに注意してください。
入出力に関する契約条件と責務
require (x∈A) ensure (f(x)∈B) という契約で、x∈A を守るのは利用者の責任となります。一方、利用者が x∈A を守った前提で、提供者は f(x)∈B であることを約束します。
- fの利用者（呼び出し側）は、変な引数をfに渡してはいけない。Aの範囲内にある正しい値を渡す責務がある。
- f（機能の提供者）は、正しい引数を渡されたなら、変な戻り値を返してはいけない。Bの範囲内にある正しい戻り値を返す責務がある。
責務は、それを履行する側の負担を伴います。入力（引数）の契約条件を守るために、利用者は引数の準備に注意を払います。出力（戻り値）の契約条件を守るためには、関数内で戻り値を勝手に作るわけにはいきません。
契約の強い（きびしい）／弱い（ゆるい）は、立場によって逆転します。利用者にとってきびしい条件が付くと、提供者は楽になります。利用者にゆるーい条件なら、提供者に負担がかかるでしょう。
ここから先、強い／弱いは、機能の提供者（関数）の立場から見てのことだとします。強い条件を守れる提供者は、より弱い条件は何もしなくてもクリアできます。弱い条件から強い条件に変更されると、そのままでは条件を守れないでしょう。
先に出した α |⇒ β とは、
- ∀f.(f |= α ⇒ f |= β)
だったので、「αを守れるf（提供者）なら何もしなくてもβは守れる」ことなので、「αは強く、βは弱い条件」ということになります。
契約条件に関する推論
先ほど、契約αとβは次のようだとしました。
- 契約αとは require (x∈A) ensure (f(x)∈B)
- 契約βは require (x∈C) ensure (f(x)∈D)
契約をパラメータfを持つ論理式と考えれば：
- α ≡ λf.(A⊆Def(f) ∧ A⊆f-1(B))
- β ≡ λf.(C⊆Def(f) ∧ C⊆f-1(D))
α |⇒ β というメタな命題は、たいへんに超越的ですが、αという命題からβという命題が証明できるなら、（モデルの健全性を前提に）α |⇒ β が言えることになります。
もちろん、何もない手ぶらの状態でαからβを証明できるわけではありません。いま、C⊆A、B⊆D だとします。この2つの包含関係とαを仮定して、βが証明できます。
仮定した C⊆A とαの一部である A⊆Def(f) から C⊆Def(f) が言えます。また、C⊆A、B⊆D とαの一部である A⊆f-1(B) から C⊆f-1(D) が言えます。結局、C⊆A、B⊆D、α からβを証明できるので、次のメタな主張が合理化されます。
- C⊆A、B⊆D ならば、α |⇒ β
契約条件の強弱に関する注意
前節の内容を言い換えてみると、αがβより強い（きびしい）とは、
- αの入力（引数）の集合Aはβのものより大きい。
- αの出力（戻り値）の集合Bはβのものより小さい。
同じことですが、βがαより弱い（ゆるい）とは、
- βの入力（引数）の集合Cはαのものより小さい。
- βの出力（戻り値）の集合Dはαのものより大きい。
入力集合と出力集合で増減の方向が逆転していることに注意してください。ここは多くの人が誤解や錯覚をしているところです。
契約を強く（きびしく）したいなら：
- 入力（引数）の集合をより大きくする。
- 出力（戻り値）の集合Bをより小さくする。
のです。逆に契約を弱く（ゆるく）したいなら：
- 入力（引数）の集合をより小さくする。
- 出力（戻り値）の集合Bをより大きくする。
もう一度繰り返しますが、提供者の立場だと、
- 既に強い条件を守っているなら、より弱い条件は何もしなくてもクリアできる。
- 弱い条件から強い条件に変更されると、そのままでは条件を守れなくなる（場合が多い）。
入力の許容範囲を広げることは提供者側への負担増となることはヨクヨク注意してください。今までは考えなくてもよかった入力値への対処を追加する必要があります。それに対して、出力の範囲を広げても、特に何もしなくても大丈夫なのです。
落ち着いて考えれば当たり前のことなんですが、入力集合と出力集合で増減の方向が逆であることで混乱したり、契約の強弱と型パラメータの具体化を混同したりして、ここらへんの議論は間違いやすいのです。時間のあるときに、ユックリと復習してみることをオススメします。
