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.
[TM,DTS,AT] >From here to the start of the next subsection is redundant and partially wrong.
Discharged: Remove it.
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