stdlib/byte_string.mlw

   1 module CString
   2
   3   use mach.int.Int
   4   use mach.int.Byte
   5   use export array.Array
   6   use array.ArrayEq
   7
   8   type char = byte
   9   type cstring = array char
  10
  11   exception Break
  12
  13   let (=) (s1 s2: cstring) : bool
  14     ensures {result <-> array_eq s1 s2}
  15   = if s1.length <> s2.length then false else
  16       try
  17         let ref i = 0 in
  18         while i < s1.length do
  19           variant   { s1.length - i }
  20           invariant { 0 <= i <= s1.length }
  21           invariant { forall j. 0 <= j < i -> s1[j] = s2[j] }
  22           if s1[i] <> s2[i] then raise Break;
  23           i <- i + 1
  24         done;
  25         true
  26       with Break -> false end
  27
  28   let function concat (s1 s2: cstring) : cstring
  29     ensures { result.length = s1.length + s2.length }
  30     ensures { forall i. 0 <= i < s1.length -> result[i] = s1[i] }
  31     ensures { forall i. s1.length <= i < result.length ->
  32                           result[i] = s2[i - s1.length] }
  33   = let r = make (s1.length + s2.length) 0 in
  34     let ref i = 0 in
  35     while i < s1.length do
  36       variant   { s1.length - i }
  37       invariant { 0 <= i <= s1.length }
  38       invariant { forall j. 0 <= j < i -> r[j] = s1[j] }
  39       r[i] <- s1[i];
  40       i <- i + 1
  41     done;
  42     while i < s1.length + s2.length do
  43       variant   { s1.length + s2.length - i }
  44       invariant { s1.length <= i <= s1.length + s2.length }
  45       invariant { forall j. 0 <= j < s1.length -> r[j] = s1[j]}
  46       invariant { forall j. s1.length <= j < i -> r[j] = s2[j - s1.length] }
  47       r[i] <- s2[i - s1.length];
  48       i <- i + 1
  49     done;
  50     r
  51
  52   (* use string.String
  53   use string.Char
  54
  55   val function of_string (s: string) : cstring
  56     ensures { String.length s = Array.length result }
  57     ensures { forall i. 0 <= i < String.length s ->
  58                 Array.([]) result i = code (Char.get s i) }
  59   meta coercion function of_string *)
  60
  61 end