**Go backward to** 2.1 The Specifications of Note M-6

**Go up to** 2 Basic Datatypes

**Go forward to** 2.3 Representations of Numbers in Note M-6

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

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.

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.

CoFI
Note: M-7 -- Version: 0.2 -- 13 April 1999.

Comments to till@informatik.uni-bremen.de