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