   Go backward to 6.1 Screens and Roundings
Go up to 6 Towards a Datatype REAL
Go forward to 6.3 Proposal of two Executable Datatypes REAL

## 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)
an new operation ° r on the screen. Please note that in general associativity of ° does not imply associativity of ° r. Furthermore addition and multiplication are not distributive.

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

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