Go backward to 4.2 Union and Extension
Go up to 4 Structured Specifications
Go forward to 4.4 Naming and Generics
4.3 Initiality and Freeness
Specifications generally have loose semantics: all models of
the declared symbols that enjoy the specified properties are allowed.
However, it may also be specified that only initial models of the
specification are allowed.
In general, initial models of CASL specifications need not exist,
due to the possibility of axioms involving disjunction, negation, and
existential quantification.
When they do exist, the CASL construct for restricting models to
the initial ones can be used, ensuring reachability--and also that
atomic formulae (equations, definedness assertions, predicate
applications) are as false as possible. The latter aspect is
particularly convenient when specifying (e.g., transition) relations
`inductively', as it would be tedious to have to specify all the cases
when a relation is not to hold, as well as those where it
should hold.
Specifications with loose and initial semantics may be combined
and extended, and extensions may be required to be free.
For generality, CASL allows specifications with initial semantics
to be united with those having loose semantics. This applies also to
extensions: the specifications being extended may be either loose or
free, and the extending part may be required to be a free extension,
which is a natural generalization of the notion of initiality.
CoFI
Document: CASL/Rationale --Version 0.97-- 20 May 1997.
Comments to cofi-language@brics.dk