もっと仕様の話(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);

}

（続く、はず）