CafeOBJ で仕様を記述するには、まずモジュールを宣言し、その中に様々な宣言を記述する。モジュールは module (またはその省略形 mod )を使って次のように宣言する:
mod <module-name> {
<module-elements>
}
<module-name> にはモジュール名を指定する。モジュール名は SIMPLE-NAT のように、全て大文字で指定することが多い (慣習) 。<module-elements> は演算や等式の宣言などの記述であり、後述する。
モジュールを宣言する際に、モジュールを (人が) 解釈する際の意味論を指定できる※。
mod! : きつい意味論 (tight sematics) に基づくモジュールmod* : ゆるい意味論 (loose sematics) に基づくモジュールmod : 意味論を指定しないモジュール例えば、自然数の仕様に現れるモジュール SIMPLE-NAT や NAT+ はきつい意味論に基づいて記述されている。自然数やブール代数などの特定の代数系を対象とした性質を扱うときはきつい意味論が用いられる。群や環など、あるクラスの代数系が共通に持つ性質を扱うときは、ゆるい意味論に基づくモジュールとして記述する。
きつい意味論で定義されるモジュールの例としては、自然数、整数、文字、文字列、列挙型などがある。一方、ゆるい意味論で定義されるモジュールの例には、群、半群、環などがある。
この時点では、これらの違いを区別できなくてもよい。よく分からなければ、mod で記述してよい。
※ CafeOBJ 処理系は、これらの違いを考慮しない。あくまで人が読む時のコメントである。
Original Copyright © Takahiro Seino, all rights reserved.