2.2 Naming Conventions for Specifications in Note M-6

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.

The Prefix "Generate".

For generated datatypes we make it a principle in Note M-6 [RM99a] to write two distinct specifications:

• The first specification is only concerned with the generation of the sorts. This is made explicit by the name of the specification: GenerateDatatypeX.
• The second specification DatatypeX, which imports the specification GenerateDatatypeX, is then devoted to the definition (typically using a definitional extension) of those predicates and operations that are not needed for sort generation.

The Prefix "Define".

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.