Modules

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:

mod <module-name> {
<module-elements>
}

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. SIMPLE-NAT.

Tight modules, Loose modules

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.

For example, SIMPLE-NAT and 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!, mod* and mod, that is, CafeOBJ system does not check whether an input module should be tight or loose.

[Next] Sorts

Original Copyright © Takahiro Seino, all rights reserved.