Go backward to 4.1 Pragmatic Issues
Go up to 4 Structured Specifications
Go forward to 4.3 Language Constructs

4.2 Semantic Concepts

The notions of signature and class of models are the same as for basic specifications. In fact the structuring part of CASL is (essentially) independent of the details of basic specification: the same structuring may be used regardless of whether basic specifications are restricted (e.g., by eliminating partial functions, subsorts, predicates, or explicit quantifiers) or extended (e.g., to higher-order functions). The reduct homomorphisms induced by signature morphisms in the institution for basic specifications are especially significant in the semantics of structured specifications.

In a specification, the so-called local environment records the symbol declarations that are currently visible. For basic specifications, visibility is linear (except within lists of datatype declarations) so the local environment merely grows as one proceeds through the declarations. For structured specifications, however, the local environments at different places may be completely unrelated.

Semantic Functions:

Structured specifications can have arbitrarily deep structure, and a compositional semantics is appropriate: the denotation of a construct is determined entirely by the denotations of its components. The denotation of a self-contained specification is a signature and class of models for that signature. The denotation of a part that extends a self-contained specification is a (partial) function from signatures to extended signatures, and from corresponding model classes to extended-model classes.


CoFI Document: CASL/GuidedTour -- Version: 1 -- July 1999.
Comments to pdmosses@brics.dk

Go backward to 4.1 Pragmatic Issues
Go up to 4 Structured Specifications
Go forward to 4.3 Language Constructs