2 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 order of the basic items is insignificant, i.e., there is non-linear visibility of symbols in lists BASIC-ITEM*.

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

A signature declaration SIG-DECL determines part of a signature and possibly some sentences. 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. A sort-generation construct SORT-GEN determines part of a signature, together with a corresponding sort generation constraint. A local basic specification LOCAL-BASIC-SPEC restricts the visibility of the part of a signature determined by one list of basic items to another such list.

2.1 Signature Declarations

2.2 Variable Declarations

2.3 Axioms and Terms

2.4 Sort Generation

2.5 Local Basic Specifications

---

CoFI Document: CASL/Summary-v0.97 --Version 0.97-- 20 May 1997.
Comments to cofi-language@brics.dk