This section provides the abstract syntax and determines the intended interpretation of the constructs on subsorted basic specifications, extending what was provided for many-sorted specifications in a preceding section.
A well-formed subsorted basic specification BASIC-SPEC of the CASL language determines a basic specification of the underlying subsorted institution, consisting of a subsorted 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.
A subsort declaration SUBSORT-DECL determines a
contribution to the subsort embedding pre-order of a subsorted
signature. A predicative subsort definition PRED-SORT-DEFN
determines a subsort and its embedding in another sort, together with
a sentence that characterizes the values of the subsort.
BASIC-ITEM ::= ... | SUBSORT-DECL | PRED-SORT-DEFN
CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk