The prefixes "Generate" and "Define" in the above listed specification names indicate that different aspects of one datatype are separated from each other into two specifications. We adopt the underlying rules of methodology also in this note.
For generated datatypes we make it a principle in Note M-6 [RM99a] to write two distinct specifications:
If we wish to instantiate a definitional extension of an abstract theory along a view, we split the specification of the abstract concept (e.g. group) again into two parts: the specification DefineGroup includes everything what one needs to define a group, i.e. an associative operation + and a unit 0 such that for all elements x there exists an element x' with x + x' = 0 /\ x' + x = 0 . The specification Group is parameterised by DefineGroup and extends DefineGroup definitionally: here we introduce a map inv that assigns to any element its inverse and the operation - as x-y=x+inv(y). Now if we want to state that Int is a group, we can define a view from DefineGroup to Int. If we now instantiate Group with this view, we automatically get the derived group operations also for Int.