Introduction to PSF

Imports / Exports

All objects defined in a module are only visible within that module. To make objects specified in one module visible in other modules, PSF uses an import/export mechanism. Every module can have an export and an import section. The layout for these sections of data and process modules is given below.
data module ^Module^
begin
    exports
    begin
        sorts
            ...
        functions
            ...
    end
    imports
        ...
    ...

process module ^Module^
begin
    exports
    begin
        atoms
            ...
        processes
            ...
        sets
            ...
    end
    imports
        ...
    ...

All objects defined in an export section of a module are made visible to modules that import this module. Objects imported by a module are also exported by this module, and thus are visible in other modules that import this module.

The imports section consists of a comma separated list of module names. A data module can only import data modules, and a process module can import both data and process modules.