**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:

*SP*_{1} **then**...**then** *SP*_{n}

When the current local environment is empty, *SP*_{1} must
determine a complete signature *Sigma*_{1}; otherwise, it must
determine an extension from the local environment to a complete
signature *Sigma*_{1}. For *i=2,...,n* each *SP*_{i} must
determine an extension from *Sigma*_{i-1} to a complete signature
*Sigma*_{i}. The signature determined by the entire extension is then
*Sigma*_{n}.

Similarly, *SP*_{1} determines a class of models *M*_{1} over
*Sigma*_{1}. For *i=2,...,n* each *SP*_{i} determines the class
*M*_{i} of those models over *Sigma*_{i} whose reducts to *Sigma*_{i-1}
are in *M*_{i-1}. The class of models determined by the entire
extension is then *M*_{n}.

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

CoFI
Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk