Wiki Agenda Contact English version

Cursor examples

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


Auteurs: Mário Pereira

Catégories: Data Structures

Outils: Why3

see also the index (by topic, by tool, by reference, by year)


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

  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

sums all the remaining elements in the cursor

end

Iteration over an immuable collection

here we choose a list

module ListCursorImpl (* : 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 }
  = ()

  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

  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 }

  clone cursor.ListCursor with
    type cursor     = cursor,
    val  create     = create,
    val  C.has_next = has_next,
    val  C.next     = next

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

  clone cursor.ListCursor

  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

module TestListCursorLink

  use ListCursorImpl

  clone TestListCursor with
    type ListCursor.cursor     = cursor,
    val  ListCursor.C.next     = next,
    val  ListCursor.C.has_next = has_next,
    val  ListCursor.create     = create

end

Iteration over a mutable collection

here we choose an array of integers

module ArrayCursorImpl (* : 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; }

  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

  clone cursor.ArrayCursor with
    type cursor   = cursor,
    val  C.next     = next,
    val  C.has_next = has_next,
    val  create     = create

end

module TestArrayCursor

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

  clone cursor.ArrayCursor

  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

module TestArrayCursorLink

  use ArrayCursorImpl

  clone TestArrayCursor with
    type ArrayCursor.cursor     = cursor,
    val  ArrayCursor.C.next     = next,
    val  ArrayCursor.C.has_next = has_next,
    val  ArrayCursor.create     = create

end

download ZIP archive

Why3 Proof Results for Project "cursor_examples"

Theory "cursor_examples.TestCursor": fully verified

ObligationsAlt-Ergo 2.0.0
VC for sum2.86

Theory "cursor_examples.ListCursorImpl": fully verified

ObligationsAlt-Ergo 2.0.0
VC for cursor0.02
VC for snoc_Cons0.04
VC for next0.13
VC for has_next0.01
VC for create0.02
VC for create'refn0.02
VC for next'refn0.02
VC for has_next'refn0.02

Theory "cursor_examples.TestListCursor": fully verified

ObligationsAlt-Ergo 2.0.0
sum_of_list---
induction_ty_lex
sum_of_list.0---
split_goal_right
sum_of_list.0.00.02
sum_of_list.0.13.48
VC for list_sum---
split_goal_right
loop invariant init0.02
loop invariant init0.01
precondition0.01
precondition0.00
precondition0.02
loop variant decrease0.02
loop invariant preservation---
simplify_trivial_quantification
loop invariant preservation4.55
loop invariant preservation0.02
postcondition1.08

Theory "cursor_examples.TestListCursorLink": fully verified

ObligationsAlt-Ergo 2.0.0
VC for create'refn0.02
VC for next'refn0.03
VC for has_next'refn0.01

Theory "cursor_examples.ArrayCursorImpl": fully verified

ObligationsAlt-Ergo 2.0.0
VC for cursor0.02
VC for create0.02
VC for has_next0.02
VC for next0.02
VC for create'refn0.01
VC for next'refn---
split_goal_right
precondition---
split_goal_right
precondition0.03
postcondition0.01
postcondition0.00
VC for has_next'refn0.02

Theory "cursor_examples.TestArrayCursor": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.5Z3 4.6.0
VC for array_sum---------
split_goal_right
loop invariant init0.02------
loop invariant init0.02------
precondition0.01------
precondition0.02------
precondition0.02------
loop variant decrease0.02------
loop invariant preservation3.17------
loop invariant preservation0.02------
postcondition------0.06
VC for harness1---0.16---

Theory "cursor_examples.TestArrayCursorLink": fully verified

ObligationsAlt-Ergo 2.0.0
VC for create'refn0.02
VC for next'refn0.02
VC for has_next'refn0.01