Go backward to References
Go up to Top
- Note that model-theoretic conservativeness of an
extension implies consequence-theoretic conservativeness, but not vice
versa, see [Vel92]. However, if we consider the consequence
relation between specifications, model-theoretic and consequence-theoretic
conservativeness become equivalent.
- Technically, this means
that the reduct functor is bijective on objects, i.e. both
specifications have the "same" model class. An abstract
axiomatization of definitional extensions
can be found in [Sri97].
- Would the annotations also make sense within architectural
- We do not propose an annotation
for intended consequences as in the Larch Shared Language
[GHG+93], since we think it is better
to include the intended consequences in the specification,
and use a %cons annotation to express
that they follow already from the rest of the specification
(namely the part that is being extended).
- An Alternative would be to allow the predefined precedences
to be overridden. However, we found this too confusing.
- There are
no built-in precedences for particular operation symbols. The usual
precedences between the arithmetic operations are defined in the
standard library for numbers [RM99].
- Note that the sort List[Elem] in
the type construct of the specification
List is already generated. Of
course one can mix up sort generation and the brackets
declaration in principle.
- This problem can
be overcome by allowing views to specify derived specification
morphisms, as in OBJ3, where constants may be mapped to terms.
One objection against derived signature morphisms has been that
the corresponding category is not cocomplete. However, if we
consider the category of derived specification morphisms, we
can retain cocompleteness, see [Sri97] for a
- We omit here the non interesting
cases of multiple signs as e.g. -+d1 :: d2 :: ...:: dn.
Note: L-11 -- Version: 0.1 -- 11 March 1999.
Comments to email@example.com