new example 'cursor'

these are experiments following the working group on June 6, 2014

examples/cursor.mlw

+
+(** Cursors
+
+   TO BE DISCUSSED
+   - a [coherent] predicate is also convenient for an immutable collection
+   - having [next] raising an exception imposes a try-with around the loop
+     it is simpler to have [next] with a precondition together with
+     an operation [has_next]
+
+  QUESTION: in IntListCursor, field to_do is no more ghost; will it be
+  allowed by refinement? otherwise, simply add a non-ghost field
+  identical to to_do
+*)
+
+module IterableList
+  use import list.List
+
+  type t
+    (** the collection *)
+  type elt
+    (** the type of its elements *)
+
+  type cursor = private {
+    mutable ghost done_: list elt; (** already processed *)
+    mutable ghost to_do: list elt; (** yet to be processed *)
+  }
+
+  predicate coherent t cursor
+
+  val create (t: t) : cursor
+    ensures { result.done_ = Nil }
+    ensures { coherent t result }
+
+  val has_next (t: t) (c: cursor) : bool
+    requires { coherent t c }
+    ensures  { result <-> c.to_do <> Nil }
+
+  val next (t: t) (c: cursor) : elt
+    requires { c.to_do <> Nil }
+    requires { coherent t c }
+    writes   { c }
+    ensures  { match old c.to_do with
+               | Nil -> false
+               | Cons x l -> result = x /\ c.done_ = Cons x (old c.done_) /\
+                             c.to_do = l end }
+    ensures  { coherent t c }
+
+end
+
+(** {2 Iteration over an immuable collection}
+
+    here we choose a list of integers *)
+
+module IntListCursor (* : IterableList *)
+
+  use import int.Int
+  use import list.List
+  use import list.RevAppend
+
+  type t = list int
+  type elt = int
+
+  type cursor = {
+    mutable ghost done_: list elt; (** already processed *)
+    mutable       to_do: list elt; (** yet to be processed *)
+  }
+
+  predicate coherent (t: t) (c: cursor) =
+    t = rev_append c.done_ c.to_do
+
+  let create (t: t) : cursor
+    ensures { result.done_ = Nil }
+    ensures { coherent t result }
+  =
+    { done_ = Nil; to_do = t }
+
+  let has_next (t: t) (c: cursor) : bool
+    requires { coherent t c }
+    ensures  { result <-> c.to_do <> Nil }
+  =
+    c.to_do <> Nil
+
+  let next (t: t) (c: cursor) : elt
+    requires { c.to_do <> Nil }
+    requires { coherent t c }
+    writes   { c }
+    ensures  { match old c.to_do with
+               | Nil -> false
+               | Cons x l -> result = x /\ c.done_ = Cons x (old c.done_) /\
+                             c.to_do = l end }
+    ensures  { coherent t c }
+  =
+    match c.to_do with
+    | Nil -> absurd
+    | Cons x r -> c.to_do <- r; c.done_ <- Cons x c.done_; x
+    end
+
+end
+
+module TestListCursor
+
+  use import int.Int
+  use import list.List
+  use import list.Length
+  use import list.Sum
+  use import ref.Refint
+  use import IntListCursor
+
+  let list_sum (l: list int) : int
+    ensures { result = sum l }
+  =
+    let s = ref 0 in
+    let c = create l in
+    while has_next l c do
+      invariant { sum l = !s + sum c.to_do }
+      invariant { coherent l c }
+      variant   { length c.to_do }
+      let x = next l c in
+      s += x
+    done;
+    !s
+
+end
+
+(** {2 Iteration over a muable collection}
+
+    here we choose an array of integers *)
+
+module IntArrayCursor (* : IterableList *)
+
+  use import int.Int
+  use import array.Array
+  use import list.List
+  use import list.Reverse
+  use import array.ToList
+
+  type t = array int
+  type elt = int
+
+  type cursor = {
+    mutable ghost done_: list elt; (** already processed *)
+    mutable ghost to_do: list elt; (** yet to be processed *)
+    mutable       index: int;      (** index of next element *)
+  }
+
+  predicate coherent (t: t) (c: cursor) =
+    0 <= c.index <= length t /\
+    c.to_do = to_list t c.index (length t) /\
+    c.done_ = reverse (to_list t 0 c.index)
+
+  let create (t: t) : cursor
+    ensures { result.done_ = Nil }
+    ensures { coherent t result }
+  =
+    { done_ = Nil; to_do = to_list t 0 (length t); index = 0; }
+
+  let has_next (t: t) (c: cursor) : bool
+    requires { coherent t c }
+    ensures  { result <-> c.to_do <> Nil }
+  =
+    c.index < length t
+
+  let rec lemma reverse_cons (a: array int) (l u: int)
+    requires { l <= u }
+    ensures  { reverse (to_list a l (u+1)) =
+               Cons a[u] (reverse (to_list a l u)) }
+    variant  { u - l }
+  = if l < u then reverse_cons a (l+1) u
+
+  let next (t: t) (c: cursor) : elt
+    requires { c.to_do <> Nil }
+    requires { coherent t c }
+    writes   { c }
+    ensures  { match old c.to_do with
+               | Nil -> false
+               | Cons x l -> result = x /\ c.done_ = Cons x (old c.done_) /\
+                             c.to_do = l end }
+    ensures  { coherent t c }
+  =
+    match c.to_do with
+    | Nil -> absurd
+    | Cons x r -> c.to_do <- r; c.done_ <- Cons x c.done_
+    end;
+    let x = t[c.index] in
+    c.index <- c.index + 1;
+    x
+
+end
+
+module TestArrayCursor
+
+  use import int.Int
+  use list.Sum as L
+  use list.Length as LL
+  use import array.Array
+  use import array.ArraySum
+  use import array.ToList
+  use import ref.Refint
+  use import IntArrayCursor
+
+  let rec lemma array_sum_array_to_list (a: array int) (l u: int) : unit
+    ensures { sum a l u = L.sum (to_list a l u) } variant { u-l }
+  = if l < u then array_sum_array_to_list a (l+1) u
+
+  let array_sum (a: array int) : int
+    ensures { result = sum a 0 (length a) }
+  =
+    let s = ref 0 in
+    let c = create a in
+    while has_next a c do
+      invariant { sum a 0 (length a) = !s + L.sum c.to_do }
+      invariant { coherent a c }
+      variant   { LL.length c.to_do }
+      let x = next a c in
+      s += x
+    done;
+    !s
+
+end