A CafeOBJ specification consists of modules, in which sorts, operators and equations are declared. A module is declared with
module (or just
mod) as follows:
The name of a module (<module-name>) is written after
mod. Module elements (<module-elements>) are declared between
[Convention] All letters of module names are capitalized, e.g.
CafeOBJ modules can be classified into tights modules and loose modules. Roughly speaking, tight modules denote a unique model, and loose modules denote a class of models (*). Those are declared with the following keywords:
mod!: Tight modules
mod*: Loose modules
mod: Used when denotations unconcerned.
NAT+ are tight modules. Tight modules are used when describing data types like natural numbers, integers, strings, Boolean algebra, enumerated types and so on. Loose modules are used when describing parameters (of List, for example), behavior of systems and so on. For example, specifications of sets, groups, rings are described as loose modules.
See literatures of CafeOBJ for more details.
(*) The current CafeOBJ system behaves in the same way for each of
mod, that is, CafeOBJ system does not check whether an input module should be tight or loose.
Original Copyright © Takahiro Seino, all rights reserved.