Footnotes

 (1)

For example, predicates hold minimally in initial models.

 (2)

CASL also allows sorts to be declared as isomorphic, with mutual subsort embeddings.

 (3)

An annotation is an auxiliary part of a specification, for use by tools, and not affecting the semantics of the specification.

 (4)

Constructors can also be partial.

 (5)

If conservative extension were to be a construct of the language, its semantics would be the same as for ordinary extension whenever the specified extension happened to be conservative, and otherwise undefined.