This section indicates the abstract and concrete syntax of the constructs of many-sorted basic specifications, and describes their intended interpretation.
For an introduction to the form of grammar used here to define the abstract syntax of language constructs, see Appendix A, which also provides the complete grammar defining the abstract syntax of the entire CASL specification language.
BASIC-SPEC ::= basic-spec BASIC-ITEMS*
A well-formed many-sorted basic specification BASIC-SPEC in the CASL language is written simply as a sequence of BASIC-ITEMS constructs:
BI1...BInThe empty basic specification is not usually needed, but can be written `{ }'.
This language construct determines a basic specification of the underlying many-sorted institution, consisting of a signature and a set of sentences of the form described in Chapter 1. The models of this signature and set of sentences provide the semantics of the basic specification. Thus this section explains well-formedness of basic specifications, and the way that they determine the underlying signatures and sentences, rather than directly explaining the intended interpretation of the constructs.
While well-formedness of terms of the language can be checked statically, the question of whether the value of a well-formed term is necessarily defined in all models or not may depend on the specified axioms (and it is not decidable in general).
BASIC-ITEMS ::= SIG-ITEMS | FREE-DATATYPE | SORT-GEN
| VAR-ITEMS | LOCAL-VAR-AXIOMS | AXIOM-ITEMS
A BASIC-ITEMS construct is always a list, written:
plural-keyword X1; ... Xn;The plural-keyword may also be written in the singular (regardless of the number of items), and the final `;' may be omitted.
Each BASIC-ITEMS construct determines part of a signature and/or some sentences (except for VAR-ITEMS, which merely declares some global variables). The order of the basic items is generally significant: there is linear visibility of declared symbols and variables in a list of BASIC-ITEMS constructs (except within a list of datatype declarations). Verbatim repetition of the declaration of a symbol does not affect the semantics (some tools may however be able to locate and warn about such duplications, in case they were not intentional).
A list of signature declarations and definitions SIG-ITEMS determines part of a signature and possibly some sentences. A FREE-DATATYPE construct determines part of a signature together with some sentences. A sort-generation construct SORT-GEN determines part of a signature, together with a corresponding sort generation constraint. A list of variable declaration items VAR-ITEMS determines sorted variables that are implicitly universally quantified in the subsequent axioms of the enclosing basic specification; note that variable declarations do not contribute to the signature of the specification in which they occur. A LOCAL-VAR-AXIOMS construct restricts the scope of the variable declarations to the indicated list of axioms. (Variables may also be declared locally in individual axioms, by explicit quantification.) An AXIOM-ITEMS construct determines a set of sentences.