why3/examples/cursor_examples.mlw

(** {1 Cursors}

    Some implementations and clients of module `cursor.Cursor`
    from the standard library.

    Author: Mário Pereira (Université Paris Sud) *)

module TestCursor

  use int.Int
  use int.Sum
  use seq.Seq
  use ref.Refint

  use cursor.Cursor

  (** sums all the remaining elements in the cursor *)
  let sum (c: cursor int) : int
    requires { permitted c }
    requires { c.visited = empty }
    ensures  { result = sum (get c.visited) 0 (length c.visited) }
    diverges
  = let s = ref 0 in
    while has_next c do
      invariant { permitted c }
      invariant { !s = sum (get c.visited) 0 (length c.visited) }
      let x = next c in
      s += x
    done;
    !s

end

(** {2 Iteration over an immuable collection}

    here we choose a list *)

module ListCursorImpl : cursor.ListCursor

  use int.Int
  use list.List
  use seq.Seq
  use seq.OfList

  type cursor 'a = {
    mutable ghost visited    : seq 'a;
            ghost collection : list 'a;
    mutable       to_visit   : list 'a;
  } invariant { visited ++ to_visit = collection }
    by { visited = empty; collection = Nil; to_visit = Nil }

  predicate permitted (c: cursor 'a) =
    length c.visited <= length c.collection /\
    forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]

  predicate complete (c: cursor 'a) =
    length c.visited = length c.collection

  let lemma snoc_Cons (s: seq 'a) (l: list 'a) (x: 'a)
    ensures { snoc s x ++ l == s ++ Cons x l }
  = ()

  scope C

    let next (c: cursor 'a) : 'a
      requires { not (complete c) }
      writes   { c }
      ensures  { c.visited = snoc (old c).visited result }
      ensures  { match (old c).to_visit with
                 | Nil -> false
                 | Cons x r -> c.to_visit = r /\ x = result
                 end }
    = match c.to_visit with
      | Nil -> absurd
      | Cons x r ->
        let ghost v0 = c.visited in
        c.visited <- snoc c.visited x; c.to_visit <- r;
        snoc_Cons v0 r x;
        assert { c.to_visit == c.collection [length c.visited ..] };
        x
      end

    let has_next (c: cursor 'a) : bool
      ensures { result <-> not (complete c) }
    = match c.to_visit with (* could define a [val eq (l1 l2: list 'a) : bool] *)
      | Nil -> false
      | _   -> true
      end

  end

  let create (t: list 'a) : cursor 'a
    ensures { result.visited = empty }
    ensures { result.collection = t }
    ensures { result.to_visit = t }
  = { visited = empty; collection = t; to_visit = t }

end

module TestListCursor

  use int.Int
  use int.Sum as S
  use list.List
  use list.Length
  use list.Sum
  use ref.Refint
  use seq.Seq
  use seq.OfList

  use ListCursorImpl

  lemma sum_of_list: forall l: list int.
    sum l = S.sum (get (of_list l)) 0 (length l)

  let list_sum (l: list int) : int
    ensures { result = sum l }
  = let s = ref 0 in
    let c = create l in
    while C.has_next c do
      invariant { !s = S.sum (get c.visited) 0 (length c.visited) }
      invariant { permitted c }
      variant   { length l - length c.visited }
      let x = C.next c in
      s += x
    done;
    !s

end

(** {2 Iteration over a mutable collection}

    here we choose an array of integers *)

module ArrayCursorImpl : cursor.ArrayCursor

  use int.Int
  use array.Array
  use array.ToSeq
  use list.List
  use list.Reverse
  use array.ToList
  use seq.Seq

  type cursor 'a = {
    mutable ghost visited    : seq 'a;
                  collection : seq 'a; (* FIXME : extraction of seq *)
    mutable       index      : int;    (** index of next element *)
  } invariant { 0 <= index <= length collection /\
                index = length visited /\
                forall i. 0 <= i < index -> collection[i] = visited[i] }
    by { visited = empty; collection = empty; index = 0 }

  predicate permitted (c: cursor 'a) =
    length c.visited <= length c.collection /\
    forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]

  predicate complete (c: cursor 'a) =
    length c.visited = length c.collection

  let create (a: array 'a) : cursor 'a
    ensures { result.visited = empty }
    ensures { result.index = 0 }
    ensures { result.collection = to_seq a }
  = { visited = empty; collection = to_seq a; index = 0; }

  scope C

    let has_next (c: cursor 'a) : bool
      ensures  { result <-> not (complete c) }
    = c.index < length c.collection

    let next (c: cursor 'a) : 'a
      requires { not (complete c) }
      writes   { c }
      ensures  { c.visited = snoc (old c).visited result }
      ensures  { c.index = (old c).index + 1 }
    = if c.index >= length c.collection then absurd
      else begin let x = c.collection[c.index] in
        c.visited <- snoc c.visited x;
        c.index <- c.index + 1;
        x end

  end

end

module TestArrayCursor

  use int.Int
  use array.Array
  use array.ToSeq
  use seq.Seq
  use int.Sum
  use ref.Refint

  use ArrayCursorImpl

  let array_sum (a: array int) : int
    ensures { result = sum (Array.([]) a) 0 (length a) }
  = let s = ref 0 in
    let c = create a in
    while C.has_next c do
      invariant { !s = sum (get c.visited) 0 (length c.visited) }
      invariant { permitted c }
      variant   { length c.collection - length c.visited }
      let x = C.next c in
      s += x
    done;
    !s

  let harness1 () : unit
  = let a = Array.make 42 0 in
    let c = create a in
    let x = C.next c in
    assert { x = 0 }

end