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
!                    |  DATATYPE-DECL | ATTRIBUTION

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. A DATATYPE-DECL determines part of a signature (a sort, together with some constructor and selector functions), as well as some sentences (defining the values of the selectors). An ATTRIBUTION determines just some sentences (asserting properties such as associativity and commutativity of particular functions).

Signature Declarations

Variable Declarations

Axioms and Terms

Sort Generation

Datatype Declarations

Attributions

---

CoFI Document: LanguageSummary --DRAFT, Version 0.96-- 30 April 1997.
Comments to cofi-language@brics.dk