Prev Up Next
Go backward to 6.1.4 Extensions
Go up to 6.1 Structured Specifications
Go forward to 6.1.6 Local Specifications

6.1.5 Free Specifications

      FREE-SPEC ::= free-spec SPEC

A free specification FREE-SPEC is written:

free { SP }
Note that the specification written:
free types DD1; ... DDn;
is parsed as a free datatype of a basic specification--but [CHANGED:] (at least in the framework for basic specifications give in Part I) [] it has the same interpretation as the free structured specification written:
free { types DD1; ... DDn}

When the current local environment is empty, SP must determine a complete signature Sigma; otherwise, it must determine an extension from the local environment to a complete signature Sigma. In both cases, Sigma is the signature determined by the free specification.

When the current local environment is empty, the free specification determines the class of initial models of SP; otherwise, it determines the class of models that are free extensions for SP of their own reducts to models of the current local environment.

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

Prev Up Next