Basic Constructs

This section provides the abstract syntax and determines the intended interpretation of the constructs of many-sorted basic specifications; constructs concerned with subsorts are deferred to a later section. For an introduction to the form of abstract syntax used to indicate constructs in this document, see Appendix A, which also collects together the abstract syntax of the entire CASL specification language. In later sections, an elided (...) alternative in the grammar indicates that the enclosing production is extending a production given earlier for the same sort of construct.

BASIC-SPEC      ::=   basic-spec BASIC-ITEM*

A  well-formed many-sorted basic specification BASIC-SPEC of the CASL language determines a basic specification of the underlying many-sorted institution, consisting of a signature and a set of sentences of the form described in the preceding section. 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, but in general it does not directly explain the intended interpretation of constructs.

Each BASIC-ITEM (apart from a VAR-DECL) may determine part of a signature and/or some sentences. The parts of signatures determined by the basic items in a basic specification are required to be disjoint; in particular, it is not allowed to specify the same BASIC-ITEM more than once in the same list BASIC-ITEM*. The order of the basic items is significant: all symbols used in a BASIC-ITEM must be in the local environment provided by the preceding BASIC-ITEMs, i.e., linear visibility of symbols.

BASIC-ITEM      ::=   SIG-DECL | VAR-DECL | AXIOM| SORT-GEN

A signature declaration SIG-DECL determines part of a signature. A variable declaration VAR-DECL determines sorted variables that are implicitly universally-quantified in the axioms of the enclosing BASIC-SPEC (variables may also be declared locally, by explicit quantification in axioms). Note that variable declarations do not contribute to the signature of the specification in which they occur. An AXIOM determines a sentence, as does a sort-generation constraint SORT-GEN.

Signature Declarations

Variable Declarations

Axioms and Terms

Sort Generation

---

CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk