examples/verifythis_2017_tree_buffer.mlw

   1 (**
   2
   3 {1 VerifyThis @ ETAPS 2017 competition
   4    Challenge 4: Tree Buffer}
   5
   6 See https://formal.iti.kit.edu/ulbrich/verifythis2017/
   7
   8 Author: Jean-Christophe Filliâtre (CNRS)
   9 *)
  10
  11 (* default implementation *)
  12 module Spec
  13
  14   use export int.Int
  15   use export list.List
  16
  17   type buf 'a = { h: int; xs: list 'a }
  18
  19   let rec function take (n: int) (l: list 'a) : list 'a =
  20     match l with
  21     | Nil -> Nil
  22     | Cons x xs -> if n = 0 then Nil
  23                    else Cons x (take (n-1) xs) end
  24
  25   let function empty (h: int) : buf 'a =
  26     { h = h; xs = Nil }
  27
  28   let function add (x: 'a) (b: buf 'a) : buf 'a =
  29     { b with xs = Cons x b.xs }
  30
  31   let function get (b: buf 'a) : list 'a =
  32     take b.h b.xs
  33
  34   (* the following lemma is useful to verify both Caterpillar and
  35      RealTime implementations below *)
  36
  37   use list.Append
  38   use list.Length
  39
  40   let rec lemma take_lemma (l1 l2 l3: list 'a) (n: int)
  41     requires { 0 <= n <= length l1 }
  42     ensures  { take n (l1 ++ l2) = take n (l1 ++ l3) }
  43     variant  { l1 }
  44   = match l1 with Nil -> ()
  45     | Cons _ ll1 -> if n > 0 then take_lemma ll1 l2 l3 (n-1) end
  46
  47 end
  48
  49 (* task 1 *)
  50 module Caterpillar
  51
  52   use Spec
  53   use list.Append
  54   use list.Length
  55
  56   type cat 'a = {
  57     ch: int;
  58     xs: list 'a;
  59     xs_len: int;
  60     ys: list 'a;
  61     ghost b: buf 'a; (* the model is the default implementation *)
  62   } invariant {
  63     b.h = ch /\
  64     xs_len = length xs < ch /\
  65     forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
  66   } by {
  67     ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
  68   }
  69
  70   (* for the three operations, the postcondition uses the default
  71   implementation *)
  72
  73   let cat_empty (h: int) : cat 'a
  74     requires { 0 < h }
  75     ensures  { result.b = empty h }
  76   = { ch = h; xs = Nil; xs_len = 0; ys = Nil;
  77       b = empty h }
  78
  79   let cat_add (x: 'a) (c: cat 'a) : cat 'a
  80     ensures { result.b = add x c.b }
  81   = if c.xs_len = c.ch - 1 then
  82       { c with xs = Nil; xs_len = 0; ys = Cons x c.xs;
  83         b = add x c.b }
  84     else
  85       { c with xs = Cons x c.xs; xs_len = 1 + c.xs_len;
  86         b = add x c.b }
  87
  88   let cat_get (c: cat 'a) : list 'a
  89     ensures { result = get c.b }
  90   = take c.ch (c.xs ++ c.ys)
  91
  92 end
  93
  94 (* task 2 *)
  95
  96 (* important note: Why3 assumes a garbage collector and so it makes
  97    little sense to implement the real time solution in Why3.
  98
  99    Yet I stayed close to the C++ code, with a queue to_delete where
 100    lists are added when discarded and then destroyed progressively
 101    (at most two conses at a time) in process_queue.
 102
 103    The C++ code seems to be missing the insertion into to_delete,
 104    which I added to rt_add; see my comment below.
 105 *)
 106
 107 module RealTime
 108
 109   use Spec
 110   use list.Append
 111   use list.Length
 112
 113   (* For technical reasons, the global queue cannot contain
 114      polymorphic values, to we assume values to be of some
 115      abstract type "elt". Anyway, the C++ code assumes integer
 116      elements. *)
 117   type elt
 118
 119   (* not different from the Caterpillar implementation
 120      replacing 'a with elt everywhere *)
 121   type rt = {
 122     ch: int;
 123     xs: list elt;
 124     xs_len: int;
 125     ys: list elt;
 126     ghost b: buf elt; (* the model is the default implementation *)
 127   } invariant {
 128     b.h = ch /\
 129     xs_len = length xs < ch /\
 130     forall len. 0 <= len <= ch -> take len (xs ++ ys) = take len b.xs
 131   } by {
 132     ch = 1; xs = Nil; xs_len = 0; ys = Nil; b = empty 1
 133   }
 134
 135   (* garbage collection *)
 136   use queue.Queue as Q
 137     (* note: when translating Why3 to OCaml, this module is mapped
 138        to OCaml's Queue module, where push and pop are O(1) *)
 139
 140   val to_delete: Q.t (list elt)
 141
 142   let de_allocate (l: list elt)
 143   = match l with Nil -> () | Cons _ xs -> Q.push xs to_delete end
 144
 145   let process_queue ()
 146   = try
 147       if not (Q.is_empty to_delete) then de_allocate (Q.pop to_delete);
 148       if not (Q.is_empty to_delete) then de_allocate (Q.pop to_delete)
 149     with Q.Empty -> absurd end
 150
 151   (* no difference wrt Caterpillar *)
 152   let rt_empty (h: int) : rt
 153     requires { 0 < h }
 154     ensures  { result.b = empty h }
 155   = { ch = h; xs = Nil; xs_len = 0; ys = Nil;
 156       b = empty h }
 157
 158   (* no difference wrt Caterpillar *)
 159   let rt_get (c: rt) : list elt
 160     ensures { result = get c.b }
 161   = take c.ch (c.xs ++ c.ys)
 162
 163   (* this is where we introduce explicit garbage collection
 164      1. process_queue is called first (as in the C++ code)
 165      2. when ys is discarded, it is added to the queue (which
 166         seems to be missing in the C++ code) *)
 167   let rt_add (x: elt) (c: rt) : rt
 168     ensures { result.b = add x c.b }
 169   = process_queue ();
 170     if c.xs_len = c.ch - 1 then begin
 171       Q.push c.ys to_delete;
 172       { c with xs = Nil; xs_len = 0; ys = Cons x c.xs;
 173         b = add x c.b }
 174     end else
 175       { c with xs = Cons x c.xs; xs_len = 1 + c.xs_len;
 176         b = add x c.b }
 177
 178 end