Prev Up Next
Go backward to I Basic Specifications
Go up to Top
Go forward to 2 Basic Constructs

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 (some category-theoretic details are omitted) and proof systems.

A  basic specification framework may be characterized by:

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 with  linear visibility, where symbols may not be used before they have been declared; or it may be the entire signature, reflecting  non-linear visibility.

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).1 Satisfaction is required to be preserved by translation: for all in Sen(Sigma), M' in 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 considers many-sorted basic specifications of the CASL specification framework, and indicates the underlying signatures, models, and sentences.2 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.

  • 1.1 Signatures
  • 1.2 Models
  • 1.3 Sentences
  • 1.4 Satisfaction

  • CoFI Document: CASL/Summary --Version 0.99-- 21 April 1998.
    Comments to cofi-language@brics.dk

    Prev Up Next