形式仕様記述言語は，何らかの数学的な体系に従って，作られている．このうち，よく使用される形式的仕様記述言語は，（公理的）集合論に基づいているものが多い．原書にある集合論に基づく形式的仕様記述言語の例は，以下である．
Z, VDM, B, Alloy, OCL
実務で使ったことがないとしても，それぞれ名前を聞いたことがあると思う．
集合で考えることの必然性はなく，ただ，そう考えると考えやすい問題があるというだけに過ぎない．例えば，データベース設計をするときのテーブルは，カラムの値からなる集合と考えることができる．
静的表現は集合にできるとして，操作はどうであろうか．出金するという操作は，出金額が，操作前の残高から操作後の残高を引いた額に等しいと考える（場合によっては，手数料分も考慮する）．
組み込みシステムのような反応型（回数に制限なく入力を受け付け出力する）のシステムと違い，トランザクション型のシステムでは，操作の前と後という考えは，なじみやすい．
もう少し考えを進めると，値は何らかの枠にはまっていることが分かる．通常の口座であれば，マイナスになることはないし，小数点を持つことはない．値は自然数と考えて良いことが分かる．
基本は，上記である．次回からは，代表的な Z を用いた原書の例を示すことにする．スキップも考えたが，KAOSの記述を行う上で，必須となる知識なので，まだ，しばらくは亀の歩みとなる．
(nil)