module

        module stack            % Implements a LIFO list of strings
            export push, pop
        
            var top : int := 0
            var contents : array 1 .. 100 of string
        
            procedure push ( s : string )
                top := top + 1
                contents ( top ) := s
            end push
        
            procedure pop ( var s : string )
                s := contents ( top )
                top := top - 1
            end pop
        end stack
        
        stack . push ( "Harvey" )
        var name : string
        stack . pop ( name )        % This sets name to Harvey

A module declaration is executed (it is initialized) by executing its declarations and statements. For example, the stack module is initialized by setting the top variable to 0. This initialization executes all the statements and declarations in the module that are not contained in procedures or functions. The initialization is completed before any procedure or function of the module can be called from outside the module. An exported subprogram must not be called until initialization of the module is complete.

A call to an exported procedure or function from outside the module executes the body of that procedure or function (the module is not initialized with each such call). See also monitor and class declarations.

The import list gives the names of items declared outside the module that can be accessed inside the module. Since stack has no import list, it is not allowed to access any names declared outside of it. See also import lists. Separately-compiled units that are imported are initialized before the importing unit.

The export list is used to implement information hiding, which isolates implementation details inside the module. The export list gives the names of items declared inside the module that can be used outside the module. For example, push and pop are exported from stack. Each such use of an exported item must be preceded by the module name and a dot, for example, stack.push. (See unqualified for advice on how to avoid using the prefix "stack."). Names that are not exported, such as top and contents, cannot be accessed outside the module.

Procedures, functions, variables, constants and types can be exported; modules, monitors or classes cannot be exported.

A class is essentially a template for creating individual modules (objects). See class for details. A monitor is essentially a module in which only one process can be active at a time. See monitor and process for details.

The opaque keyword is used (only) in export lists to precede exported type names that have declarations in the module. Outside of the module, the type will be distinct from all others types. This means, for example, that if the opaque type is a record, its fields cannot be accessed outside of the module. Opaque types are used to guarantee that certain items are inspected and manipulated in only one place, namely, inside the module. These types are sometimes called abstract data types. See also export lists, which also describes unqualified and pervasive exports.

Implement and implement-by lists are used to separate a module's interface from its body. This allows only a part of a module (its interface) to be visible to its users (its importers), while hiding its implementation. See implement and implement by lists.

        module complex
            export opaque value, constant, add,
                            … other operations …
            type value :
                record
                    realPt, imagPt : real
                end record
        
            function constant (realPt, imagPt: real ) : value
                var answer : value
                answer . realPt := realPt
                answer . imagPt := imagPt
                result answer
            end constant
        
            function add (L, R : value ) : value
                var answer : value
                answer . realPt := L . realPt + R . realPt
                answer . imagPt := L . imagPt + R . imagPt
                result answer
            end add
        
        … other operations for complex arithmetic go here …
        end complex
        
        var c,d : complex .value :=complex.constant ( 1, 5 ) 
                % c and d become the complex number (1,5)
        var e : complex .value := complex.add (c, d )
                % e becomes the complex number (2,10)

The syntax of a moduleDeclaration presented above has been simplified by leaving out pre, invariant and post clauses; the full syntax is:

        module id
            [ implement implementItem ]
            [ implement by implementByItem ]
            [ import [ var ] importItem {, [ var ] importItem } ]
            [ export [ howExport ] id {, [ howExport ] id } ]
            [ pre trueFalseExpn ]
            statementsAndDeclarations
            [ invariant trueFalseExpn ]
            statementsAndDeclarations
            [ post trueFalseExpn ]
        end id