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

an new operationforall x,yeS^{*}: 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**

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

Comments to till@informatik.uni-bremen.de