spec SigOrder = sort Elem pred __ <= __, __ >= __, __ < __, __ > __: Elem * Elem; var x,y:Elem . %[geqSigOrder_def] x >= y <=> y <= x . %[lessSigOrder_def] x < y <=> (x <= y /\ not (x=y)) . %[greaterSigOrder_def] x > y <=> y < x end spec PartialOrder = sort Elem pred __ <= __: Elem * Elem vars x,y,z:Elem . %[reflPO_def] x <= x . %[antisymPO_def] x = y if x <= y /\ y <= x . %[transPO_def] x <= z if x <= y /\ y <= z end spec TotalOrder = PartialOrder with sort Elem, pred __ <= __ then vars x,y:Elem . %[comparabilityTOrder_def] x <= y \/ y <= x end spec DefineBooleanAlgebra = sort Elem ops 0:Elem; 1:Elem; __ cap __: Elem * Elem -> Elem, assoc, comm, unit 1; __ cup __: Elem * Elem -> Elem, assoc, comm, unit 0; %prec __ cup __ < __ cap __ vars x,y,z:Elem . %[adjointness_def1] x cap ( x cup y) = x . %[adjointness_def2] x cup ( x cap y) = x . %[zeroAndCap_def] x cap 0 = 0 . %[oneAndCap_def] x cup 1 = 1 . %[distrDefBA_def1] x cap ( y cup z) = (x cap y) cup ( x cap z) . %[distrDefBA_def2] x cup ( y cap z) = (x cup y) cap ( x cup z) . %[inverseDefBA_def] exists x': Elem . x cup x' = 1 /\ x cap x' = 0 end spec BooleanAlgebra [DefineBooleanAlgebra with sort Elem, ops 0, 1,__ cap __, __ cup __] = SigOrder with preds __ <= __,__ >= __,__<__,__>__ then %def vars x,y:Elem . %[poBA_def] x <= y <=> x cap y = x end view PartialOrder_in_BooleanAlgebra [DefineBooleanAlgebra]: PartialOrder to BooleanAlgebra [DefineBooleanAlgebra] = sort Elem |-> Elem, pred __ <= __ |-> __ <= __ end spec GenerateNat = free types Nat ::= 0 | sort Pos; Pos ::= suc(pre: Nat) %% intended system of representatives: %% suc^n(0), %% where n >= 0 is a natural number, and %% suc^0(0) := 0, %% suc^(n+1)(0):= suc(sucn(0)). end spec Nat = GenerateNat with sorts Nat, Pos, ops 0, suc, pre then SigOrder with sort Elem |-> Nat, preds __ <= __,__ >= __,__<__,__>__ then preds __ <= __,__ >= __,__<__,__>__ : Nat * Nat ops +__, abs: Nat -> Nat; __ + __, __ * __, __ ^ __, min, max: Nat × Nat -> Nat; __ - __, __ / __, __ div __, __ mod __: Nat × Nat ->? Nat; __ div __, __ mod __: Nat × Pos -> Nat; 1,2,3,4,5,6,7,8,9: Nat; __ :: __ : Nat × Nat -> Nat %left assoc %number __::__ %prec { __ + __, __ - __ } < { __ * __, __ / __, __ div __, __ mod __ } %prec { __*__, __ / __, __div__, __mod__ } < __ ^ __ vars m,n,r: Nat; p: Pos . %[leqNat_def1] 0 <= n . %[leqNat_def2] not (p <= 0) . %[leqNat_def3] suc(m) <= suc(n) <=> m <= n . %[plusNat_def] + n = n . %[absNat_def] abs(n) = n . %[addNat_0] 0 + m = m . %[addNat_suc] suc(n) + m = suc(n + m) . %[multNat_0] 0 * m = 0 . %[multNat_suc] suc(m) * n = (m * n) + n . %[powerNat_0] m ^ 0 = suc(0) . %[powerNat_suc] m ^ suc(n) = (m ^ n) * m . %[minNat_def1] min(m,n) = m if m <= n . %[minNat_def2] min(m,n) = n if m > n . %[maxNat_def1] max(m,n) = m if m >= n . %[maxNat_def2] max(m,n) = n if m < n . %[subNat_def] m - n = r <=> m = r + n . %[divideNat_Zero] not def(m / n) if n=0 . %[divideNat_Pos] ( m / n = r <=> m = r * n ) if n>0 . %[divNat_pfun] m div n = r <=> (exists s: Nat . m = (n*r) + s /\ 0 <= s /\ r < n) . %[modNat_pfun] m div n = r <=> (exists s: Nat . m = (n*s) + r /\ 0 <= r /\ r < n) %% representing the natural numbers with digits: . %[digit_def1] 1 = suc (0) . %[digit_def2] 2 = suc (1) . %[digit_def3] 3 = suc (2) . %[digit_def4] 4 = suc (3) . %[digit_def5] 5 = suc (4) . %[digit_def6] 6 = suc (5) . %[digit_def7] 7 = suc (6) . %[digit_def8] 8 = suc (7) . %[digit_def9] 9 = suc (8) . %[sequence_def] m :: n = (m * suc(9)) + n then %%implies var m,n,r,s,t: Nat; p: Pos . %[subNat_dom] def(m-n) <=> m >= n . %[divideNat_dom] def(m / n) <=> m mod n = 0 . %[divNat_tfun] m div p = s <=> (exists r: Nat . m = (p*s) + r /\ 0 <= r /\ r < p) . %[divNat_dom] def ( m div n ) <=> not (n=0) . %[modNat_tfun] m mod p = r <=> (exists s: Nat . m = (p*s) + r /\ 0 <= r /\ r < p) . %[modNat_dom] def ( m mod n ) <=> not (n=0) . %[distrNat_def1] (r + s) * t = (r * t) + (s * t) . %[distrNat_def2] t * (r + s) = (t* r ) + (t * s) . %[make_digit1] suc(0) = 1 . %[make_digit2] suc(1) = 2 . %[make_digit3] suc(2) = 3 . %[make_digit4] suc(3) = 4 . %[make_digit5] suc(4) = 5 . %[make_digit6] suc(5) = 6 . %[make_digit7] suc(6) = 7 . %[make_digit8] suc(7) = 8 . %[make_digit9] suc(8) = 9 . %[make_digit10] suc(9) = 1::0 . %[make_digit11] suc(n::0) = n::1 . %[make_digit12] suc(n::1) = n::2 . %[make_digit13] suc(n::2) = n::3 . %[make_digit14] suc(n::3) = n::4 . %[make_digit15] suc(n::4) = n::5 . %[make_digit16] suc(n::5) = n::6 . %[make_digit17] suc(n::6) = n::7 . %[make_digit18] suc(n::7) = n::8 . %[make_digit19] suc(n::8) = n::9 . %[make_digit20] suc(n::9) = suc(n)::0 . %[suc_not_0] not 0 = suc(n) . %[inj_suc] suc(m)=suc(n) => m=n . %[cong_suc] m=n => suc(m)=suc(n) . %[commutative_add] m+n = n+m vars m,n,x,y,m0,n0:Nat end view CommutativeMonoid_in_Nat_Add: CommutativeMonoid to Nat = sort Elem |-> Nat, ops 0 |-> 0, __+__ |-> __+__ end view CommutativeMonoid_in_Nat_Mult: CommutativeMonoid to Nat = sort Elem |-> Nat, ops 0 |-> 1, __+__ |-> __*__ end view TotalOrder_in_Nat: TotalOrder to Nat = sort Elem |-> Nat, pred __ <= __ |-> __ <= __ end spec GenerateInt = GenerateNat with sorts Nat, Pos, ops 0, suc, pre then free types Int ::= sort Nat | sort Neg; Neg ::= -__ (Pos) %% intended system of representatives: %% suc^n(0), n>0, %% 0, and %% -suc^n(0), n>0. ops suc, pre: Int -> Int var p:Pos %% in GenerateNat the operations suc and pre are defined as %% suc: Nat -> Nat and pre: Pos -> Nat; %% here we augment them to total operations of type Int -> Int. . %[sucInt_minus_one] suc(-(suc(0))) = 0 . %[sucInt_Neg] suc(-(suc(p))) = -p . %[preInt_def1] pre(0) = -suc(0) . %[preInt_def2] pre(-p) = -suc(p) end spec Int = GenerateInt with sorts Nat, Pos, Neg, Int, ops 0, suc, pre and {Nat hide op __ - __ } with preds __ <= __,__ >= __,__<__,__>__, ops +__, abs, __ + __, __ * __, __ div __, __ mod __, min, max, __ ^ __, 1,2,3,4,5,6,7,8,9, __ :: __ then preds __ <= __,__ >= __,__<__,__>__ : Int * Int sort NonZeroInt = { x : Int . not x = 0 } preds odd, even: Int; ops +__, -__: Int -> Int; abs: Int -> Nat; __ + __, __ - __, __ * __, min, max: Int × Int -> Int; __^ __: Int × Nat -> Int; __ / __, __ div __, __ mod __, __ quot __, __ rem __: Int × Int ->? Int; __ div __, __ mod __, __ quot __, __ rem __: Int × NonZeroInt -> Int; vars m,n: Nat; p,q: Pos; x,y,z: Int . %[leqInt_def1] -p <= n . %[leqInt_def2] not (m <= -p) . %[leqInt_def3] -p <= -q <=> q <= p . %[even_zero] even(0) . %[odd_zero] not odd(0) . %[odd_suc] odd(suc(m)) <=> even(m) . %[even_suc] even(suc(m)) <=> odd(m) . %[even_Neg] even(-p) <=> even(p) . %[odd_Neg] odd(-p) <=> odd(p) . %[plusInt_def] + (-p) = -p . %[minusInt_zero] -0 = 0 . %[minusInt_Neg] - (- p) = p . %[absInt_Neg] abs(-p)=p . %[addInt_def1] 0 + (-p) = -p . %[addInt_def2] (-p) + 0 = -p . %[addInt_def3] suc(m) + (-p) = m + suc(-p) . %[addInt_def4] (-p) + suc(m) = suc(-p) + m . %[addInt_def5] (-p) + (-q) = - (p + q) . %[subInt_def] x - y = x + (-y) . %[multInt_def1] 0 * (-p) = 0 . %[multInt_def2] (-p) * 0 = 0 . %[multInt_def3] (-p) * (-q) = p * q . %[multInt_def4] (-p) * q = - (p * q) . %[multInt_def5] p * (-q) = - (p * q) . %[minInt_def1] min(x,y) = x if x <= y . %[minInt_def2] min(x,y) = y if x > y . %[maxInt_def1] max(x,y) = y if x <= y . %[maxInt_def2] max(x,y) = x if x > y . %[powerInt_zero] (-p) ^ 0 = suc(0) . %[powerInt_suc] (-p) ^ suc(n) = ((-p) ^ n) * (-p) . %[divideInt_Zero] not def(x / y) if y=0 . %[divideInt_NonZeroInt] ( x / y = z <=> x = z * y ) if not y=0 . %[divInt_pfun] x div y = z <=> (exists r: Int . x = (z*y) + r /\ 0 <= r /\ r < abs(y)) . %[modInt_pfun] x mod y = z <=> (exists s: Int . x = (s*y) + z /\ 0 <= z /\ z < abs(y)) . %[quotInt_pfun1] x quot y = abs(x) div abs(y) if (x >= 0 /\ y >= 0) \/ (x < 0 /\ y < 0) . %[quotInt_pfun2] x quot y = - (abs(x) div abs(y)) if (x >= 0 /\ y < 0) \/ (x < 0 /\ y >= 0) . %[remInt_pfun1] x rem y = abs(x) mod abs(y) if x >= 0 . %[remInt_pfun2] x rem y = - (abs(x) mod abs(y)) if x < 0 then %implies vars n : NonZeroInt; x,y,z: Int . %[divideInt_dom] def (x / y) <=> x mod y = 0 . %[divInt_tfun] x div n = z <=> (exists r: Int . x = (z*n) + r /\ 0 <= r /\ r < abs(n)) . %[divInt_dom] def (x div y) <=> not y=0 . %[modInt_tfun] x mod n = z <=> (exists s: Int . x = (s*n) + z /\ 0 <= z /\ z < abs(n)) . %[modInt_dom] def (x mod y) <=> not y=0 . %[quotInt_tfun1] x quot n = abs(x) div abs(n) if (x >= 0 /\ n > 0) \/ (x < 0 /\ n < 0) . %[quotInt_tfun2] x quot n = - (abs(x) div abs(n)) if (x >= 0 /\ n < 0) \/ (x < 0 /\ n > 0) . %[quotInt_dom] def (x quot y) <=> not y=0 . %[remInt_tfun1] x rem n = abs(x) mod abs(n) if x >= 0 . %[remInt_tfun2] x rem n = - (abs(x) mod abs(n)) if x < 0 . %[remInt_dom] def (x rem y) <=> not y=0 end view TotalOrder_in_Int: TotalOrder to Int = sort Elem |-> Int, pred __ <= __ |-> __ <= __ end spec GenerateRat = {Int hide op __ / __ } with sorts Nat, Pos, Neg,Int, NonZeroInt, preds __ <= __,__ >= __,__<__,__>__, odd, even, ops 0, suc, pre, +__, -__, abs, __ + __, __-__, __ * __, min, max, __ ^ __, __ div __, __ mod __, __ quot __, __ rem __, 1,2,3,4,5,6,7,8,9, __ :: __ then free { type Rat ::= sort Int | __ / __ (nom: Int ; denom: Pos) vars i,j: Int; p,q: Pos . %[embeddingIntToRat] i/1 = i . %[equalityInRat] i/p = j/q <=> i*q = j*p } %% intended system of representatives: %% i and %% j / p, %% where i,j are of sort Int, p > 1 is of sort Pos, %% and for any pair j/p holds: j and p are relatively prime. end spec Rat = GenerateRat with sortsNat, Pos, Neg, Int, Rat, NonZeroInt, preds__ <= __,__ >= __,__<__,__>__, odd, even, ops 0, suc, pre, +__, -__, abs, __ + __, __-__, __ * __, __ / __, __ div __, __ mod __, min, max, __ ^ __, 1,2,3,4,5,6,7,8,9, __ :: __ then SigOrder with sort Elem |-> Rat, preds __ <= __,__ >= __,__<__,__>__ then preds __ <= __,__ >= __,__<__,__>__ : Rat * Rat sort NonZeroRat = { r: Rat . not r=0 } ops + __ , - __ : Rat -> Rat; __ + __ , __ - __ , __ * __ : Rat × Rat -> Rat; __ / __ : Rat × Rat ->? Rat; __ / __ : Rat × NonZeroRat -> Rat; %% operations for a representation of Rat as decimal fraction: ops __ ::: __ : Nat × Nat -> Rat; __ E __ : Rat × Int -> Rat %prec __ E __ < __ ::: __ vars m,n: Nat; r,s: Rat . %[plusRat_def] + r = r . %[minusRat_def] - r = (-nom(r)) / denom(r) . %[addRat_def] r+s = ((nom(r) * denom(s)) + (nom(s)* denom(r)))/ (denom(r) * denom(s)) . %[subRat_def] r-s = ((nom(r) * denom(s)) - (nom(s)* denom(r)))/ (denom(r) * denom(s)) . %[multRat_def] r*s = (nom(r) * nom(s)) / ( denom(r) * denom(s) ) . %[divRat_pfun1] r/s = (nom(r) * denom(s)) / ((denom(r) * nom(s)) as Pos) if nom(s) >= 0 . %[divRat_pfun2] r/s = ( (-1) * (nom(r) * denom(s))) / ( ((-1) * (denom(r) * nom(s))) as Pos) if nom(s) < 0 . %[leqRat_def] r <= s <=> nom(r)*denom(s) <= nom(s) * denom(r) then %implies vars r,s,t:Rat; n:NonZeroRat . %[divRat_tfun1] r/n = (nom(r) * denom(n)) / ((denom(r) * nom(n)) as Pos) if nom(n) > 0 . %[divRat_tfun2] r/n = ( (-1) * (nom(r) * denom(n))) / ( ((-1) * (denom(r) * nom(n))) as Pos) if nom(n) < 0 . %[divRat_dom] def r/s <=> not (s = 0) then local op tenPower: Nat -> Nat vars n,m: Nat %% tenPower(n):= min { 10k | k in N \{0}, 10k > n }: . %[tenPower_digit] tenPower(n)=1::0 if n < (1::0) . %[tenPower_number] tenPower( ((1::0) * m) + n)= (1::0) * tenPower(m) if n < (1::0) within vars r:Rat; n,m: Nat; p: Pos %% represent the decimal fraction n.m as rational: . %[decfract_def] n:::m = n + (m/tenPower(m)) %% introduce an exponent: . %[exponentRat_Nat] r E n = r* ((1::0) ^ n) . %[exponentRat_Neg] r E (-p) = r / ((1::0) ^ n) end view CommutativeField_in_Rat: DefineCommutativeField to Rat = sort Elem |-> Rat, ops 0 |-> 0, 1 |-> 1, __+__ |-> __+__, __*__ |-> __*__ end view TotalOrder_in_Rat: TotalOrder to Rat = sort Elem |-> Rat, pred __ <= __ |-> __ <= __ end spec Boolean = free type Boolean ::= TRUE | FALSE %% intended system of representatives: %% TRUE, FALSE ops NOT : Boolean -> Boolean; __AND__, __OR__ : Boolean * Boolean -> Boolean %prec __OR__ < __AND__ vars x,y,z:Boolean . %[NOT_FALSE] NOT(FALSE)=TRUE . %[NOT_TRUE] NOT(TRUE)=FALSE . %[AND_def1] FALSE AND FALSE = FALSE . %[AND_def2] FALSE AND TRUE = FALSE . %[AND_def3] TRUE AND FALSE = FALSE . %[AND_def4] TRUE AND TRUE = TRUE . %[OR_def] x OR y= NOT ( NOT (x) AND NOT (y) ) end view BooleanAlgebra_in_Boolean: DefineBooleanAlgebra to Boolean = sort Elem |-> Boolean, ops 0 |-> FALSE, 1 |-> TRUE, __ cap __ |-> __AND__, __ cup __ |-> __OR__ end spec CARDINAL [op Wordlength: Nat] given Nat = Nat then op __ ^ __ : Nat * Nat -> Nat type CARDINAL ::= natToCard (cardToNat : Nat)? vars x : Nat; c:CARDINAL . %[natToCard_dom] def natToCard(x) <=> x <= (2 ^ Wordlength) - 1 . %[natToCard_def] natToCard (cardToNat(c)) = c %% %% cardToNat (natToCard(x)) = x if defnatToCard(x) %% - is provided by the semantics of the type construct. then SigOrder with Elem |-> CARDINAL then preds __ <= __,__ >= __,__<__,__>__ : CARDINAL * CARDINAL ops maxCardinal: Nat; maxCardinal: CARDINAL; 0,1: CARDINAL; +__, abs: CARDINAL -> CARDINAL; __ + __, __ - __, __ * __, __ div __, __ mod __: CARDINAL × CARDINAL ->? CARDINAL; axioms %[maxCardinal_Nat] maxCardinal= (2 ^ Wordlength) - 1; %[maxCardinal_CARDINAL] maxCardinal= natToCard(maxCardinal) vars x,y: CARDINAL . %[leq_CARDINAL] x <= y <=> cardToNat(x) <= cardToNat(y) . %[plus_CARDINAL] + x = natToCard(+ cardToNat(x)) . %[abs_CARDINAL] abs(x) = natToCard(abs(cardToNat(x))) . %[add_CARDINAL] x + y = natToCard(cardToNat(x) + cardToNat(y)) . %[sub_CARDINAL] x-y = natToCard(cardToNat(x) - cardToNat(y)) . %[mult_CARDINAL] x*y = natToCard(cardToNat(x) * cardToNat(y)) . %[div_CARDINAL] x div y = natToCard(cardToNat(x) div cardToNat(y)) . %[mod_CARDINAL] x mod y = natToCard(cardToNat(x) mod cardToNat(y)) then %implies ops __ + __: CARDINAL × CARDINAL ->? CARDINAL, assoc, comm, unit 0; __ * __: CARDINAL × CARDINAL ->? CARDINAL, assoc, comm, unit 1; vars x,y: CARDINAL . %[add_CARDINAL_dom] def x+y <=> cardToNat(x) + cardToNat(y) <= maxCardinal . %[sub_CARDINAL_dom] def x-y <=> x >= y . %[mult_CARDINAL_dom] def x*y <=> cardToNat(x) * cardToNat(y) <= maxCardinal . %[div_CARDINAL_dom] def x div y <=> not y=0 . %[mod_CARDINAL_dom] def x mod y <=> not y=0 end spec INTEGER [op Wordlength: Nat] given Nat = Int then type INTEGER ::= intToInteger (integerToInt: Int)? vars x:Int; i:INTEGER . %[intToInteger_dom] def intToInteger(x) <=> - (2 ^ (Wordlength-1)) <= x /\ x <= (2 ^ (Wordlength-1)) -1 . %[intToInteger_def] intToInteger (integerToInt(i)) = i %% the other direction - %% integerToInt (intToInteger(x)) = x if defintToInteger(x) %% - is provided by the semantics of the type construct. then SigOrder with Elem |-> INTEGER then preds __ <= __,__ >= __,__<__,__>__ : INTEGER * INTEGER ops maxInteger, minInteger: Int; maxInteger, minInteger: INTEGER; 0,1: INTEGER; +__: INTEGER -> INTEGER; -__, abs: INTEGER ->? INTEGER; __ + __, __ - __, __ * __, __ / __, __ div __, __ mod __, __ quot __, __ rem__: INTEGER × INTEGER ->? INTEGER axioms %[maxInteger_Int] maxInteger= (2 ^ (Wordlength-1))-1; %[minInteger_Int] minInteger= -(2 ^ (Wordlength-1)); %[maxInteger_INTEGER] maxInteger=intToInteger(maxInteger); %[minInteger_INTEGER] minInteger=intToInteger(minInteger) vars x,y: INTEGER . %[leq_INTEGER] x <= y <=> integerToInt(x) <= integerToInt(y) . %[plus_INTEGER] + x = x . %[minus_INTEGER] - x = intToInteger( - integerToInt(x) ) . %[abs_INTEGER] abs(x) = intToInteger( abs( integerToInt(x)) ) . %[add_INTEGER] x + y = intToInteger( integerToInt(x) + integerToInt(y)) . %[sub_INTEGER] x - y = intToInteger( integerToInt(x) - integerToInt(y) ) . %[mult_INTEGER] x * y = intToInteger( integerToInt(x) * integerToInt(y)) . %[divide_INTEGER] x / y = intToInteger( integerToInt(x) / integerToInt(y)) . %[div_INTEGER] x div y = intToInteger (integerToInt(x) div integerToInt(y)) . %[mod_INTEGER] x mod y = intToInteger( integerToInt(x) mod integerToInt(y)) . %[quot_INTEGER] x quot y = intToInteger( integerToInt(x) mod integerToInt(y)) . %[rem_INTEGER] x rem y = intToInteger( integerToInt(x) mod integerToInt(y)) then %implies ops __ + __: INTEGER × INTEGER ->? INTEGER, assoc, comm, unit 0; __ * __: INTEGER × INTEGER ->? INTEGER, assoc, comm, unit 1; vars x,y:INTEGER . %[minus_INTEGER_dom] def - x <=> integerToInt(x) >= minInteger + 1 . %[abs_INTEGER_dom] def abs(x) <=> integerToInt(x) >= minInteger + 1 . %[add_INTEGER_dom] def x + y <=> minInteger <= integerToInt(x) + integerToInt(y) /\ integerToInt(x) + integerToInt(y) <= maxInteger . %[sub_INTEGER_dom] def x - y <=> minInteger <= integerToInt(x) - integerToInt(y) /\ integerToInt(x) - integerToInt(y) <= maxInteger . %[mult_INTEGER_dom] def x * y <=> minInteger <= integerToInt(x) * integerToInt(y) /\ integerToInt(x) * integerToInt(y) <= maxInteger . %[divide_INTEGER_dom] def x / y <=> def integerToInt(x)/integerToInt(y) . %[div_INTEGER_dom] def x div y <=> not y=0 . %[mod_INTEGER_dom] def x mod y <=> not y=0 . %[quot_INTEGER_dom] def x quot y <=> not y=0 . %[rem_INTEGER_dom] def x rem y <=> not y=0 end spec Elem = sort Elem end spec GenerateFiniteSet [Elem with sort Elem] = free { type FinSet[Elem]::= {} | set(Elem) | __ union __ (FinSet[Elem];FinSet[Elem]) op __ union __: FinSet[Elem] * FinSet[Elem] -> FinSet[Elem], assoc, comm, idem, unit {} } %% intended system of representatives: %% {} and %% set(x1) union ... union set(xn), %% where n >= 1, xi in Elem, xi =/= xj for i =/= j, and %% x1 < x2 < ...< xn (< is an arbitrary order on Elem) end spec FiniteSet [Elem with sort Elem] = GenerateFiniteSet [Elem] with sort FinSet[Elem], ops {}, set, __ union __ and Nat with sorts Nat, Pos, preds __ <= __,__ >= __,__<__,__>__, ops 0, suc, pre, +__, abs, __+__, __*__, __^ __, min, max,__ / __, __ - __, __ div __, __ mod __, 1,2,3,4,5,6,7,8,9, __ :: __ then preds __ elemOf __: Elem * FinSet[Elem]; __ isSubsetOf __: FinSet[Elem] * FinSet[Elem] ops __ + __ : Elem * FinSet[Elem] -> FinSet[Elem]; __ + __, __ - __ : FinSet[Elem] * Elem -> FinSet[Elem]; __ intersection __, __ - __, __ symmDiff __: FinSet[Elem] * FinSet[Elem] -> FinSet[Elem]; #__: FinSet[Elem] -> Nat; vars x,y : Elem; S,T,U,V:FinSet[Elem] . %[elemOf_empty] not x elemOf {} . %[elemOf_set] x elemOf set(y) <=> (x=y) . %[elemOf_union] x elemOf (S union T) <=> (x elemOf S) \/ (x elemOf T) . %[subset_empty] {} isSubsetOf S . %[subset_set] set(x) isSubsetOf S <=> x elemOf S . %[subset_union] (S union T) isSubsetOf U <=> S isSubsetOf U /\ T isSubsetOf U . %[add_FinSet_def1] x + S = set(x) union S . %[add_FinSet_def2] S + x = x + S . %[sub_FinSet_empty] {} - x = {} . %[sub_FinSet_set1] set(y) - x = set(y) if not x = y . %[sub_FinSet_set2] set(y) - x = {} if x = y . %[sub_FinSet_union] (S union T) - x = (S - x) union (T - x) . %[intersect_empty] {} intersection S = {} . %[intersect_set1] set(x) intersection S = {} if not x elemOf S . %[intersect_set2] set(x) intersection S = set(x) if x elemOf S . %[intersect_union] (S union T) intersection U = ( S intersection U ) union (T intersection U) . %[diff_empty] {} - S = {} . %[diff_set1] set(x) - S = set(x) if not x elemOf S . %[diff_set2] set(x) - S = {} if x elemOf S . %[diff_union] (S union T) - U = (S - U ) union (T - U) . %[symmDiff_def] S symmDiff T = (S - T) union (T - S) . %[numberOf_FinSet_empty] #{} = 0 . %[numberOf_FinSet_set] #set(x) = 1 . %[numberOf_FinSet_union] #(S union T) = (#S) + (#T) then %implies ops __ intersection __: FinSet[Elem] * FinSet[Elem] -> FinSet[Elem], assoc, comm, idem; __ symmDiff __ : FinSet[Elem] * FinSet[Elem] -> FinSet[Elem], comm; vars x: Elem; S,T: FinSet[Elem] . %[subset_characterization] S isSubsetOf T <=> ( forall x: Elem . x elemOf S => x elemOf T ) end view PartialOrder_in_FiniteSet [Elem]: PartialOrder to FiniteSet [Elem] = sort Elem |-> FinSet[Elem] , pred __ <= __ |-> __ isSubsetOf __ end spec Pair [sort S] [sort T] = free type Pair[S,T] ::= pair(first:S; second:T) end spec SemiGroup = sort Elem op __ + __: Elem * Elem -> Elem, assoc end spec Monoid = SemiGroup with sort Elem, op __ + __ then op 0:Elem; __ + __: Elem * Elem -> Elem, unit 0 end spec CommutativeMonoid = Monoid with sort Elem, op 0, __ + __ then op __ + __: Elem * Elem -> Elem, comm end spec DefineGroup = Monoid with sort Elem, op 0, __ + __ then var x:Elem . %[ExInverseDefGroup_def] exists x': Elem . x + x' = 0 /\ x' + x = 0 end spec Group [DefineGroup with sort Elem, op 0, __ + __ ] = %def ops inv: Elem -> Elem; __ - __: Elem * Elem -> Elem; vars x,y: Elem . %[inv1] x + inv(x) = 0 . %[inv2] inv(x) + x = 0 . %[minusGroup_def] x - y = x + inv(y) end spec DefineCommutativeGroup = DefineGroup with sort Elem, op 0, __ + __ then op __ + __: Elem * Elem -> Elem, comm end spec CommutativeGroup [DefineCommutativeGroup with sort Elem, op 0, __ + __ ] = %def Group [DefineGroup] with ops inv, __ - __ end spec DefineRing = DefineCommutativeGroup with sort Elem, ops 0, __ + __ then Monoid with 0 |-> 1, __+__ |-> __*__ then op 1: Elem op __ * __ : Elem * Elem -> Elem %prec __ + __ < __ * __ vars x,y,z:Elem . %[distrRing_def1] (x+y)*z = (x * z) + (y * z) . %[distrRing_def2] z * ( x + y ) = (z * x) + (z * y) end spec Ring [DefineRing with sort Elem, ops 0, 1, __+__, __ * __ ] = %def CommutativeGroup [DefineCommutativeGroup] with ops inv, __ - __ %%prec __ - __ < __ * __ then %def sort RUnit = { x: Elem . exists x': Elem . x * x' = 1 /\ x' * x = 1 } end spec DefineIntegralDomain = DefineRing with sort Elem, ops 0, 1, __+__, __ * __ then axiom %[zeroNotEqualOne_def] not (1 = 0) op __ * __: Elem * Elem -> Elem, comm vars x, y :Elem . %[withoutZeroDivisors_def] x=0 \/ y=0 if x * y = 0 end spec IntegralDomain [DefineIntegralDomain with sort Elem, ops 0, 1, __+__, __ * __ ] = %def Ring [DefineRing] with sort RUnit, ops inv, __ - __ then %def sort Irred= { x: Elem . not (x in RUnit) /\ ( forall y, z: Elem . x = y * z => (y in RUnit \/ z in RUnit ) ) } end spec DefineEuclidianRing = DefineIntegralDomain with sort Elem, ops 0, 1, __+__, __ * __ and {Nat reveal pred __ < __ } then op delta: Elem -> Nat vars a,b: Elem . exists q,r : Elem . a = (q * b) + r /\ (r = 0 \/ delta(r) < delta(b) ) if ( not b=0 ) end spec EuclidianRing [DefineEuclidianRing with sorts Elem, Nat, pred __ < __, ops 0, 1, __+__, __ * __ ] = IntegralDomain [DefineIntegralDomain] with sorts RUnit, Irred, ops inv, __ - __ end view EuclidianRing_in_Int: DefineEuclidianRing to Int = %% Signature of DefineIntegralDomain: sort Elem |-> Int, ops 0 |-> 0, 1 |-> 1, __ + __ |-> __ + __ , __ * __ |-> __ * __, %% Nat is a subsort of Int op delta |-> abs end spec ConstructField = DefineRing with sort Elem, ops 0, 1, __+__, __ * __ then axiom not 0 = 1 sort NonZeroElement = { x: Elem . not x = 0 } then DefineGroup with Elem |-> NonZeroElement, 0 |-> 1, __+__ |-> __*__ end %% an obvious view which helps to write the specification Field: view MultiplicativeGroup_in_Field: DefineGroup to ConstructField = sort Elem |-> NonZeroElement, ops 0 |-> 1, __+__ |-> __*__ end spec DefineField = ConstructField hide sort NonZeroElement with sort Elem, ops 0, 1, __+__, __ * __ end spec Field [DefineField with sort Elem, ops 0, 1, __+__, __ * __ ] = %def Ring [DefineRing] with sort RUnit, ops inv, __ - __ then %def Group [view MultiplicativeGroup_in_Field] with sort NonZeroElement, ops __ - __ |-> __ / __: NonZeroElement × NonZeroElement -> NonZeroElement, inv |-> multInv %%prec {__+ __, __ - __ } < __ / __ then op __ / __: Elem × Elem ->? Elem; __ / __: Elem × NonZeroElement -> Elem vars x,y,z: Elem . %[divField_pfun] x/y=z <=> ( x in NonZeroElement /\ y in NonZeroElement /\ z in NonZeroElement) \/ (x=0 /\ not y=0 /\ z=0) then %implies vars x,y,z:Elem; n: NonZeroElement . %[divField_tfun] x/n=z <=> ( x in NonZeroElement /\ z in NonZeroElement) \/ (x=0 /\ z=0) . %[divField_dom] def x/y <=> not y = 0 end spec DefineCommutativeField = DefineField with sort Elem, ops 0, 1, __+__, __ * __ then op __ * __ : Elem × Elem -> Elem, comm end spec CommutativeField [DefineCommutativeField with sort Elem, ops 0, 1, __+__, __ * __ ] = %def Field [DefineField] end spec PairIndexElem [sort Index] [sort Elem] = free type Pair[Index,Elem] ::= pair(first:Index; second:Elem) end spec GenerateFiniteSetPair [sorts Index, Elem] = PairIndexElem then free { type FinSet[Pair[Index,Elem]]::= {} | set(Pair[Index,Elem]) | __ union __ (FinSet[Pair[Index,Elem]];FinSet[Pair[Index,Elem]]) op __ union __: FinSet[Pair[Index,Elem]] * FinSet[Pair[Index,Elem]] -> FinSet[Pair[Index,Elem]], assoc, comm, idem, unit {} } %% intended system of representatives: %% {} and %% set(x1) union ... union set(xn), %% where n >= 1, xi in Pair[Index,Elem], xi =/= xj for i =/= j, and %% x1 < x2 < ...< xn (< is an arbitrary order on Pair[Index,Elem]) end spec FiniteSetPair [sorts Index, Elem] = GenerateFiniteSetPair [sorts Index, Elem] and Nat then preds __ elemOf __: Pair[Index,Elem] * FinSet[Pair[Index,Elem]]; __ isSubsetOf __: FinSet[Pair[Index,Elem]] * FinSet[Pair[Index,Elem]] ops __ + __ : Pair[Index,Elem] * FinSet[Pair[Index,Elem]] -> FinSet[Pair[Index,Elem]]; __ + __, __ - __ : FinSet[Pair[Index,Elem]] * Pair[Index,Elem] -> FinSet[Pair[Index,Elem]]; __ intersection __, __ - __, __ symmDiff __: FinSet[Pair[Index,Elem]] * FinSet[Pair[Index,Elem]] -> FinSet[Pair[Index,Elem]]; #__: FinSet[Pair[Index,Elem]] -> Nat; vars x,y : Pair[Index,Elem]; S,T,U,V:FinSet[Pair[Index,Elem]] . %[elemOf_empty] not x elemOf {} . %[elemOf_set] x elemOf set(y) <=> (x=y) . %[elemOf_union] x elemOf (S union T) <=> (x elemOf S) \/ (x elemOf T) . %[subset_empty] {} isSubsetOf S . %[subset_set] set(x) isSubsetOf S <=> x elemOf S . %[subset_union] (S union T) isSubsetOf U <=> S isSubsetOf U /\ T isSubsetOf U . %[add_FinSet_def1] x + S = set(x) union S . %[add_FinSet_def2] S + x = x + S . %[sub_FinSet_empty] {} - x = {} . %[sub_FinSet_set1] set(y) - x = set(y) if not x = y . %[sub_FinSet_set2] set(y) - x = {} if x = y . %[sub_FinSet_union] (S union T) - x = (S - x) union (T - x) . %[intersect_empty] {} intersection S = {} . %[intersect_set1] set(x) intersection S = {} if not x elemOf S . %[intersect_set2] set(x) intersection S = set(x) if x elemOf S . %[intersect_union] (S union T) intersection U = ( S intersection U ) union (T intersection U) . %[diff_empty] {} - S = {} . %[diff_set1] set(x) - S = set(x) if not x elemOf S . %[diff_set2] set(x) - S = {} if x elemOf S . %[diff_union] (S union T) - U = (S - U ) union (T - U) . %[symmDiff_def] S symmDiff T = (S - T) union (T - S) . %[numberOf_FinSet_empty] #{} = 0 . %[numberOf_FinSet_set] #set(x) = 1 . %[numberOf_FinSet_union] #(S union T) = (#S) + (#T) then %implies ops __ intersection __: FinSet[Pair[Index,Elem]] * FinSet[Pair[Index,Elem]] -> FinSet[Pair[Index,Elem]], assoc, comm, idem; __ symmDiff __ : FinSet[Pair[Index,Elem]] * FinSet[Pair[Index,Elem]] -> FinSet[Pair[Index,Elem]], comm; vars x: Pair[Index,Elem]; S,T: FinSet[Pair[Index,Elem]] . %[subset_characterization] S isSubsetOf T <=> ( forall x: Pair[Index,Elem] . x elemOf S => x elemOf T ) end spec FiniteMap [sort Index] [sort Elem] = FiniteSetPair [sorts Index, Elem] then sort Array[Elem] = { F : FinSet[Pair[Index,Elem]] . forall g,h: Pair[Index,Elem] . (g elemOf F /\ h elemOf F /\ first(g)=first(h)) => second(g)=second(h) } preds isEmpty: Array[Elem]; __elemOf__: Pair[Index,Elem] × Array[Elem]; __canBeAddedTo __: Pair[Index,Elem] × Array[Elem]; %% elemOf is determined by overloading ops emptyMap: Array[Elem]; add: Pair[Index,Elem] × Array[Elem] ->? Array[Elem]; remove: Pair[Index,Elem] × Array[Elem] -> Array[Elem]; evaluate: Index × Array[Elem] ->? Elem; axiom %[emptyMap_def] emptyMap = {} as Array[Elem] vars p:Pair[Index,Elem]; F: Array[Elem]; s:Index; t: Elem . %[isEmpty_def] isEmpty(F) <=> F=emptyMap . %[addFiniteMap_def] add(p,F) = (F union set(p)) as Array[Elem] . %[canBeAddedTo_def] p canBeAddedTo F <=> def add(p,F) . %[remove_def] remove(p,F) = (F - p) as Array[Elem] . %[evaluate_def] evaluate(s,F) = t <=> pair(s,t) elemOf F then %implies vars p: Pair[Index,Elem]; F: Array[Elem]; s: Index . %[addFiniteMap_domain] def add(p,F) <=> forall q : Pair[Index,Elem] . (q elemOf F /\ first(p)=first(q)) => second(p)=second(q) . %[evaluate_domain] def evaluate(s,F) <=> exists t:Elem . pair(s,t) elemOf F end spec Array [ops min, max: Int axiom %[Cond_nonEmptyIndex] min <= max] [sort Elem] given Int = sort Index = { i : Int . min <= i /\ i <= max } then { FiniteMap [sort Index] [sort Elem] then ops init: Array[Elem] -> Array[Elem]; __!__: Array[Elem] × Index ->? Elem; __!__:=__ : Array[Elem] × Index × Elem -> Array[Elem]; vars A: Array[Elem]; i: Index; e: Elem . %[initArray_def] init(A)= emptyMap . %[evaluateArray_def] A!i = evaluate(i,A) . %[assignmentArray_def] A!i:=e = add(pair(i,e),remove(pair(i,A!i),A)) } reveal sort Array[Elem], ops init, __!__, __!__:=__ then %implies vars A: Array[Elem]; i,j: Index; e,f: Elem . %[evaluateArray_domain1] not def init(A)!i . %[evaluateArray_domain2] def (A!i:=e)!i . %[evaluateArray_assignment1] (A!i:=e)!j = e if i=j . %[evaluateArray_assignment2] (A!i:=e)!j = A!j if not (i=j) end %% The following specification asssumes that a %% certain list of names delimited by single quotes %% are available as identifiers. %% The list comprises of \verb@'c'@, where \verb@c@ %% is any printing character except \verb@'@, \verb@"@ and \verb@\@ %% and of \verb@'\nnn'@ where nnn is a numeral in the range %% from 0 to 255.\\ %% Moreover, a syntax for numerals is assumed. spec Char = Nat with sorts Nat, Pos, preds __ <= __,__ >= __,__<__,__>__, ops 0, suc, pre, +__, abs, __ + __, __ - __, __ * __, __ div __, __ mod __, min, max, __ ^ __, 1,2,3,4,5,6,7,8,9, __ :: __ then sort Char preds isLetter, isDigit, isPrintable: Char ops chr : Nat ->? Char; ord : Char -> Nat; vars n:Nat; c:Char %% definedness of chr: . def chr(n) <=> n <= 255 %% correspondence between ord and chr: . chr(ord(c))=c . ord(chr(n))=n if n < 255 %% definition of the printable characters: op ' ' : Char; axiom ord(' ') = 32; op '!' : Char; axiom ord('!') = 33; op '\"' : Char; axiom ord('\"') = 34; op '#' : Char; axiom ord('#') = 35; op '$' : Char; axiom ord('$') = 36; op '%' : Char; axiom ord('%') = 37; op '&' : Char; axiom ord('&') = 38; op '\'' : Char; axiom ord('\'') = 39; op '(' : Char; axiom ord('(') = 40; op ')' : Char; axiom ord(')') = 41; op '*' : Char; axiom ord('*') = 42; op '+' : Char; axiom ord('+') = 43; op ',' : Char; axiom ord(',') = 44; op '-' : Char; axiom ord('-') = 45; op '.' : Char; axiom ord('.') = 46; op '/' : Char; axiom ord('/') = 47; op '0' : Char; axiom ord('0') = 48; op '1' : Char; axiom ord('1') = 49; op '2' : Char; axiom ord('2') = 50; op '3' : Char; axiom ord('3') = 51; op '4' : Char; axiom ord('4') = 52; op '5' : Char; axiom ord('5') = 53; op '6' : Char; axiom ord('6') = 54; op '7' : Char; axiom ord('7') = 55; op '8' : Char; axiom ord('8') = 56; op '9' : Char; axiom ord('9') = 57; op ':' : Char; axiom ord(':') = 58; op ';' : Char; axiom ord(';') = 59; op '<' : Char; axiom ord('<') = 60; op '=' : Char; axiom ord('=') = 61; op '>' : Char; axiom ord('>') = 62; op '?' : Char; axiom ord('?') = 63; op '@' : Char; axiom ord('@') = 64; op 'A' : Char; axiom ord('A') = 65; op 'B' : Char; axiom ord('B') = 66; op 'C' : Char; axiom ord('C') = 67; op 'D' : Char; axiom ord('D') = 68; op 'E' : Char; axiom ord('E') = 69; op 'F' : Char; axiom ord('F') = 70; op 'G' : Char; axiom ord('G') = 71; op 'H' : Char; axiom ord('H') = 72; op 'I' : Char; axiom ord('I') = 73; op 'J' : Char; axiom ord('J') = 74; op 'K' : Char; axiom ord('K') = 75; op 'L' : Char; axiom ord('L') = 76; op 'M' : Char; axiom ord('M') = 77; op 'N' : Char; axiom ord('N') = 78; op 'O' : Char; axiom ord('O') = 79; op 'P' : Char; axiom ord('P') = 80; op 'Q' : Char; axiom ord('Q') = 81; op 'R' : Char; axiom ord('R') = 82; op 'S' : Char; axiom ord('S') = 83; op 'T' : Char; axiom ord('T') = 84; op 'U' : Char; axiom ord('U') = 85; op 'V' : Char; axiom ord('V') = 86; op 'W' : Char; axiom ord('W') = 87; op 'X' : Char; axiom ord('X') = 88; op 'Y' : Char; axiom ord('Y') = 89; op 'Z' : Char; axiom ord('Z') = 90; op '[' : Char; axiom ord('[') = 91; op '\\' : Char; axiom ord('\\') = 92; op ']' : Char; axiom ord(']') = 93; op '^' : Char; axiom ord('^') = 94; op '_' : Char; axiom ord('_') = 95; op '`' : Char; axiom ord('`') = 96; op 'a' : Char; axiom ord('a') = 97; op 'b' : Char; axiom ord('b') = 98; op 'c' : Char; axiom ord('c') = 99; op 'd' : Char; axiom ord('d') = 100; op 'e' : Char; axiom ord('e') = 101; op 'f' : Char; axiom ord('f') = 102; op 'g' : Char; axiom ord('g') = 103; op 'h' : Char; axiom ord('h') = 104; op 'i' : Char; axiom ord('i') = 105; op 'j' : Char; axiom ord('j') = 106; op 'k' : Char; axiom ord('k') = 107; op 'l' : Char; axiom ord('l') = 108; op 'm' : Char; axiom ord('m') = 109; op 'n' : Char; axiom ord('n') = 110; op 'o' : Char; axiom ord('o') = 111; op 'p' : Char; axiom ord('p') = 112; op 'q' : Char; axiom ord('q') = 113; op 'r' : Char; axiom ord('r') = 114; op 's' : Char; axiom ord('s') = 115; op 't' : Char; axiom ord('t') = 116; op 'u' : Char; axiom ord('u') = 117; op 'v' : Char; axiom ord('v') = 118; op 'w' : Char; axiom ord('w') = 119; op 'x' : Char; axiom ord('x') = 120; op 'y' : Char; axiom ord('y') = 121; op 'z' : Char; axiom ord('z') = 122; op '{' : Char; axiom ord('{') = 123; op '|' : Char; axiom ord('|') = 124; op '}' : Char; axiom ord('}') = 125; op '~' : Char; axiom ord('~') = 126; end spec Char1 = Char then op ' ' : Char; axiom ord(' ') = 160; op '¡' : Char; axiom ord('¡') = 161; op '¢' : Char; axiom ord('¢') = 162; op '£' : Char; axiom ord('£') = 163; op '¤' : Char; axiom ord('¤') = 164; op '¥' : Char; axiom ord('¥') = 165; op '¦' : Char; axiom ord('¦') = 166; op '§' : Char; axiom ord('§') = 167; op '¨' : Char; axiom ord('¨') = 168; op '©' : Char; axiom ord('©') = 169; op 'ª' : Char; axiom ord('ª') = 170; op '«' : Char; axiom ord('«') = 171; op '¬' : Char; axiom ord('¬') = 172; op '­' : Char; axiom ord('­') = 173; op '®' : Char; axiom ord('®') = 174; op '¯' : Char; axiom ord('¯') = 175; op '°' : Char; axiom ord('°') = 176; op '±' : Char; axiom ord('±') = 177; op '²' : Char; axiom ord('²') = 178; op '³' : Char; axiom ord('³') = 179; op '´' : Char; axiom ord('´') = 180; op 'µ' : Char; axiom ord('µ') = 181; op '¶' : Char; axiom ord('¶') = 182; op '·' : Char; axiom ord('·') = 183; op '¸' : Char; axiom ord('¸') = 184; op '¹' : Char; axiom ord('¹') = 185; op 'º' : Char; axiom ord('º') = 186; op '»' : Char; axiom ord('»') = 187; op '¼' : Char; axiom ord('¼') = 188; op '½' : Char; axiom ord('½') = 189; op '¾' : Char; axiom ord('¾') = 190; op '¿' : Char; axiom ord('¿') = 191; op 'À' : Char; axiom ord('À') = 192; op 'Á' : Char; axiom ord('Á') = 193; op 'Â' : Char; axiom ord('Â') = 194; op 'Ã' : Char; axiom ord('Ã') = 195; op 'Ä' : Char; axiom ord('Ä') = 196; op 'Å' : Char; axiom ord('Å') = 197; op 'Æ' : Char; axiom ord('Æ') = 198; op 'Ç' : Char; axiom ord('Ç') = 199; op 'È' : Char; axiom ord('È') = 200; op 'É' : Char; axiom ord('É') = 201; op 'Ê' : Char; axiom ord('Ê') = 202; op 'Ë' : Char; axiom ord('Ë') = 203; op 'Ì' : Char; axiom ord('Ì') = 204; op 'Í' : Char; axiom ord('Í') = 205; op 'Î' : Char; axiom ord('Î') = 206; op 'Ï' : Char; axiom ord('Ï') = 207; op 'Ð' : Char; axiom ord('Ð') = 208; op 'Ñ' : Char; axiom ord('Ñ') = 209; op 'Ò' : Char; axiom ord('Ò') = 210; op 'Ó' : Char; axiom ord('Ó') = 211; op 'Ô' : Char; axiom ord('Ô') = 212; op 'Õ' : Char; axiom ord('Õ') = 213; op 'Ö' : Char; axiom ord('Ö') = 214; op '×' : Char; axiom ord('×') = 215; op 'Ø' : Char; axiom ord('Ø') = 216; op 'Ù' : Char; axiom ord('Ù') = 217; op 'Ú' : Char; axiom ord('Ú') = 218; op 'Û' : Char; axiom ord('Û') = 219; op 'Ü' : Char; axiom ord('Ü') = 220; op 'Ý' : Char; axiom ord('Ý') = 221; op 'Þ' : Char; axiom ord('Þ') = 222; op 'ß' : Char; axiom ord('ß') = 223; op 'à' : Char; axiom ord('à') = 224; op 'á' : Char; axiom ord('á') = 225; op 'â' : Char; axiom ord('â') = 226; op 'ã' : Char; axiom ord('ã') = 227; op 'ä' : Char; axiom ord('ä') = 228; op 'å' : Char; axiom ord('å') = 229; op 'æ' : Char; axiom ord('æ') = 230; op 'ç' : Char; axiom ord('ç') = 231; op 'è' : Char; axiom ord('è') = 232; op 'é' : Char; axiom ord('é') = 233; op 'ê' : Char; axiom ord('ê') = 234; op 'ë' : Char; axiom ord('ë') = 235; op 'ì' : Char; axiom ord('ì') = 236; op 'í' : Char; axiom ord('í') = 237; op 'î' : Char; axiom ord('î') = 238; op 'ï' : Char; axiom ord('ï') = 239; op 'ð' : Char; axiom ord('ð') = 240; op 'ñ' : Char; axiom ord('ñ') = 241; op 'ò' : Char; axiom ord('ò') = 242; op 'ó' : Char; axiom ord('ó') = 243; op 'ô' : Char; axiom ord('ô') = 244; op 'õ' : Char; axiom ord('õ') = 245; op 'ö' : Char; axiom ord('ö') = 246; op '÷' : Char; axiom ord('÷') = 247; op 'ø' : Char; axiom ord('ø') = 248; op 'ù' : Char; axiom ord('ù') = 249; op 'ú' : Char; axiom ord('ú') = 250; op 'û' : Char; axiom ord('û') = 251; op 'ü' : Char; axiom ord('ü') = 252; op 'ý' : Char; axiom ord('ý') = 253; op 'þ' : Char; axiom ord('þ') = 254; op 'ÿ' : Char; axiom ord('ÿ') = 255; %% definition of the predicates: var c:Char . isLetter(c) <=> ( (ord('A') < ord(c) /\ ord(c) < ord('Z')) \/ (ord('a') < ord(c) /\ ord(c) < ord('z')) ) . isDigit(c) <=> ord('0') < ord(c) /\ ord(c) < ord('9') . isPrintable(c) <=> ( (ord(' ') < ord(c) /\ ord(c) < ord('~') ) \/ (ord(' ') < ord(c) /\ ord(c) < ord('ÿ')) ) end %% alternative definition of characters as '\nnn': spec Char2 = Char1 then op '\000' : Char; axiom ord('\000') = 0; op '\001' : Char; axiom ord('\001') = 1; op '\002' : Char; axiom ord('\002') = 2; op '\003' : Char; axiom ord('\003') = 3; op '\004' : Char; axiom ord('\004') = 4; op '\005' : Char; axiom ord('\005') = 5; op '\006' : Char; axiom ord('\006') = 6; op '\007' : Char; axiom ord('\007') = 7; op '\008' : Char; axiom ord('\008') = 8; op '\009' : Char; axiom ord('\009') = 9; op '\010' : Char; axiom ord('\010') = 10; op '\011' : Char; axiom ord('\011') = 11; op '\012' : Char; axiom ord('\012') = 12; op '\013' : Char; axiom ord('\013') = 13; op '\014' : Char; axiom ord('\014') = 14; op '\015' : Char; axiom ord('\015') = 15; op '\016' : Char; axiom ord('\016') = 16; op '\017' : Char; axiom ord('\017') = 17; op '\018' : Char; axiom ord('\018') = 18; op '\019' : Char; axiom ord('\019') = 19; op '\020' : Char; axiom ord('\020') = 20; op '\021' : Char; axiom ord('\021') = 21; op '\022' : Char; axiom ord('\022') = 22; op '\023' : Char; axiom ord('\023') = 23; op '\024' : Char; axiom ord('\024') = 24; op '\025' : Char; axiom ord('\025') = 25; op '\026' : Char; axiom ord('\026') = 26; op '\027' : Char; axiom ord('\027') = 27; op '\028' : Char; axiom ord('\028') = 28; op '\029' : Char; axiom ord('\029') = 29; op '\030' : Char; axiom ord('\030') = 30; op '\031' : Char; axiom ord('\031') = 31; op '\032' : Char; axiom ord('\032') = 32; op '\033' : Char; axiom ord('\033') = 33; op '\034' : Char; axiom ord('\034') = 34; op '\035' : Char; axiom ord('\035') = 35; op '\036' : Char; axiom ord('\036') = 36; op '\037' : Char; axiom ord('\037') = 37; op '\038' : Char; axiom ord('\038') = 38; op '\039' : Char; axiom ord('\039') = 39; op '\040' : Char; axiom ord('\040') = 40; op '\041' : Char; axiom ord('\041') = 41; op '\042' : Char; axiom ord('\042') = 42; op '\043' : Char; axiom ord('\043') = 43; op '\044' : Char; axiom ord('\044') = 44; op '\045' : Char; axiom ord('\045') = 45; op '\046' : Char; axiom ord('\046') = 46; op '\047' : Char; axiom ord('\047') = 47; op '\048' : Char; axiom ord('\048') = 48; op '\049' : Char; axiom ord('\049') = 49; op '\050' : Char; axiom ord('\050') = 50; op '\051' : Char; axiom ord('\051') = 51; op '\052' : Char; axiom ord('\052') = 52; op '\053' : Char; axiom ord('\053') = 53; op '\054' : Char; axiom ord('\054') = 54; op '\055' : Char; axiom ord('\055') = 55; op '\056' : Char; axiom ord('\056') = 56; op '\057' : Char; axiom ord('\057') = 57; op '\058' : Char; axiom ord('\058') = 58; op '\059' : Char; axiom ord('\059') = 59; op '\060' : Char; axiom ord('\060') = 60; op '\061' : Char; axiom ord('\061') = 61; op '\062' : Char; axiom ord('\062') = 62; op '\063' : Char; axiom ord('\063') = 63; op '\064' : Char; axiom ord('\064') = 64; op '\065' : Char; axiom ord('\065') = 65; op '\066' : Char; axiom ord('\066') = 66; op '\067' : Char; axiom ord('\067') = 67; op '\068' : Char; axiom ord('\068') = 68; op '\069' : Char; axiom ord('\069') = 69; op '\070' : Char; axiom ord('\070') = 70; op '\071' : Char; axiom ord('\071') = 71; op '\072' : Char; axiom ord('\072') = 72; op '\073' : Char; axiom ord('\073') = 73; op '\074' : Char; axiom ord('\074') = 74; op '\075' : Char; axiom ord('\075') = 75; op '\076' : Char; axiom ord('\076') = 76; op '\077' : Char; axiom ord('\077') = 77; op '\078' : Char; axiom ord('\078') = 78; op '\079' : Char; axiom ord('\079') = 79; op '\080' : Char; axiom ord('\080') = 80; op '\081' : Char; axiom ord('\081') = 81; op '\082' : Char; axiom ord('\082') = 82; op '\083' : Char; axiom ord('\083') = 83; op '\084' : Char; axiom ord('\084') = 84; op '\085' : Char; axiom ord('\085') = 85; op '\086' : Char; axiom ord('\086') = 86; op '\087' : Char; axiom ord('\087') = 87; op '\088' : Char; axiom ord('\088') = 88; op '\089' : Char; axiom ord('\089') = 89; op '\090' : Char; axiom ord('\090') = 90; op '\091' : Char; axiom ord('\091') = 91; op '\092' : Char; axiom ord('\092') = 92; op '\093' : Char; axiom ord('\093') = 93; op '\094' : Char; axiom ord('\094') = 94; op '\095' : Char; axiom ord('\095') = 95; op '\096' : Char; axiom ord('\096') = 96; op '\097' : Char; axiom ord('\097') = 97; op '\098' : Char; axiom ord('\098') = 98; op '\099' : Char; axiom ord('\099') = 99; op '\100' : Char; axiom ord('\100') = 100; op '\101' : Char; axiom ord('\101') = 101; op '\102' : Char; axiom ord('\102') = 102; op '\103' : Char; axiom ord('\103') = 103; op '\104' : Char; axiom ord('\104') = 104; op '\105' : Char; axiom ord('\105') = 105; op '\106' : Char; axiom ord('\106') = 106; op '\107' : Char; axiom ord('\107') = 107; op '\108' : Char; axiom ord('\108') = 108; op '\109' : Char; axiom ord('\109') = 109; op '\110' : Char; axiom ord('\110') = 110; op '\111' : Char; axiom ord('\111') = 111; op '\112' : Char; axiom ord('\112') = 112; op '\113' : Char; axiom ord('\113') = 113; op '\114' : Char; axiom ord('\114') = 114; op '\115' : Char; axiom ord('\115') = 115; op '\116' : Char; axiom ord('\116') = 116; op '\117' : Char; axiom ord('\117') = 117; op '\118' : Char; axiom ord('\118') = 118; op '\119' : Char; axiom ord('\119') = 119; op '\120' : Char; axiom ord('\120') = 120; op '\121' : Char; axiom ord('\121') = 121; op '\122' : Char; axiom ord('\122') = 122; op '\123' : Char; axiom ord('\123') = 123; op '\124' : Char; axiom ord('\124') = 124; op '\125' : Char; axiom ord('\125') = 125; op '\126' : Char; axiom ord('\126') = 126; op '\127' : Char; axiom ord('\127') = 127; op '\128' : Char; axiom ord('\128') = 128; op '\129' : Char; axiom ord('\129') = 129; op '\130' : Char; axiom ord('\130') = 130; op '\131' : Char; axiom ord('\131') = 131; op '\132' : Char; axiom ord('\132') = 132; op '\133' : Char; axiom ord('\133') = 133; op '\134' : Char; axiom ord('\134') = 134; op '\135' : Char; axiom ord('\135') = 135; op '\136' : Char; axiom ord('\136') = 136; op '\137' : Char; axiom ord('\137') = 137; op '\138' : Char; axiom ord('\138') = 138; op '\139' : Char; axiom ord('\139') = 139; op '\140' : Char; axiom ord('\140') = 140; op '\141' : Char; axiom ord('\141') = 141; op '\142' : Char; axiom ord('\142') = 142; op '\143' : Char; axiom ord('\143') = 143; op '\144' : Char; axiom ord('\144') = 144; op '\145' : Char; axiom ord('\145') = 145; op '\146' : Char; axiom ord('\146') = 146; op '\147' : Char; axiom ord('\147') = 147; op '\148' : Char; axiom ord('\148') = 148; op '\149' : Char; axiom ord('\149') = 149; op '\150' : Char; axiom ord('\150') = 150; op '\151' : Char; axiom ord('\151') = 151; op '\152' : Char; axiom ord('\152') = 152; op '\153' : Char; axiom ord('\153') = 153; op '\154' : Char; axiom ord('\154') = 154; op '\155' : Char; axiom ord('\155') = 155; op '\156' : Char; axiom ord('\156') = 156; op '\157' : Char; axiom ord('\157') = 157; op '\158' : Char; axiom ord('\158') = 158; op '\159' : Char; axiom ord('\159') = 159; op '\160' : Char; axiom ord('\160') = 160; op '\161' : Char; axiom ord('\161') = 161; op '\162' : Char; axiom ord('\162') = 162; op '\163' : Char; axiom ord('\163') = 163; op '\164' : Char; axiom ord('\164') = 164; op '\165' : Char; axiom ord('\165') = 165; op '\166' : Char; axiom ord('\166') = 166; op '\167' : Char; axiom ord('\167') = 167; op '\168' : Char; axiom ord('\168') = 168; op '\169' : Char; axiom ord('\169') = 169; op '\170' : Char; axiom ord('\170') = 170; op '\171' : Char; axiom ord('\171') = 171; op '\172' : Char; axiom ord('\172') = 172; op '\173' : Char; axiom ord('\173') = 173; op '\174' : Char; axiom ord('\174') = 174; op '\175' : Char; axiom ord('\175') = 175; op '\176' : Char; axiom ord('\176') = 176; op '\177' : Char; axiom ord('\177') = 177; op '\178' : Char; axiom ord('\178') = 178; op '\179' : Char; axiom ord('\179') = 179; op '\180' : Char; axiom ord('\180') = 180; op '\181' : Char; axiom ord('\181') = 181; op '\182' : Char; axiom ord('\182') = 182; op '\183' : Char; axiom ord('\183') = 183; op '\184' : Char; axiom ord('\184') = 184; op '\185' : Char; axiom ord('\185') = 185; op '\186' : Char; axiom ord('\186') = 186; op '\187' : Char; axiom ord('\187') = 187; op '\188' : Char; axiom ord('\188') = 188; op '\189' : Char; axiom ord('\189') = 189; op '\190' : Char; axiom ord('\190') = 190; op '\191' : Char; axiom ord('\191') = 191; op '\192' : Char; axiom ord('\192') = 192; op '\193' : Char; axiom ord('\193') = 193; op '\194' : Char; axiom ord('\194') = 194; op '\195' : Char; axiom ord('\195') = 195; op '\196' : Char; axiom ord('\196') = 196; op '\197' : Char; axiom ord('\197') = 197; op '\198' : Char; axiom ord('\198') = 198; op '\199' : Char; axiom ord('\199') = 199; op '\200' : Char; axiom ord('\200') = 200; op '\201' : Char; axiom ord('\201') = 201; op '\202' : Char; axiom ord('\202') = 202; op '\203' : Char; axiom ord('\203') = 203; op '\204' : Char; axiom ord('\204') = 204; op '\205' : Char; axiom ord('\205') = 205; op '\206' : Char; axiom ord('\206') = 206; op '\207' : Char; axiom ord('\207') = 207; op '\208' : Char; axiom ord('\208') = 208; op '\209' : Char; axiom ord('\209') = 209; op '\210' : Char; axiom ord('\210') = 210; op '\211' : Char; axiom ord('\211') = 211; op '\212' : Char; axiom ord('\212') = 212; op '\213' : Char; axiom ord('\213') = 213; op '\214' : Char; axiom ord('\214') = 214; op '\215' : Char; axiom ord('\215') = 215; op '\216' : Char; axiom ord('\216') = 216; op '\217' : Char; axiom ord('\217') = 217; op '\218' : Char; axiom ord('\218') = 218; op '\219' : Char; axiom ord('\219') = 219; op '\220' : Char; axiom ord('\220') = 220; op '\221' : Char; axiom ord('\221') = 221; op '\222' : Char; axiom ord('\222') = 222; op '\223' : Char; axiom ord('\223') = 223; op '\224' : Char; axiom ord('\224') = 224; op '\225' : Char; axiom ord('\225') = 225; op '\226' : Char; axiom ord('\226') = 226; op '\227' : Char; axiom ord('\227') = 227; op '\228' : Char; axiom ord('\228') = 228; op '\229' : Char; axiom ord('\229') = 229; op '\230' : Char; axiom ord('\230') = 230; op '\231' : Char; axiom ord('\231') = 231; op '\232' : Char; axiom ord('\232') = 232; op '\233' : Char; axiom ord('\233') = 233; op '\234' : Char; axiom ord('\234') = 234; op '\235' : Char; axiom ord('\235') = 235; op '\236' : Char; axiom ord('\236') = 236; op '\237' : Char; axiom ord('\237') = 237; op '\238' : Char; axiom ord('\238') = 238; op '\239' : Char; axiom ord('\239') = 239; op '\240' : Char; axiom ord('\240') = 240; op '\241' : Char; axiom ord('\241') = 241; op '\242' : Char; axiom ord('\242') = 242; op '\243' : Char; axiom ord('\243') = 243; op '\244' : Char; axiom ord('\244') = 244; op '\245' : Char; axiom ord('\245') = 245; op '\246' : Char; axiom ord('\246') = 246; op '\247' : Char; axiom ord('\247') = 247; op '\248' : Char; axiom ord('\248') = 248; op '\249' : Char; axiom ord('\249') = 249; op '\250' : Char; axiom ord('\250') = 250; op '\251' : Char; axiom ord('\251') = 251; op '\252' : Char; axiom ord('\252') = 252; op '\253' : Char; axiom ord('\253') = 253; op '\254' : Char; axiom ord('\254') = 254; op '\255' : Char; axiom ord('\255') = 255; end spec String = List [Char with sorts Nat, Pos, Char, preds __ < __,__ > __,__<__,__>__, isLetter, isDigit, isPrintable, ops 0, suc, pre, +__, abs, __ + __, __ - __, __ * __, __ div __, __ mod __, min, max, __ ^ __, 1,2,3,4,5,6,7,8,9, __ :: __, chr, ord ] with sorts List[Char] |-> String, NonEmptyList[Char] |-> NonEmptyString, preds empty, ops __::__, last, length, __ ++ __, reverse, take, drop end spec BasicDatatypes = {} end