First, before considering the particular concepts underlying CASL,
here is a brief reminder of how specification frameworks in general
may be formalized in terms of so-called *institutions* (some
category-theoretic details are omitted) and *proof systems*.

A *basic specification framework* may be characterized by:

- a class
**Sig**of*signatures**Sigma*, each determining the set of*symbols**|Sigma|*whose intended interpretation is to be specified, with*morphisms*between signatures; - a class
**Mod***(Sigma)*of*models*, with*homomorphisms*between them, for each signature*Sigma*; - a set
**Sen***(Sigma)*of*sentences*(or*axioms*), for each signature*Sigma*; - a relation
*satisfaction*, between models and sentences over the same signature; and - a
*proof system*, for inferring sentences from sets of sentences.

The (loose) *semantics* of a basic specification is the
class of those models in **Mod***(Sigma)* which satisfy all the
specified sentences. A specification is said to be
*consistent* when there are some models that satisfy all the
sentences, and *inconsistent* when there are no such models.
A sentence is a *consequence* of a basic specification if it
is satisfied in all the models of the specification.

A *signature morphism* *sigma:Sigma -> Sigma'* determines
a *translation* function **Sen***(sigma)* on sentences,
mapping **Sen***(Sigma)* to **Sen***(Sigma')*, and a *reduct*
function **Mod***(sigma)* on models, mapping **Mod***(Sigma')* to
**Mod***(Sigma)*.^{2}
Satisfaction is required to be preserved by translation: for all
*S ***e*** ***Sen***(Sigma), M' ***e*** ***Mod***(Sigma')*,

The proof system is required to be sound, i.e., sentences inferred from a specification are always consequences; moreover, inference is to be preserved by translation.Mod(sigma)(M')|=S <=> M'|=Sen(sigma)(S).

Sentences of basic specifications may include *constraints*
that restrict the class of models, e.g., to reachable ones.

The rest of this chapter considers many-sorted basic specifications of
the CASL specification framework, and indicates the underlying
signatures, models, and sentences.^{3}
Consideration of the extra features concerned with subsorts is
deferred to Chapter 3.

The syntax of the language constructs used for expressing many-sorted basic specifications is described in Chapter 2; subsorting constructs are deferred to Chapter 4. The abstract syntax of any well-formed basic specification determines a signature and a set of sentences, the models of which provide the semantics of the basic specification.

CoFI Document: CASL/Summary-v1.0 -- Version: 1.0 -- 22 October 1998.

Comments to cofi-language@brics.dk