Up Next
Go up to 6.1 Structured Specifications
Go forward to 6.1.2 Reductions

6.1.1 Translations

  TRANSLATION      ::= translation SPEC RENAMING
  RENAMING         ::= renaming  SYMB-MAP-ITEMS+

A translation is written:

SP with SM
Symbol mappings SM are described in Section 6.4.

The symbols mapped by SM must be among those declared by SP. The signature Sigma given by SP and the mapping SM then determine a signature morphism to a signature Sigma', as explained in Chapter 5. The morphism must not affect the symbols already declared in the local environment, which is passed unchanged to SP.

The class of models of the translation consists exactly of those models over Sigma' whose reducts along the morphism are models of SP.

When the symbol mapping SM is simply a list of identity maps (which may be abbreviated to a simple list of symbols) the only effect of the translation on the semantics of SP is to require that the symbols listed are indeed included in the signature given by SP, otherwise the translation is not well-formed.


CoFI Document: CASL/Summary --Version 0.99-- 21 April 1998.
Comments to cofi-language@brics.dk

Up Next