もっと仕様の話(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. それ以外では、実装者に何も言わない。

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

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

（続く）