examples/cursor_examples.mlw

   1
   2 (** {1 Cursors}
   3
   4     Some implementations and clients of module `cursor.Cursor`
   5     from the standard library.
   6
   7     Author: Mário Pereira (Université Paris Sud) *)
   8
   9 module TestCursor
  10
  11   use int.Int
  12   use int.Sum
  13   use seq.Seq
  14   use ref.Refint
  15
  16   use cursor.Cursor
  17
  18   (** sums all the remaining elements in the cursor *)
  19   let sum (c: cursor int) : int
  20     requires { permitted c }
  21     requires { c.visited = empty }
  22     ensures  { result = sum (get c.visited) 0 (length c.visited) }
  23     diverges
  24   = let s = ref 0 in
  25     while has_next c do
  26       invariant { permitted c }
  27       invariant { !s = sum (get c.visited) 0 (length c.visited) }
  28       let x = next c in
  29       s += x
  30     done;
  31     !s
  32
  33 end
  34
  35 (** {2 Iteration over an immuable collection}
  36
  37     here we choose a list *)
  38
  39 module ListCursorImpl : cursor.ListCursor
  40
  41   use int.Int
  42   use list.List
  43   use seq.Seq
  44   use seq.OfList
  45
  46   type cursor 'a = {
  47     mutable ghost visited    : seq 'a;
  48             ghost collection : list 'a;
  49     mutable       to_visit   : list 'a;
  50   } invariant { visited ++ to_visit = collection }
  51     by { visited = empty; collection = Nil; to_visit = Nil }
  52
  53   predicate permitted (c: cursor 'a) =
  54     length c.visited <= length c.collection /\
  55     forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
  56
  57   predicate complete (c: cursor 'a) =
  58     length c.visited = length c.collection
  59
  60   let lemma snoc_Cons (s: seq 'a) (l: list 'a) (x: 'a)
  61     ensures { snoc s x ++ l == s ++ Cons x l }
  62   = ()
  63
  64   scope C
  65
  66     let next (c: cursor 'a) : 'a
  67       requires { not (complete c) }
  68       writes   { c }
  69       ensures  { c.visited = snoc (old c).visited result }
  70       ensures  { match (old c).to_visit with
  71                  | Nil -> false
  72                  | Cons x r -> c.to_visit = r /\ x = result
  73                  end }
  74     = match c.to_visit with
  75       | Nil -> absurd
  76       | Cons x r ->
  77         let ghost v0 = c.visited in
  78         c.visited <- snoc c.visited x; c.to_visit <- r;
  79         snoc_Cons v0 r x;
  80         assert { c.to_visit == c.collection [length c.visited ..] };
  81         x
  82       end
  83
  84     let has_next (c: cursor 'a) : bool
  85       ensures { result <-> not (complete c) }
  86     = match c.to_visit with (* could define a [val eq (l1 l2: list 'a) : bool] *)
  87       | Nil -> false
  88       | _   -> true
  89       end
  90
  91   end
  92
  93   let create (t: list 'a) : cursor 'a
  94     ensures { result.visited = empty }
  95     ensures { result.collection = t }
  96     ensures { result.to_visit = t }
  97   = { visited = empty; collection = t; to_visit = t }
  98
  99 end
 100
 101 module TestListCursor
 102
 103   use int.Int
 104   use int.Sum as S
 105   use list.List
 106   use list.Length
 107   use list.Sum
 108   use ref.Refint
 109   use seq.Seq
 110   use seq.OfList
 111
 112   use ListCursorImpl
 113
 114   lemma sum_of_list: forall l: list int.
 115     sum l = S.sum (get (of_list l)) 0 (length l)
 116
 117   let list_sum (l: list int) : int
 118     ensures { result = sum l }
 119   = let s = ref 0 in
 120     let c = create l in
 121     while C.has_next c do
 122       invariant { !s = S.sum (get c.visited) 0 (length c.visited) }
 123       invariant { permitted c }
 124       variant   { length l - length c.visited }
 125       let x = C.next c in
 126       s += x
 127     done;
 128     !s
 129
 130 end
 131
 132 (** {2 Iteration over a mutable collection}
 133
 134     here we choose an array of integers *)
 135
 136 module ArrayCursorImpl : cursor.ArrayCursor
 137
 138   use int.Int
 139   use array.Array
 140   use array.ToSeq
 141   use list.List
 142   use list.Reverse
 143   use array.ToList
 144   use seq.Seq
 145
 146   type cursor 'a = {
 147     mutable ghost visited    : seq 'a;
 148                   collection : seq 'a; (* FIXME : extraction of seq *)
 149     mutable       index      : int;    (** index of next element *)
 150   } invariant { 0 <= index <= length collection /\
 151                 index = length visited /\
 152                 forall i. 0 <= i < index -> collection[i] = visited[i] }
 153     by { visited = empty; collection = empty; index = 0 }
 154
 155   predicate permitted (c: cursor 'a) =
 156     length c.visited <= length c.collection /\
 157     forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
 158
 159   predicate complete (c: cursor 'a) =
 160     length c.visited = length c.collection
 161
 162   let create (a: array 'a) : cursor 'a
 163     ensures { result.visited = empty }
 164     ensures { result.index = 0 }
 165     ensures { result.collection = to_seq a }
 166   = { visited = empty; collection = to_seq a; index = 0; }
 167
 168   scope C
 169
 170     let has_next (c: cursor 'a) : bool
 171       ensures  { result <-> not (complete c) }
 172     = c.index < length c.collection
 173
 174     let next (c: cursor 'a) : 'a
 175       requires { not (complete c) }
 176       writes   { c }
 177       ensures  { c.visited = snoc (old c).visited result }
 178       ensures  { c.index = (old c).index + 1 }
 179     = if c.index >= length c.collection then absurd
 180       else begin let x = c.collection[c.index] in
 181         c.visited <- snoc c.visited x;
 182         c.index <- c.index + 1;
 183         x end
 184
 185   end
 186
 187 end
 188
 189 module TestArrayCursor
 190
 191   use int.Int
 192   use array.Array
 193   use array.ToSeq
 194   use seq.Seq
 195   use int.Sum
 196   use ref.Refint
 197
 198   use ArrayCursorImpl
 199
 200   let array_sum (a: array int) : int
 201     ensures { result = sum (Array.([]) a) 0 (length a) }
 202   = let s = ref 0 in
 203     let c = create a in
 204     while C.has_next c do
 205       invariant { !s = sum (get c.visited) 0 (length c.visited) }
 206       invariant { permitted c }
 207       variant   { length c.collection - length c.visited }
 208       let x = C.next c in
 209       s += x
 210     done;
 211     !s
 212
 213   let harness1 () : unit
 214   = let a = Array.make 42 0 in
 215     let c = create a in
 216     let x = C.next c in
 217     assert { x = 0 }
 218
 219 end