2.9 Library ExactFixedPointNumbers:

library Basic/ExactFixedPointNumbers 
version 0.3
%% authors: M.Roggenbach, T.Mossakowski
%% date: 1.11.99

from

Basic/Orders version 0.3 getSigOrder

from

Basic/Numbers version 0.3 getNat

from

Basic/StructuredDatatypes version 0.3 get

List, Array, Pair

spec

ExactFixedPointNumber 

[

op	L:List[Nat]
axioms	%[EFPN_Param_Cond1] isModulus(L);
	%[EFPN_Param_Cond2] ¬ isEmpty(L)

]

given

{List [Nat fit sort Elem ^_|-> Nat ]

then

pred isModulus: List[Nat]

vars L: List[Nat]; n: Nat

. %[isModulus_nil] isModulus(nil)

. %[isModulus_NonEmptyList]

isModulus(n::L) <=> n>1 /\ isModulus(L)

}

=

op

m:Nat = #(L); %% number of moduli

n:Nat = m+1 %% number of components of an efp-number

then

Array

[ Nat then op m: Nat fit ops min ^_|-> 1, max ^_|-> m ]

[ Nat fit sort Elem ^_|-> Nat ]

with

Index	|->	IndexModulus,
Array[Nat]	|->	ArrayModulus

then

%%

re-arraning the input-list L as an array Modulus

op

Modulus: ArrayModulus

var

i: IndexModulus

.

%[rearrange_modulus]

Modulus!i = first(drop( (i-1) as Nat ,L ) )

then

Array

[ Nat then op n:Nat fit ops min ^_|-> 1, max ^_|-> n ]

[ Nat fit sort Elem ^_|-> Nat ]

with

Index	|->	IndexEfpn,
Array[Nat]	|->	ArrayEfpn

then

%%

an exact fixed point number will be of the form

%%

(sign,z_n, z_n-1, ..., z₁),

%%

where

%%

z_i e {1,2,..., (Modulus!i) - 1} for 1 < i < n,

%%

z_n e N, and

%%

sign e {-1,1}.

%%

we will encode such a number as a pair

%%

(sign,z),

%%

consisting of

%%

z=(z_n, z_n-1, ..., z₁) and

%%

sign e {-1,1}.

sorts

IndexModulus < IndexEfpn;

IndexModulus, IndexEfpn < Nat

sorts

PosEfpn =	{	A: ArrayEfpn . def A!(n as IndexModulus) /\
		forall i:IndexModulus . A!i < Modulus!i };
Sign =	{	z : Int . z = 1 \/ z = -1 }

then

Pair

[ sort Sign ]

[ sort PosEfpn ]

with ops

first |-> sgn,

second |-> number

then

sort

Efpn =	{	p: Pair[Sign,PosEfpn] . ¬
		(sgn(p)= -1 /\ forall i:IndexEfpn . number(p)!i=0 )
	}

preds

isZero, isPos, isNeg:	Efpn;
__ < __ :	Efpn × Efpn;

ops

0, 1 :	Efpn;
proj:	IndexEfpn × Efpn -> Nat;
sgn:	Efpn -> Sign; %% already declared within Pair
make:	IndexEfpn × Nat ->? Efpn;
-__:	Efpn -> Efpn;
__ + __, __ - __ :	Efpn × Efpn -> Efpn;
__ * __:	Int × Efpn -> Efpn;
__ * __:	Efpn × Int -> Efpn;

%prec

{ __+__, __-__, __*__, __div__, __mod__ } < __!__

then

local

{

ops

efpnToInt:	Efpn -> Int;
intToEfpn:	Int -> Efpn;
prod:	Nat ->? Int;
	%% computes PRODi=1k Modulus!(k asIndexModulus)
sum:	Efpn × Nat ->? Int;
	%% computes SUMi=1k zi * prod(i-1)

vars

z: Int; x:Efpn; i: Nat

.

%[prod_0] prod(0)= 1

.

%[prod_Pos]

prod(i)= prod(i-1) * Modulus!(i as IndexModulus) if i>0

.

%[intToEfpn_def]

intToEfpn(z)=x <=>

(( z > 0 => sgn(x)=1 ) /\

(z < 0 => sgn(x)= -1 ) /\

( number(x)!(n as IndexEfpn) = abs(z) div prod(m) ) /\

( (forall k:IndexModulus .

( number(x)!k = (abs(z) div prod(k-1)) mod Modulus!k)

)))

.

%[sum_0] sum(x,0) = 0

.

%[sum_Pos]

sum(x,i) =	sum(x,i-1) +
	(number(x)!(i as IndexEfpn) * prod(i-1))
if i>0

.

%[efpnToInt_def]

efpnToInt(x)= sgn(x) * sum(x,n)

then

%implies

vars

z: Int; x:Efpn; i: Nat

.

%[prod_domain] def prod(i) <=> i < m

.

%[sum_domain] def sum(x,i) <=> i < n

.

%[EfpnInt_bij1] efpnToInt(intToEfpn(z)) = z

.

%[EfpnInt_bij2] intToEfpn(efpnToInt(x)) = x

}

within

vars

x,y:Efpn

.

%[isZeroEfpn_def] isZero(x) <=> efpnToInt(x) = 0

.

%[isPosEfpn_def] isPos(x) <=> efpnToInt(x) > 0

.

%[isNegEfpn_def] isNeg(x) <=> efpnToInt(x) < 0

.

%[isLessEfpn_def] x < y <=> efpnToInt(x) < efpnToInt(y)

axioms

%[ZeroEfpn_def] 0 = efpnToInt(0);

%[OneEfpn_def] 1 = efpnToInt(1)

vars

x,y:Efpn; i:IndexEfpn; k:Nat; z:Int

.

%[proj_def] proj(i,x) = number(x)!i

.

%[makeEfpn_def]

make(i,k)=x <=>	( sgn(x)=1 /\ forall l:IndexEfpn .
	((¬ i=l => proj(i,x)=0) /\
	( i=l => proj(i,x)=k)))

.

%[MinusEpfn_def] - x = intToEfpn( - efpnToInt(x))

.

%[AddEfpn_def] x + y = intToEfpn( efpnToInt(x) + efpnToInt(y) )

.

%[SubEfpn_def] x - y = intToEfpn( efpnToInt(x) - efpnToInt(y) )

.

%[MultEfpn_def1] z * x = intToEfpn( z * efpnToInt(x) )

.

%[MultEfpn_def2] x * z = z * x

then

%implies

vars

i:IndexEfpn; k:Nat; z:Int

.

%[makeEfpn_domain]

def make(i,k) <=>
i=n \/ (i<n => k < Modulus!(i as IndexModulus))

then

SigOrder

with

sort Elem |-> Efpn,

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

end