Go to the first, previous, next, last section, table of contents.

3.2.9 MODULE declarations

A module is an encapsulated collection of declarations. Once defined, a module can be reused as many times as necessary. Modules can also be so that each instance of a module can refer to different data values. A module can contain instances of other modules, allowing a structural hierarchy to be built.

The syntax of a module declaration is as follows.

module ::
        "MODULE" atom [ "(" atom "," atom "," ... atom ")" ]
        [ var_declaration        ]
        [ ivar_declaration       ]
        [ assign_declaration     ]
        [ trans_declaration      ]
        [ init_declaration       ]
        [ invar_declaration      ]
        [ spec_declaration       ]
        [ checkinvar_declaration ]
        [ ltlspec_declaration    ]
        [ compute_declaration    ]
        [ fairness_declaration   ]
        [ define_declaration     ]
        [ isa_declaration        ]

The atom immediately following the keyword "MODULE" is the name associated with the module. Module names are drawn from a separate name space from other names in the program, and hence may clash with names of variables and definitions. The optional list of atoms in parentheses are the formal parameters of the module. Whenever these parameters occur in expressions within the module, they are replaced by the actual parameters which are supplied when the module is instantiated (see below).

An instance of a module is created using the VAR declaration (see section 3.2.1 State Variables). This declaration supplies a name for the instance, and also a list of actual parameters, which are assigned to the formal parameters in the module definition. An actual parameter can be any legal expression. It is an error if the number of actual parameters is different from the number of formal parameters. The semantic of module instantiation is similar to call-by-reference. For example, in the following program fragment:

MODULE main
...
 VAR
  a : boolean;
  b : foo(a);
...
MODULE foo(x)
 ASSIGN
   x := 1;

the variable a is assigned the value 1. This distinguishes the call-by-reference mechanism from a call-by-value scheme.

Now consider the following program:

MODULE main
...
 DEFINE
   a := 0;
 VAR
   b : bar(a);
...
MODULE bar(x)
 DEFINE
   a := 1;
   y := x;

In this program, the value of y is 0. On the other hand, using a call-by-name mechanism, the value of y would be 1, since a would be substituted as an expression for x.

Forward references to module names are allowed, but circular references are not, and result in an error.