Footnotes

 

(1)

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.  

(2)

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].  

(3)

Would the annotations also make sense within architectural specifications?  

(4)

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).  

(5)

An Alternative would be to allow the predefined precedences to be overridden. However, we found this too confusing.  

(6)

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].  

(7)

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.  

(8)

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 completeness proof.  

(9)

We omit here the non interesting cases of multiple signs as e.g. -+d₁ :: d₂ :: ...:: d_n.