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.