fmod BINARY is protecting INT . sorts Bit Bits . subsort Bit < Bits . ops 0 1 : -> Bit . op __ : Bits Bits -> Bits [assoc prec 1 gather (e E)] . op |_| : Bits -> Int . op normalize : Bits -> Bits . op bits : Bits Int Int -> Bits . op _++_ : Bits Bits -> Bits [assoc comm prec 5 gather (E e)] . op _**_ : Bits Bits -> Bits [assoc comm prec 4 gather (E e)] . op _>_ : Bits Bits -> Bool [prec 6 gather (E E)] . op not_ : Bits -> Bits [prec 2 gather (E)] . op _-- : Bits -> Bits [prec 2 gather (E)] . vars S T : Bits . vars B C : Bit . var L : Bool . vars I J : Int . *** Length eq | B | = 1 . eq | S B | = | S | + 1 . *** Extract Bits... eq bits(S B,0,0) = B . eq bits(B,J,0) = B . ceq bits(S B,J,0) = bits(S, J - 1,0) B if J > 0 . ceq bits(S B,J,I) = bits(S,J - 1,I - 1) if I > 0 and J > 0 . *** Not eq not (S T) = (not S) (not T) . eq not 0 = 1 . eq not 1 = 0 . *** Normalize supresses zeros at the *** left of a binary number eq normalize(0) = 0 . eq normalize(1) = 1 . eq normalize(0 S) = normalize(S) . eq normalize(1 S) = 1 S . *** Greater than eq 0 > S = false . eq 1 > (0).Bit = true . eq 1 > (1).Bit = false . eq B > (0 S) = B > S . eq B > (1 S) = false . eq (1 S) > B = true . eq (B S) > (C T) = if | normalize(B S) | > | normalize(C T) | then true else if | normalize(B S) | < | normalize(C T) | then false else (S > T) fi fi . *** Binary addition eq 0 ++ S = S . eq 1 ++ 1 = 1 0 . eq 1 ++ (T 0) = T 1 . eq 1 ++ (T 1) = (T ++ 1) 0 . eq (S B) ++ (T 0) = (S ++ T) B . eq (S 1) ++ (T 1) = (S ++ T ++ 1) 0 . *** Binary multiplication eq 0 ** T = 0 . eq 1 ** T = T . eq (S B) ** T = ((S ** T) 0) ++ (B ** T) . *** Decrement eq 0 -- = 0 . eq 1 -- = 0 . eq (S 1) -- = normalize(S 0) . ceq (S 0) -- = normalize(S --) 1 if normalize(S) =/= 0 . ceq (S 0) -- = 0 if normalize(S) == 0 . endfm