Prev Up Next
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.

The Prefix "Generate".

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

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.

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

Prev Up Next