Modules

In Maude the basic units of specification and programming are called modules.^3.1 A module consists of syntax declarations, providing appropriate language to describe the system at hand, and of statements, asserting the properties of such a system. The syntax declaration part is called a signature and consists of declarations for:

• sorts, giving names for the types of data,
• subsorts, organizing the data types in a hierarchy,
• kinds, that are implicit and intuitively correspond to ``error supertypes'' that, in addition to normal data, can contain ``error expressions,'' and
• operators, providing names for the operations that will act upon the data and allowing us to build expressions (or terms) referring to such data.

We use symbols $\Sigma, \Sigma'$, etc. to denote signatures.

In Core Maude there are two kinds of modules: functional modules and system modules. Signatures are common for both of them. The difference between functional and system modules resides in the statements they can have:

• functional modules admit equations, identifying data, and memberships, stating typing information for some data, while
• system modules also admit rules, describing transitions between states, in addition to equations and memberships.

We use $E, E'$, etc. to denote sets of equations and memberships, and $R, R'$, etc. to denote sets of rules.

From a programming point of view, a functional module is an equational-style functional program with user-definable syntax in which a number of sorts, their elements, and functions on those sorts are defined. From a specification viewpoint, a functional module is an equational theory $(\Sigma, E)$ with initial algebra semantics. Functional modules are described in detail in Chapter 4, here we just discuss some of their top-level syntax. Each functional module has a name, which is a Maude identifier. Any Maude identifier can be used, but the preferred style for module names is an all capitalized identifier, and in the case of a compound name the different parts are linked with hyphens. For example, a module defining numbers and operations on them can be called NUMBERS. The top-level syntax will then be

  fmod NUMBERS is
    ...
  endfm

with `$\ldots$' corresponding to all the declarations of submodule importations, sorts, subsorts, operators, variables, equations, and so on.

From a programming point of view, a system module is a declarative-style concurrent program with user-definable syntax. From a specification viewpoint, it is a rewrite theory $(\Sigma, E, \phi, R)$ (where $\phi$ specifies the frozen arguments of operators in $\Sigma$; see Section 4.4.9) with initial model semantics. Again, each system module has a name, which is a Maude identifier. And as for functional modules, the preferred style is an all capitalized name, with consecutive parts linked with hyphens in the case of compound names. For example, a module specifying the behavior of a vending machine may be called VENDING-MACHINE. It will then be introduced with the following top-level syntax:

  mod VENDING-MACHINE is
    ...
  endm

where again `$\ldots$' corresponds to all the declarations of submodule importations, sorts, subsorts, operators, variables, equations, rules, and so on. System modules are described in detail in Chapter 5.

In the rest of the chapter we will describe the ingredients of signatures, that is, the syntactic elements common to both functional and system modules, such as sorts, subsorts, kinds, operators, variables, and the terms that can be built on a signature, postponing the discussion about the syntax specific to functional and system modules to Chapters 4 and 5, respectively.