Go backward to 3.1 Pragmatic Issues
Go up to 3 Basic Specifications
Go forward to 3.3 Language Constructs
3.2 Semantic Concepts
The essential semantic concepts for basic specifications are
well-known: signatures (of declared symbols), models (interpreting the
declared symbols), and sentences (asserting properties of the
interpretation), with a satisfaction relation between models and sets
of sentences. Defining these (together with some categorical
structure, and such that translation of symbols preserves
satisfaction) provides a so-called institution for basic
specifications.
A well-formed basic specification in CASL determines a signature and a
set of sentences, and hence the class of all models over that
signature which satisfy all the sentences.
Sigma= (S,TF,PF,P, < ):
A signature Sigma for a CASL specification consists of a set of
sorts S, disjoint sets TF, PF of total and partial operation
symbols (for each profile of argument and result sorts), a set of
predicate symbols P (for each profile of argument sorts), and a
partial order of subsort embeddings < . The same symbol may be
overloaded, with more than one profile; there are no conditions on the
relationship between overloading and subsorts, and both so-called
ad-hoc overloading and subsort overloading are allowed.
M e Mod(Sigma):
A model M provides a non-empty carrier set for each sort in S, a
partial function for each operation symbol in PF u TF (for each
of its profiles), a relation for each predicate symbol in P (for
each of its profiles), and an embedding for each pair of sorts related
by < . The interpretation of an operation symbol in TF has to
be a total function. Moreover, embedding and overloading have to be
compatible: embeddings commute with overloaded operations.
Phi e Sen(Sigma):
A sentence Phi is generally a closed, many-sorted first-order
formula. The atomic formulae in it may be equations (strong or
existential), definedness and (subsort) membership assertions, and
fully-qualified predicate applications. The terms in atomic formulae
may be fully-qualified operation applications, variables,
explicitly-sorted terms (interpreted as subsort embeddings) or casts
(interpreted as projection onto subsorts).
M |- Phi: The satisfaction of a
closed first-order formula Phi in a model M is as usual regarding
quantifiers and logical connectives; it involves the holding of open
formulae, and the values of terms, relative to assignments of values
to variables.
The value of a term may be undefined when it involves the application
of a partial operation symbol (or a cast). When the value of any
argument term is undefined, the application of a predicate never
holds, and the application of an operation is always undefined (as
usual in partial algebra). Definedness of terms also affects the
holding of atomic formulae: an existential equation holds when both
terms are defined and equal, whereas a strong equation holds when they
are both undefined, or defined and equal.
(S',F') c (S,F), where F = TF u PF: A sort generation
constraint is treated as a further kind of sentence. It is satisfied
in a model when the carriers of sorts in S' are generated by
functions in F' (possibly from sorts in S \ S').
The institution for basic specifications in CASL is given by equipping
signatures with morphisms, and models with homomorphisms. A signature
morphism sigma from Sigma to Sigma' preserves overloading,
embeddings, and totality of operation symbols. A homomorphism h: M1
-> M2 (M1, M2 e Mod(Sigma)) preserves operation values
(including definedness), and the holding predicates.
A signature morphism sigma from Sigma to Sigma' determines a
translation of sentences from Sen(Sigma) to Sen(Sigma'), and a
reduct functor Mod(sigma): Mod(Sigma') -> Mod(Sigma).
Translation preserves satisfaction: M' |- sigma(Phi) iff
Mod(sigma)(M') |- Phi.
Whereas applications of predicates and operations in the atomic
formulae and terms of the CASL institution are fully qualified
by their profiles, basic specifications in the CASL language
allow the profiles to be omitted (since they are usually evident from
the context). In general, there may be many ways--but possibly none
at all--of expanding an atomic formula in CASL by inserting profiles
to give a well-sorted fully-qualified atom for constructing a sentence
of the underlying institution. The atomic formula is deemed to be
well-formed when its expansion is unique (up to the commuting of
embeddings with overloaded operations); the axioms of a well-formed
basic specification determine a set of sentences of the CASL institution.
In fact the subsorted CASL institution outlined above may be reduced
to an ordinary many-sorted CASL institution, by replacing subsort
inclusion by explicit embeddings: Sigma= (S,TF,PF,P, < ) reduces
to Sigma# = (S,TF u Emb,PF u Proj,P u Memb) where Emb =
{embs,s' | s < s'} is a set of total operation symbols for
subsort embeddings, and the sets Proj (of projections onto subsorts)
and Memb (of subsort membership predicates) are defined similarly.
The semantics of a well-formed basic specification in CASL is given by
a signature Sigma together with the class of those models M e Mod(Sigma) that satisfy all the sentences determined by the
specification.
CoFI
Document: CASL/GuidedTour -- Version: 1 -- July 1999.
Comments to pdmosses@brics.dk
Go backward to 3.1 Pragmatic Issues
Go up to 3 Basic Specifications
Go forward to 3.3 Language Constructs