| | | Semantics |
The formal semantics of Casl, which is complete but whose presentation still requires some polishing, is given in [17]. The semantics is divided into the same parts as the language definition (basic specifications, structured specifications, etc.); each part is split further into static semantics and model semantics.
The static semantics checks well-formedness of phrases and produces a `syntactic' object as result, failing to produce any result for ill-formed phrases. For example, for a basic specification the static semantics yields a theory presentation containing the sorts, function symbols, predicate symbols and axioms that belong to the specification. (Actually it yields an enrichment: when a basic specification is used to extend an existing specification it may refer to sorts, functions and predicates from the local environment.) A phrase may be ill-formed because it makes reference to non-existent identifiers or because it contains a sub-phrase that fails to type check.
The model semantics provides the corresponding model-theoretic part of the semantics, and is intended to be applied only to phrases that are well-formed according to the static semantics. A statically well-formed phrase may still be ill-formed according to the model semantics: for example, if a generic specification is instantiated with an argument specification that has an appropriate signature but which has models that fail to satisfy the axioms in the parameter specification, then the result is undefined. The judgements of the static and model semantics are defined inductively by means of rules in the style of Natural Semantics.
The orthogonality of basic specifications in Casl with respect to the rest of the language is reflected in the semantics by the use of a variant of the notion of institution [21] called an institution with symbols [35]. The semantics of basic specifications introduces a particular institution with symbols, and the rest of the semantics is based on an arbitrary institution with symbols.
The semantics provides a basis for the development of a proof system for Casl. As usual, at least three levels are needed: proving consequences of sets of axioms; proving consequences of structured specifications; and finally, proving the refinement relation between structured specifications. The semantics of Casl gives a reference point for checking the soundness of each of the proposed proof systems and for studying their completeness.
Apart from polishing the full semantics of Casl and from consideration of the semantics of sublanguages and extensions of Casl, the development of a proof system for Casl is the main work remaining for the semantics task group.
| | | Semantics |