Go backward to Part I: Basic Specifications:
Go up to Top
Go forward to Basic Constructs

Basic Concepts

First, here is an brief reminder of how specification frameworks 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 symbols 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 |= of satisfaction, between models and sentences over the same signature; and
a proof system, for inferring sentences from sets of sentences.

A basic specification consists of a signature Sigma together with a set of sentences from Sen(Sigma). The signature provided for a particular sentence in a specification is called its local environment. (It may be a restriction of the entire signature of the specification, e.g., determined by an order of presentation for the signature declarations and the 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). Satisfaction is required to be preserved by translation: for all S e Sen(Sigma), M' e Mod(Sigma'),

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 section indicates the underlying signatures, models, sentences, and proof system for many-sorted basic specifications of the CASL specification framework; the extra components concerned with subsorts are deferred to a later section. The abstract syntax of the language constructs used for many-sorted basic specifications is described in the next section, with subsorting constructs deferred to a later section. 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 Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk