論理（学）と仕様 - 檜山正幸のキマイラ飼育記 (はてなBlog)

僕は、マークアップとプログラミング（i.e. XML構文とソフトウェア）をつなぐものは仕様技術だと思っています。よって当然、仕様の理論に興味があるわけ。 仕様技術についてヨーク考えてみると、それは結局、論理（logic）*1と同じことに気がつきます。元来は論理的な概念である充足（satisfaction）と伴意（entailment）が、仕様においても核心となる概念です。 α、βなどが何らかの表明／条件式（たとえばホーア論理式で書かれた制約）だとして、実装Mに対して、「M satisfies α」という言明（メタ表明、judgement）にハッキリした意味を持たせない限り、仕様の議論は何もできません。 「M satisfies α」は論理（モデル論）における「M |= α」とまったく同じこと（だと定義できます）。まー、実際には、仕様（制約）が1個の論理式で書けるとは限らないので、A = {

[facet]

充足（satisfaction）と伴意（entailment）

[hiromark]

なーるほどー。

[yohei]

"マークアップとプログラミング（i.e. XML構文とソフトウェア）をつなぐものは仕様技術" そうか!