examples/string_hex_encoding.mlw

   1
   2 (** {1 Hexadecimal encoding and decoding of a string}
   3
   4   Implementation of functions to encode and decode strings into
   5   hexadecimal.
   6
   7   The length of the encoded string is always twice the length of the
   8   input string.
   9 *)
  10
  11 use mach.int.Int
  12 use mach.int.Int63
  13 use string.String
  14 use string.Char
  15 use string.OCaml
  16 use string.StringBuffer
  17
  18 (** `valid_hex_char c` is true, if and only if, `c` is a valid
  19 hexadecimal character *)
  20 predicate valid_hex_char (c: char) =
  21   48 <= code c < 58 || 65 <= code c < 71
  22
  23 (** `hex i` gives the `i`th hexadecimal value, for `0 <= i < 16` or
  24 `0` otherwise. *)
  25 function hex (i: int) : char =
  26   if 0 <= i < 10 then chr (i + 48)
  27   else if 10 <= i < 16 then chr (i + 55)
  28   else "\000"[0]
  29
  30 let hex (i: int63) : char
  31   requires { 0 <= i < 16 }
  32   ensures  { result = hex i }
  33 = if i < 10 then chr (i + 48) else chr (i + 55)
  34
  35 (** `xeh c` gives the index of the hexadecimal value `c`, if `c` is a
  36 valid hexadecimal value or `-1` otherwise *)
  37 function xeh (c: char) : int =
  38   if 48 <= code c < 58 then code c - 48
  39   else if 65 <= code c < 71 then code c - 55
  40   else -1
  41
  42 let xeh (c: char) : int63
  43   requires { valid_hex_char c }
  44   ensures  { result = xeh c }
  45 = if 48 <= code c < 58 then code c - 48
  46   else code c - 55
  47
  48 (** checks whether a string contains only valid hexadecimal characters *)
  49 predicate valid_hex (s : string) =
  50   mod (length s) 2 = 0 &&
  51   ( forall i. 0 <= i < length s -> valid_hex_char s[i] )
  52
  53 (** `encoding s1 s2` is true, if and only if, `s2` is an encoding of
  54 `s1` *)
  55 predicate encoding (s1 s2: string) =
  56   length s2 = 2 * length s1 &&
  57   (forall i. 0 <= i < length s1 ->
  58              s1[i] = chr (xeh s2[2 * i] * 16 + xeh s2[2 * i + 1])) &&
  59   valid_hex s2
  60
  61 (** the encoding of a string is unique *)
  62 lemma decode_unique: forall s1 s2 s3.
  63   encoding s1 s2 /\ encoding s3 s2 -> s1 = s3
  64
  65 let encode (s: string) : string
  66   ensures { encoding s result }
  67 = let ref i = 0 in
  68   let r = StringBuffer.create (length s) in
  69   while i < OCaml.length s do
  70     variant { length s - i }
  71     invariant { 0 <= i <= length s }
  72     invariant { length r = 2 * i }
  73     invariant { forall j. 0 <= j < i  ->
  74                   r[2 * j] = hex (div (code s[j]) 16) &&
  75                   r[2 * j + 1] = hex (mod (code s[j]) 16)
  76     }
  77     invariant { forall j. 0 <= j < 2*i -> valid_hex_char r[j]}
  78     let v = code s[i] in
  79     StringBuffer.add_char r (hex (v / 16));
  80     StringBuffer.add_char r (hex (v % 16));
  81     i <- i + 1
  82   done;
  83   StringBuffer.contents r
  84
  85 let decode (s: string) : string
  86   requires { valid_hex s }
  87   ensures  { encoding result s }
  88 = let ref i = 0 in
  89   let r = StringBuffer.create (length s / 2) in
  90   while i < length s do
  91     variant {length s - i}
  92     invariant { mod i 2 = 0 }
  93     invariant { 0 <= i <= length s }
  94     invariant { length r = div i 2 }
  95     invariant { forall j. 0 <= j < div i 2 ->
  96                   r[j] = chr (xeh s[2 * j] * 16 + xeh s[2 * j + 1]) }
  97     let v_i = xeh s[i] in
  98     let v_ii = xeh s[i + 1] in
  99     StringBuffer.add_char r (chr (v_i * 16 + v_ii));
 100     i <- i + 2
 101   done;
 102   StringBuffer.contents r
 103
 104 let decode_encode (s: string) : unit
 105 = let s1 = encode s in
 106   let s2 = decode s1 in
 107   assert { s = s2 }