1 Basic Concepts |

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**
[GB92] (some category-theoretic details are
omitted) and

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, withbetween signatures;*morphisms* - a class
**Mod***(Sigma)*of, with*models*between them, for each signature*homomorphisms**Sigma*; - a set
**Sen***(Sigma)*of(or*sentences*), for each signature*axioms**Sigma*; - a relation
, between models and sentences over the same signature; and*satisfaction* - a
, for inferring sentences from sets of sentences.*proof system*

The (loose) ** semantics** of a basic specification is the
class of those models in

A *signature morphism**sigma:Sigma -> Sigma'* determines
a ** translation** function

Mod(sigma)(M')|=S <=> M'|=Sen(sigma)(S).

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.

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 -- Version: 1.0.1 -- 25 March 2001.

Comments to cofi-language@brics.dk

1 Basic Concepts |