This section describes the abstract syntax and intended interpretation of the language constructs for structured specifications, extending that given for basic specifications in Part I.
The summary below indicates when structured specifications are well-formed, and how their signatures and classes of models are determined by those of their component specifications. Thus the interpretation is essentially based on models, rather than on a reduction to sets of sentences.
A structured specification can only be well-formed when all its component specifications are well-formed.
[HB] Is there a way to name a non-generic specification other than using a SPEC-DEFN with an empty OF-SPEC list, see a later section? ([AT] No, but it should be stated explicitly somewhere that this is the way to do it.)
Discharged: This is the only way to do it, and this should be mentioned. Adjust wording