examples/equality_up_to_spaces.mlw

   1
   2 (** Check that two strings are equal up to space characters.
   3
   4     This problem was suggested by Rustan Leino (Amazon Web Services).
   5     The trick is in finding a loop invariant that makes the proof easy.
   6
   7     Author: Jean-Christophe Filliâtre (CNRS)
   8 *)
   9
  10 use int.Int
  11 use seq.Seq
  12 use seq.FreeMonoid
  13
  14 type char
  15 val constant space: char
  16 val function eq (x y: char): bool ensures { result <-> x = y }
  17 type char_string = seq char
  18
  19 (** The specification uses a function `remove_spaces`.
  20     It is recursively defined over a string, from left to right. *)
  21
  22 let rec function remove_spaces (s: char_string) : char_string
  23   variant { length s }
  24 =      if length s = 0  then s
  25   else if eq s[0] space then remove_spaces s[1..]
  26                         else cons s[0] (remove_spaces s[1..])
  27
  28 (** Code and proof.
  29
  30    It would be natural to have a loop invariant such as
  31
  32      remove_spaces x[..i] = remove_spaces y[..j]
  33
  34    Unfortunately, since `remove_spaces` is defined recursively from
  35    left to right, we would have hard time proving such an invariant.
  36    So instead we use an invariant which refers to the *suffixes* of `x`
  37    and `y`. *)
  38
  39 let rec compare_up_to_spaces (x y: char_string) : bool
  40   ensures { result <-> remove_spaces x = remove_spaces y }
  41 = let n = length x in
  42   let m = length y in
  43   let ref i = 0 in
  44   let ref j = 0 in
  45   while i < n || j < m do
  46     invariant { 0 <= i <= n }
  47     invariant { 0 <= j <= m }
  48     invariant { remove_spaces x      = remove_spaces y
  49             <-> remove_spaces x[i..] = remove_spaces y[j..] }
  50     variant   { n - i + m - j }
  51     if i < n && eq x[i] space then begin
  52       assert { remove_spaces x[i..] == remove_spaces x[i+1..] };
  53       i <- i + 1
  54     end else if j < m && eq y[j] space then begin
  55       assert { remove_spaces y[j..] == remove_spaces y[j+1..] };
  56       j <- j + 1
  57     end else begin
  58       assert { i < n ->
  59                remove_spaces x[i..] == cons x[i] (remove_spaces x[i+1..]) };
  60       assert { j < m ->
  61                remove_spaces y[j..] == cons y[j] (remove_spaces y[j+1..]) };
  62       if i = n || j = m then return false;
  63       if not (eq x[i] y[j]) then return false;
  64       i <- i + 1;
  65       j <- j + 1
  66     end
  67   done;
  68   return true