We propose two different semantic annotations on extensions, namely %def (for "definitionally") and %cons (for "conservatively"). A discussion of the rôle of conservative and definitional extensions and further references can be found in [Mai97]. Semantically, a conservative extension
means that each model of the specification SP_{1} can be extended to a model of the specification (SP_{1} then SP_{2}). This implies that all SP_{1}-sentences that follow from (SP_{1} then SP_{2}) already follow from SP_{1}, i.e. semantical consequence is conserved^{1}.
SP_{1} then %cons SP_{2}
In case of a definitional extension
we require that each model of SP_{1} can be uniquely extended^{2} to a model of (SP_{1} then SP_{2}).
SP_{1} then %def SP_{2}
Both annotations are also possible at the beginning of the body of a named parameterized specifications, since the body is an extension of the parameters:^{3}
and
SP [SP_{1}] ... [SP_{n}] = %cons BODY
SP [SP_{1}] ... [SP_{n}] = %def BODY
The typical example for a definitional extension is the introduction of derived operations or predicates. Consider e.g. the partial order < in the specification BooleanAlgebra of [RM99]:
0:Elem; | |
1:Elem; | |
__ |¯| __: | Elem ×Elem -> Elem, |
assoc, comm, unit 1; | |
__ |_| __: | Elem ×Elem -> Elem, |
assoc, comm, unit 0; |
The laws on the operations 0,1, |_| , |¯| in the specification
DefineBooleanAlgebra describe a class
of models (boolean algebras), which are all partially ordered in a
canonical way. Thus, in
BooleanAlgebra the partial order can
be defined in terms of the operations of boolean algebras, and there
is a unique choice for the extension of a boolean algebra to a
partially ordered boolean algebra.
Another aspect of the annotation %def arises in combination with a view. It is an established principle in mathematics to define an abstract concept like a Boolean algebra in terms of the weakest possible axioms. This makes it easy to prove that a concrete structure like the powerset of a set is an instance of an abstract concept. In CASL the property "to be an instance of" is expressed by a view. Thus on the one hand we would like to have a view from the specification BooleanAlgebra to the specification FinitePowerSet (see [RM99] for this specification) where the proof obligations only have to deal with the axioms that define a Boolean algebra, i.e. the derived predicate < is out of scope. On the other hand, having established this view we would like to speak about a partial order in the specification FinitePowerSet, which arises "automatically" from this view.
We suggest to reflect this idea in CASL as follows. As a view from SP_{1} to SP_{2} has to map all symbols of SP_{1} on symbols of SP_{2}, we split the specification of a Boolean algebra in two parts: the specification DefineBooleanAlgebra introduces only the operations 0,1, |_| , |¯| and their axioms, while the specification BooleanAlgebra extends the former definitionally by the predicate < (see above). Then we relate the specifications DefineBooleanAlgebra and FinitePowerSet by a view:
0 ^{|}-> {}, |
1 ^{|}-> X, |
__ |¯| __ ^{|}-> __ n __, |
__ |_| __ ^{|}-> __ u __ |
A main use of the annotation %cons is to specify those intended consequences^{4} which should follow, in the specifier's view, from the specification. This can help in detecting errors in the specification, namely in those cases where the intended consequences actually do not follow from the specification. For example, look at the specification FiniteSet from [RM99]:
Another example for the annotation %cons is the above discussed specification FinitePowerSet_with_BooleanAlgebra. As we mentioned in this specification the partial order < is not related with set inclusion c , although these predicates are equivalent. Thus we could add this property using a conservative extension:
In some cases, it is more convenient to use a view to specify intended consequences. For example, to state that the specification BOOLEAN of [RM99]
NOT__ : | Boolean -> Boolean; |
__AND__, __OR__ : | Boolean ×Boolean -> Boolean, |