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.