The PASP Translator
The PASP Translator is invoked from the PASP
Translators Environment and is applicable to all implementations
which are currently analysed, but
not translated.
Overview
Since the scoping rules of AMN
are different (less strict) from those of PASP, we allow PASP developments
to use the scoping rules of the former, and make the PASP translation a
multi-stage process to enable `incomplete' PASP modules to play a transitory
role; this allows the use of `parameterised' constructs.
The sharing of contextual information (through the AMN SEES
and USES clauses) also
falls naturally into this scheme and permits, for example, the use of abstract
sets and constants
in a layered development which are accorded PASP types and given values
at the implementation stage by the module `owning' the set or constant.
The latter leads to the re-declaration of constants by modules using
but not owning them; however since all such declarations will be identical
throughout the development this presents no problem.
The PASP Translator translates an IMPLEMENTATION
into a PASP module; a prerequisite for translation is that the implementation
and all subordinate implementations are analysed;
Subordinate implementations that are analysed but not yet translated are
translated first.
Note that, an IMPLEMENTATION
has no variables of its own which are global to all operations (e.g. the
VARIABLES clause is not allowed). All static data (information global to
the module) or persistent data (information which survives from one invocation
of the module to the next) must be held within other machines which the
implementation IMPORTS.
In the B-Toolkit environment there is a selection of such pre-defined machines.
The pre-defined machines are held in the
System Library and can
be introduced into a development by using the `Introduce
construct from SLIB' facility.
Stage 1: Translation (trl)
If the specification `module.mch' is implemented by `prog.imp', then translation
of the latter will produce the file `module.param',written to the CDE/PASP
directory.
`module.param' is thus an incomplete PASP module in which formal parameters
of the construct (if any) appear unset; each AMN implementation is translated
in this manner.
Stage 2: Instantiation of Parameters (ipm)
This second-stage translation is invoked only for the top-level unparameterised
MAIN module, which should comprise a single operation called MAIN, which
should also be unparamererised. All subsidiary modules are automatically
translated, and each subsidiary module needs to be imported (somewhere
in the development) for this translation stage to be successful - i.e.
the development really must be complete.
The file `module.noatt' is created from `module.param', parameters being
replaced by their actual values. Translation is now complete except for
memory attribute information: a template memory map file is automatically
produced at this stage, permitting the setting of memory and read/write
attributes for all global and local variables of the entire development
in one single file (for subsequent use in the next translation phase).
Stage 3: Setting of Attributes (sat)
This third-stage translation is again invoked only for the top-level MAIN
module, with the code `module.pasp' is created from `module.noatt'
by inserting attribute information from the memory map file.
Editing the map file results in the removal of this PASP module, and
so the `sat' button must be invoked each time the map file is edited.
Stage 4: Finalisation of PASP Modules (fin)
This final phase produces a filtered `module.pas' (only those operations
actually employed are included) in the DECCO sub-directory of CDE/PASP.
The memort map file and a link (.lnk) file is also produced.
Hypertext
During each of the four stages a hypertext version of the code module is created and
written to the HTX
directory; this means that each of the files `module.param', `module.noatt',
`module.pasp', `module.pas' and `module.map' exist in hypertext form with links between
each, and back to the AMN implementation `prog.imp'. These may be accessed
through the hypertext tool.
The Translation Process
The PASP Translator translates the following clauses of an IMPLEMENTATION:
-
The MACHINE header clause:
The Translator provides for an implementation of the formal machine
parameters.
-
The IMPORTS clause:
The Translator provides for an implementation which makes instances
of the imported MACHINEs known to this implementation; an imported MACHINE
must be a library (SLIB
machine, a generated
machine (with code module, for example generated through the Enumerator)
or a MACHINE which already has been provided with an IMPLEMENTATION within
the development.
-
The SEES clause:
The Translator provides for an implementation which makes seen MACHINEs
known to the implementation. A seen MACHINE must be a committed construct
which is imported elsewhere, in which case its state is shared between
the machine which imports it and the machine which sees it.
-
The CONSTANTS and PROPERTIES
clauses:
All constants must be given an exact value in the PROPERTIES
clause. The constants and its values are known to all implementation which
SEES or IMPORTS
the MACHINE for which we are providing an implementation. Header information
is generated from this clause.
-
The SETS and PROPERTIES
clauses:
The Translator provides for an implementation of enumerated sets and
deferred sets. The deferred sets must be given an exact value within the
latter clause; however the value is normally a deferred set from an imported
machine. Header information is generated from this clause.
A full on-line help listing is available
in the Contents Page
Also available in the form of a complete
Index.
© B-Core
(UK) Limited, Last updated: 25/08/99