Prev Up Next
Go backward to 6.1.3 Unions
Go up to 6.1 Structured Specifications
Go forward to 6.1.5 Free Specifications

6.1.4 Extensions

  EXTENSION        ::= extension SPEC+

An extension is written:

SP1 then ... then SPn

When the current local environment is empty, SP1 must determine a complete signature Sigma1; otherwise, it must determine an extension from the local environment to a complete signature Sigma1. For i=2,...,n each SPi must determine an extension from Sigmai-1 to a complete signature Sigmai. The signature determined by the entire extension is then Sigman.

Similarly, SP1 determines a class of models M1 over Sigma1. For i=2,...,n each SPi determines the class Mi of those models over Sigmai whose reducts to Sigmai-1 are in Mi-1. The class of models determined by the entire extension is then Mn.

An annotation is to be provided for indicating that a series of extensions is conservative, i.e., every model in Mi-1 is the reduct of some model in Mi, for i=2,...,n.


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

Prev Up Next