仕様の話

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

1. 論理（学）と仕様 - 檜山正幸のキマイラ飼育記 (はてなBlog)
2. 仕様の話(1)：いつもはじまりはホーア式 - 檜山正幸のキマイラ飼育記 (はてなBlog)
3. 仕様の話(2)：呼び出しからメッセージへ - 檜山正幸のキマイラ飼育記 (はてなBlog)
4. 仕様の話(3)：仕様のパイプライン結合 - 檜山正幸のキマイラ飼育記 (はてなBlog)

論理（学）と仕様

僕は、マークアップとプログラミング（i.e. XML構文とソフトウェア）をつなぐものは仕様技術だと思っています。よって当然、仕様の理論に興味があるわけ。

仕様技術についてヨーク考えてみると、それは結局、論理（logic）*1と同じことに気がつきます。元来は論理的な概念である充足（satisfaction）と伴意（entailment）が、仕様においても核心となる概念です。

α、βなどが何らかの表明／条件式（たとえばホーア論理式で書かれた制約）だとして、実装Mに対して、「M satisfies α」という言明（メタ表明、judgement）にハッキリした意味を持たせない限り、仕様の議論は何もできません。

「M satisfies α」は論理（モデル論）における「M |= α」とまったく同じこと（だと定義できます）。まー、実際には、仕様（制約）が1個の論理式で書けるとは限らないので、A = {α1, α2, ...}を論理式の集合（これが仕様記述に対応する）として、「M satisfies A」を、「A satisfies α1 かつ A satisfies α2 かつ … 」として定義しておきましょう。

そうすれば、仕様における伴意（entailment）「A entails B」は、

• M satisfies A となるようなMに対しては常に M satisfies B

であること、として定義できます。言い換えれば、

• 仕様Aを満たす実装Mは、常に仕様Bも満たしている

そのときに、A entails B なわけですね。

仕様の話(1)：いつもはじまりはホーア式

ソフトウェア技術のなかで僕が一番興味を持っているのは仕様技術です。正確に適切な仕様を記述すること、そしてその仕様をもとに検証ができること、それを望んでいるのですけど、まー、難しいですね、イロイロと。

で、仕様に関して最近思っていることなどを少し書いてみます。

「仕様を書く」という作業では、記述言語が必要ですね。その記述言語の基本単位を文（sentence）と呼びます。ここで、「文」という語は技術用語ですよ、なんとなく使っているわけでもないし、国語辞書的な用法でもないですからご注意。でも、「文」だけだと短すぎるので、以下「記述文」にします。

一番有名な記述文（の構文）はホーア式でしょう。事前条件P、実行部E、事後条件Qを組み合わせて {P}E{Q} という形で書きますが、現在のプログラミング言語との相性からは、中括弧の使用法を逆にして P{E}Q がいいと僕は思います（ので、こっちを使います）。P{E}Q の意味は、「条件Pを満たしている状態で、Eを実行したら、実行後には条件Qを満たす」というものです。

例えば、 (value() >= 0){inc();}(value() > 0) ならば、「value()が0以上の状態で、inc(); を実行したら、実行後にはvalue()は0より大きくなる」です。テストコードに直せば：

if (value() >= 0) {

  inc();

  if (value() > 0 ) {

    return true;

  } else {

    return false;

  }

} else {

  return true;

}

このコードは仕様違反があったときにだけfalseを返します。事前条件が成立してないことは仕様違反ではないのでtrueを返すことに注意してください。事前条件を調整するのはテスターの仕事ですから、(value() >= 0)じゃないから仕様違反だ、は理不尽すぎますね。

[追記]このケースだと、(value() >= 0) が不変条件のような雰囲気がありますが、ほんとに不変条件なら、(true){}(value() >= 0) と書かないといけません。

仕様の話(2)：呼び出しからメッセージへ

条件PやQを書くには副作用のない関数（のようなメソッド）が必要です。条件の評価のときに副作用があると、話がとんでもなくややこしくなります。また、条件評価で例外が生じたりするのも望ましくないので、副作用がなくエラーしない関数的メソッドが欲しいわけで、そういうメソッドはアクセッサ、オブザーバー、クエリーなどと呼んだりします。

一方、実行部のところには、メソッド呼び出しか単純代入文（var = method();）を並べるだけにします。これも話をややこしくしないためです。実行部に並べるメソッドのほうは、アクション、コマンド、ミューテータなどと呼びます。（ここまでの話は、何度かしたことがあります。）

さて、最近、実行部のところをもう少し抽象化したいと思っています。メソッド呼び出しだけでなくて、たとえば、HTTP GET/POSTでやってきたリクエスト＋パラメータとかも同じ枠組みで考えたいのですね。そこで、実行部のところには、外部からやって来たメッセージ（あるいはシグナル）の列を書くのだ、と考えます。メソッド呼び出しもメッセージだと思えばいいので、言葉使いとそれに伴う雰囲気が変わるだけ、とも言えます（が、その効果は無視できないものがあります。）

メッセージとメッセージが引き起こす内部効果は別物なので、MESSAGE causes EFFECTのような書き方をしましょう。さらに、EFFECTは状態遷移と外部へのメッセージ（イベントと言ったほうがお馴染み？）発信に分けて、例えば、次のように書きます（別に記述構文はどうでもいいのですが）。

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

  results (value() > 0)

  emits {valueChanged();}

これは、「(value() >= 0)の状態で、{inc();}というメッセージを受け取ると、(value() > 0)の状態になり、{valueChanged();}というメッセージ（イベント）が発行される」ということです。

仕様の話(3)：仕様のパイプライン結合

一般的には、事前条件P、受け取るメッセージ列M、状態遷移（move）m、発行されるメッセージ（イベント）列Nを使って、on P receiving M causes m emits N が仕様記述文てことになります。が、状態遷移は、遷移後の状態が満たす条件＝事後条件を書けば指定できるので、on P receiving M results Q emits N でもいいでしょう。

受信も送信もメッセージとして抽象化してあるので、パイプラインの記述が自然にできます。

spec Counter {

 // 安全なとき

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

   emits {valueChanged();}

 // 限界を超えているとき

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

   emits {overflow();}

}
spec Alarm {

 on (true) receiving {valueChanged();}

   emits {} // 何も起きない

 on (true) receiving {overflow();}

   emits {warn();}

}

CounterとAlarmを直列結合したものは、次の仕様を満たすことがわかるでしょう。

spec CounterWithAlarm {

 // 安全なとき

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

   emits {} // 何も起きない

 // 限界を超えているとき

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

   emits {warn();}

}

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

*1:「論理学」と書いたほうが誤解が少ないかもしれない。「論理」や「ロジック」はいろいろな意味で使われるから。