Go backward to 3 Rôle of conservative extension
Go up to Top
Go forward to Footnotes

4 Complexity of specification expressions

The following is an attempt to provide hints how complex a specification expressions needs to be. Note that the complexity of a specification expression depends on where the specification expression is used, for example, as a part of an extension, as a named specification, in the local part of a local specification etc.

Name = cons-ext 
          Import1
          (extension 
             Import2
             (local-spec 
                (cons-ext
                   Import1'
                   (extension
                      Import2'
                      BASIC-SPEC))
                Sp))

Import is the union of possibly translated named specifications or instantiations. The specification Import1 is protected, while the specification Import2 can be refined. Sp is either a list of basic items or a conservative extension, where the sub-specifications are basic specifications.

CoFI Note: M-1 --0.1-- 18 Sep 1997.
Comments to hubert@mpi-sb.mpg.de