Go backward to 4.4 The Specification BasicReal
Go up to 4 A Specification of Real Numbers

## 4.5 The Specification CompactBasicReal

spec
CompactBasicReal =
BasicReal reveal
 sort Real, preds __ < __, __ > __, __ < __, __ > __, ops __+, __-, __ + __, __ - __, __ * __, __ / __
then
free
type CompactReal ::= sort Real | posInfinity | negInfinity
then
SigOrder with Elem |-> CompactReal
var
r:Real
.
negInfinity < posInfinity
.
r < posInfinity
.
negInfinity < r
then
sorts
 PosCompactReal = {x:CompactReal . x > 0 }; NegCompactReal = {x:CompactReal . x < 0 }
preds
isReal, isInfinity: CompactReal
ops
 +__, -__: CompactReal -> CompactReal; __ + __, __ * __: CompactReal × CompactReal ->? CompactReal, comm; __ - __, __ / __: CompactReal × CompactReal ->? CompactReal;
vars
 r:Real; p: PosCompactReal; n: NegCompactReal; x,y: CompactReal
%%
Defining the sort-predicates:
.
isReal(x) <=> x e Real
.
isInifinite(x) <=> x=posInfinity \/ x=negInfinity
%%
Extending the operations for the new values
%%
negInfinity and posInfinity;
%%
the results of the terms
%%
0/0, infty/infty, 0 * infty, infty-infty
%%
are undefined:
.
+ negInfinity = negInfinity
.
+ posInfinity = posInfinity
.
- negInfinity = posInfinity
.
- posInfinity = negInfinity
.
r + posInfinity = posInfinity
.
r + negInfinity = negInfinity
.
posInfinity + posInfinity = posInfinity
.
negInfinity + negInfinity = negInfinity
.
¬ def (posInfinity + negInfinity)
.
x - y = x + (-y)
.
p * posInfinity = posInfinity
.
p * negInfinity = negInfinity
.
n * posInfinity = negInfinity
.
n * negInfinity = posInfinity
.
¬ def (0 * x) if isInfinity(x)
.
r / posInfinity =0
.
r / negInfinity =0
.
¬ def (x/y) if (isInfinity(x) /\ isInfinity(y))
then
%cons
vars
x,y: CompactReal
.
def (x + y) <=>
 isReal(x) \/ isReal(y) \/ (x=posInfinity /\ y=posInfinity) \/ (x=negInfinity /\ y=negInfinity)
.
def (x - y) <=>
 isReal(x) \/ isReal(y) \/ (x=posInfinity /\ y=negInfinity) \/ (x=negInfinity /\ y=posInfinity)
.
def (x * y) <=> ¬ ((x=0 /\ isInfinity(y)) \/ (y=0 /\ isInfinity(x)) )
.
def (x / y) <=> ¬ (y = 0) /\ (isReal(x) \/ isReal(y))
end
view
TotalOrder_in_CompactReal:
TotalOrder
to CompactBasicReal =
sort
Elem |-> CompactReal,
pred
__ < __ |-> __ < __
end

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