(* bits.rml -- Inductively defined bitstrings, with: (1) a datasort refinement: bits = any bitstring, std = "standardized" bitstrings, i.e. with no leading zeros, pos = standardized bitstrings of nonzero value (i.e. not the empty bitstring). (2) index refinement: (length, value) where length : nat = the length of the bitstring, value : nat = the number represented. *) (*[ datasort bits : pos <= std; std <= bits datacon E : std(0, 0) datacon Zero : -all len, value : nat- pos(len, value) -> pos(len+1, 2*value) & bits(len, value) -> bits(len+1, 2*value) datacon One : -all len, value : nat- std(len, value) -> pos(len+1, 2*value + 1) & bits(len, value) -> bits(len+1, 2*value + 1) datatype bits with nat * nat ]*) datatype bits = E | Zero of bits | One of bits ; (*[ val xx : std(0, 0) ]*) val xx = E (*[ val yy : bits(2, 1) ]*) val yy = One (Zero (E)) (* e01 : Leading zero *) (*[ val zz : pos (2, 2) ]*) val zz = Zero (One (E)) (* e10 : No leading zero *) (*[ val zz' : pos(6, 43) ]*) val zz' = One (One (Zero (One (Zero (One (E)))))) (* e101011 : No leading zero *) (*[ val inc : -all len, value : nat- std(len, value) -> pos(len, value+1) \/ pos(len+1, value+1) & bits(len, value) -> bits(len, value+1) \/ bits(len+1, value+1) ]*) fun inc n = case n of E => One E | Zero n => One n | One n => Zero (inc n) (*[ val add : -all len1, len2, val1, val2 : nat- bits(len1, val1) * bits(len2, val2) -> (-exists len : nat- [len >= len1 and len >= len2] bits(len, val1 + val2)) ]*) fun add arg = case arg of (x, E) => x | (E, y) => y | (Zero x', Zero y') => Zero (add (x', y')) | (One x', Zero y') => One (add (x', y')) | (x, One y') => inc (add (x, Zero y')) (*[ val toInt :! -all len, value : nat- bits(len, value) -> int(value) ]*) fun toInt n = case n of E => 0 | Zero n' => 2 * toInt n' | One n' => (2 * toInt n) + 1 (* BUG *) (*[ val toInt : -all len, value : nat- bits(len, value) -> int(value) ]*) fun toInt n = case n of E => 0 | Zero n' => 2 * toInt n' | One n' => (2 * toInt n') + 1 (*[ val length : -all len, value : nat- bits(len, value) -> int(len) ]*) fun length n = case n of E => 0 | Zero n' => 1 + length n' | One n' => 1 + length n' (* Can't properly check spec because div, mod not supported by constraint solver (*[ val fromInt : -all value : nat- int(value) -> -exists len : nat- std(len, value) ]*) *) (* Weak specification: *) (*[ val fromInt : int -> bits ]*) fun fromInt n = if n = 0 then E else let val d = fromInt (n div 2) val r = n mod 2 in if r = 0 then Zero d else One d end