module

[sys:]module[!|*] <modname> [ ( <params> ) ] [ <principal_sort_spec> ] { mod_elements ... }

Defines a module, the basic building block of CafeOBJ. Possible elements are declarations of

• import - see protecting, extending, including, using
• sorts - see sort declaration
• variable - see var
• equation - see op, eq, ceq, bop, beq, bceq
• transition - see trans, ctrans, btrans, bctrans

modname is an arbitrary string.

module* introduces a loose semantic based module.

module! introduces a strict semantic based module.

module introduces a module without specified semantic type.

If params are given, it is a parameterized module. See parameterized module for more details.

If principal_sort_spec is given, it has to be of the form principal-sort <sortname> (or p-sort <sortname>). The principal sort of the module is specified, which allows more concise views from single-sort modules as the sort mapping needs not be given.