Appendix: Changes from version 0.98

The main changes are as follows:

BASIC-ITEMS, SORT-GEN-ITEMS:

The abstract syntax now reflects the grouping of basic items of the same kind (sorts, operations, predicates, variables, axioms).

Visibility:

The semantics now enforces linear visibility in lists of basic items, everywhere except within lists of datatype declarations. Also, subsort (and isomorphic sort) declarations now declare all the mentioned sorts.

FREE-DATATYPE:

This construct has been added; there are to be some restrictions on the DATATYPE-DECLs used in it, such that its models are the same as with a corresponding FREE-SPEC (but these restrictions are not reflected by the grammar).

LOCAL-VARS-AXIOMS:

This construct for declaring variables local to a group of axioms has been added.

UNIT-OP-ATTR:

The unit may now be any TERM, not just a (constant) OP-NAME.

ALTERNATIVE:

There is now explicit indication of totality/partiality of constructors and selectors.

PRED-SYMB, OP-SYMB, SYMB:

The grammar here has merely been reorganized, to avoid superfluous ambiguity.

VAR:

The distinction between a constant and a variable in a term is context-dependent, in general, and no longer assumed by the abstract syntax. A constant can be indicated using a qualified operation name; an analogous qualification has been added for indicating variables.

SUBSORTS:

More than one subsort can now be given in a single ALTERNATIVE.

ISO-DECL:

This now has a single (list) component.

TRANSLATION:

A construct for requiring symbols to be declared by a (referenced) specification, without hiding the other symbols, has been added. Required symbols are simply renamed to themselves.

REDUCTION:

The SPEC is now the first component, and the revealing case has been generalized to allow translation of the revealed symbols.

SYMB-ITEMS, SYMB-MAP-ITEMS, SYMB-OR-MAP-ITEMS:

The kind of the symbols in such a list can now also be indicated explicitly, as well as being left implicit.

CONS-EXTN:

Conservativeness is now allowed only an annotation--so the semantics no longer takes account of whether an extension is conservative.

GEN-SPEC:

IMPORTS have been added, and the body is now a single SPEC.

GEN-SPEC-INST:

The overall symbol mapping has been removed.

VIEW, FIT-ARG:

Constructs for defining views (specification morphisms) and using them in generic instantiations have been added, according to the revised proposal resulting from the discussion on the language design mailing list.

ARCH-SPEC:

The new grammar here corresponds closely to that proposed in Note M-4.

LIB-NAME:

This replaces the URL. The LIB-NAME is to be interpreted relative to a map from LIB-NAMEs to physical URLs of libraries. Global LIB-IDs identify registered libraries, whereas local LIB-IDs identify local, perhaps unregistered, libraries. The list of SIMPLE-IDs may be interpreted as a path in a file system. The lack of a VERSION indicates the latest version of the library concerned. (The syntax of VERSION has not yet been decided.)

ITEM-NAME-OR-MAP:

The grammar has merely been reorganized.