6.2 Proposal of an Abstract Datatype REAL

The notions screen and rounding - see the last subsection - lead to a specification AbstractExecutableReal in between the mathematical concept of real numbers and the datatype REAL of a programming language. The phrase "abstract" means that this datatype is conceptual on the mathematical side: it is defined in the abstract terms of a screen and a rounding. The phrase "executable" indicates that we assume it to be "near" the datatype REAL of a programming language.

The main idea of AbstractExecutableReal is to use a rounding to define an operation on a screen in terms of an operation on the real numbers: Let ° : R^* ×R^* -> R^* be a binary operation, let r: R^* -> S^* be a rounding. Then we obtain by

forall x,y e S^*: x ° _r y := r(x ° y) (RG)

It is important to note that the screens in ScreenAndRounding and thus in AbstractExecutableReal can be finite or infinite (even not countable).

spec

 ScreenAndRounding =

CompactBasicReal

then

sort

CompactS < CompactReal

op

round: CompactReal -> CompactS

then

SigOrder with Elem ^_|-> CompactS

then

var

r: CompactReal

%%

CompactS is a screen on CompactReal:

.

exists glb: CompactS . (glb < r /\ forall s: CompactS . (s < r => s < glb))

.

exists lub: CompactS . (r < lub /\ forall s: CompactS . (r < s => lub < s))

var

r, r': CompactReal; s: CompactS

%%

round has the projection property:

.

round(s) = s

%%

round is monotone:

.

r < r' => round(r) < round(r')

end

spec

 AbstractExecutableReal

[ScreenAndRounding with

sort CompactS,

preds __ < __, __ > __, __<__, __ > __,

op round ]

given CompactBasicReal =

CompactBasicReal

then

type

Screen::= compactSToScreen(screenToCompactS: CompactS)

var

s:Screen

.

compactSToScreen (screenToCompactS(s)) = s

%%

the other direction -

%%

screenToCompactS(compactSToSecreen(x)) = x

%%

- is provided by the semantics of the type construct.

ops

+__, -__:	Screen -> Screen;
__ + __, __ - __, __ * __:	Screen × Screen -> Screen;
__ / __:	Screen × Screen ->? Screen;

var

x,y: Screen

.

+ x = compactSToScreen(round(screenToCompactS(x)))

.

- x = compactSToScreen(round(screenToCompactS(x)))

.

x + y =

compactSToScreen(round(

screenToCompactS(x) + screenToCompactS(y)))

.

x - y =

compactSToScreen(round(

screenToCompactS(x) - screenToCompactS(y)))

.

x * y =

compactSToScreen(round(

screenToCompactS(x) * screenToCompactS(y)))

.

x / y =

compactSToScreen(round(

screenToCompactS(x) / screenToCompactS(y)))

end