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.
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*.
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.
BASIC-SPEC ::= basic-spec BASIC-ITEM*
[DTS]
Not even the same axiom? Or the same sort-generating constraint?
What does "same" mean for these -- are two logically equivalent
axioms the same? What about axioms that are logically equivalent
under the assumption that all the other axioms are satisfied?
What about variable declarations?
(This restriction just applies to SIG-DECLs.)
Discharged:
The restriction is eliminated, making the question redundant.
[DTS]
When the BASIC-SPEC is used in an enrichment
of another specification, does this restriction apply to the whole
enriched specification and not just the enrichment, so e.g. it is
also forbidden for an sort in the specification being enriched to be
re-declared in the enrichment?
(Yes)
Discharged:
The restriction is eliminated, making the question redundant.
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.
Discharged:
We now unfortunately allow non-linear visibility because some people
think that it might conceivably save somebody somewhere a couple
of keystrokes someday. :-)
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
BASIC-ITEM ::= SIG-DECL | VAR-DECL | AXIOM| SORT-GEN
[HB,DTS,AT]
That is, in the later axioms
Discharged:
No, because of non-linear visibility.
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.
CoFI
Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk