もっと仕様の話

かつて、次のURLsで書いた短い記事群をまとめてみた。文章はそのまま。

1. もっと仕様の話(1)：かたいことばっかり言ってると… - 檜山正幸のキマイラ飼育記 (はてなBlog)
2. もっと仕様の話(2)：インクリメント仕様をどう書くの - 檜山正幸のキマイラ飼育記 (はてなBlog)
3. もっと仕様の話(3)：テストメソッドとテスター - 檜山正幸のキマイラ飼育記 (はてなBlog)

もっと仕様の話(1)：かたいことばっかり言ってると…

昨日、仕様の話をしたのだけど、もう少し書いておこうかと。この話題になると長くなりがちですね、ヤッパリ。

昨日より：

とまー、こういう仕様の計算が自由にできたらいいな、と思っているのです。

けれども、

まー、難しいですね、イロイロと。

なんです。

「難しい」という話だけだとつまらないので、楽しそうなこと(?)や少しは現実的な話をすることにします。

実際には1人だけで作業するにしても、仕様を書く（設計）、実装する、テストするという3つの立場、役割は区別する必要があります。そうしないと、仕様技術の意義は全然理解できないでしょう。

以下では、仕様を書く人（役割）はあまり考えないで、実装者とテスターについて考えます。-- すごく大事な前提があります。

テスターと実装者のお約束：

1. 実装者は、仕様に書いてあることは守る。だが、仕様に書いてないことはどのように実装してもよい。
2. テスターは、仕様に書いてあることと明白に違う動作にはクレームをつける。だが、仕様に書いてないことでトヤカク言ってはいけない。

つまり、実装者とテスターは、共通の仕様記述以外の手段では情報交換しないことになります。

が、実際には、実装者とテスターの直接コミュニケーションを断っても、それでも、暗黙の情報が流れてしまいます。

例えば、昨日のエントリーで僕は、Counter, value(), inc()のような名前を使いました。これを見て、「incはインクリメント（increement）のことで、カウンタの値を1増やすのだろう」とだいたいの人は思うわけです。つまり、名前を通じて情報が勝手に流れます。

このことは、名前の付け方が大事であるという教訓を導くと同時に、名前やコメントの印象が「実装とテスト」の役割を曖昧にしてしまう危険性も示唆＜しさ＞します。

例えば、次の2つの記述文（制約）しかない状況を考えます。

  // 制約1

  on (value() < 100) receiving {inc();}

   emits {valueChanged();}

  // 制約2

  on (value() >= 100) receiving {inc();}

   emits {overflow();}

メッセージ受発信はメソッド呼び出しだとして、次の実装は完全に仕様を満たします。

int value() {

 return 1;

}
void inc() {

 valueChanged();

}

制約1に従って、inc()が来たらvalueChanged()を発行してます。この実装では、(value() >= 100)という条件が満たされることは絶対にないので、制約2を根拠にクレームされることはあり得ません。つまり、テスターがどんなテストをしようと、クレームを付けられません（完璧！）。

フォーマルな立場からは、「もっと精密に仕様を記述せよ」ということになりますが、そればっかり言うと、仕様技術を誰も使わなくなります。現実的には：

1. 自然言語記述や、自然言語の意味を利用した伝達を許す。
2. しかし、形式的記述も併用し、形式的に書かれた仕様の充足は絶対条件とする。

となるでしょうか。

今の例では、第3の仕様記述文として「inc()の後では、value()が返す値が1だけ増える」という自然言語文を加えます。すると、いつでも1ばっかり返している当該の実装はダメということになります。

もっと仕様の話(2)：インクリメント仕様をどう書くの

「インフォーマルな記述や伝達は許しましょうね」と言いました。そうでないと、たいてい破綻します。そのことは踏まえた上で、なるべくフォーマルに書くことを引き続き考えます。例は、カウンターのインクリメント。

inc()が実際にインクリメントであることを正確に書くのはけっこう難しいのです。事前条件は「value()の値が n」で、事後条件は「value()の値が n + 1」ですから、ホーア式では (value() == n){inc();}(value() == n + 1) です。

が、変数nの扱いが難しい。論理（学）の言葉でいえば、nは、for all n として使われる束縛変数ですから、制約全体の意味は：

どんなnに対しても

  「value()の値が n ならば、

    inc(); の後では、

    value() == n + 1」

となる。

となります。

「どんなnに対しても」だから、いろいろな値を片っ端からnに入れてテスト、ってのはバカバカしいですね。実際的には、等号（==）の意味を、「値未定の変数があれば代入操作をして、真とみなす」と解釈すればいいでしょう（これはPrologのユニフィケーションと同じです）。あるいは、汚い記述だけど、(true){n = value(); inc();}(value() == n + 1) で済ます手もあります。

値の代入がされてないなら代入を行う等号を「:==」とでもして、とりあえず次の形を採用しましょう。（:==の論理的な意味はあくまで「等しい」です。）

 forall(int n) {

   on (n :== value()) receiving {inc();}

     results (value() == n + 1)

     emits {valueChanged();}

 }

これに対するテストコードは、（メッセージ発信は別にして）次のようにでもすればいいでしょう。

public boolean testInc(int n) {

 if (n == value()) { // :== の論理的解釈

   inc();

   if (value() == n + 1) {

     return true;

   } else {

     return false;

   }

 } else {

   return true;

 }

}
public boolean testInc() {

  int n;

  n = value(); // :== の手続き的解釈

  return testInc(n);

}

もっと仕様の話(3)：テストメソッドとテスター

仕様記述文のメッセージ受発信をメソッド呼び出しと解釈するなら、on (P) receiving {E} results (Q) に対して、

if (P) {

  {E}

  return (Q);

} else {

  return true;

}

としてテストメソッドが書けます。

emits（メッセージ送信）の部分のチェックは、スタブメソッドを作って呼び出しログを取って、ログとつきあわせて検証することにします（ちょっとダサイけど）。

すると、仕様記述文 on (P) receiving {E} results (Q) emits {F} にテストメソッド（＋ログチェック）が対応します。forall(変数宣言) {文} のときは、{文}のところだけをメソッド化して、束縛変数はメソッド引数として人が具体化指定することで我慢しておきましょう（昨日のtestIncの例参照）。

さて、仕様記述からテストメソッド一式を準備できたとして、テスターは：

1. テストメソッドを（引数があれば適当な引数で）呼び出す。テストメソッドがfalseを返したら、即座に実装者にクレームする。
2. テストメソッド実行中のスタブ呼び出しログをemits部分と比較して、食い違いがあったら、即座に実装者にクレームする。
3. それ以外では、実装者に何も言わない。

これがテスターの作業です。

こういう前提のもとで、「テスターや実装者に無駄／無意味な作業をさせない、彼（女）らの労力をできるだけ減らすには、どうしたらいいか？」と、そういう問題意識を持つと、仕様技術（の一側面）を理解しやすくなります。特に、仕様技術で論理（学）がヘビーに使われる理由が納得できると思います。