僕は、マークアップとプログラミング（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:「論理学」と書いたほうが誤解が少ないかもしれない。「論理」や「ロジック」はいろいろな意味で使われるから。
