cursor.mlw 2.12 KB
Newer Older
Mário Pereira's avatar
Mário Pereira committed
1 2 3 4 5
module Cursor

  use import seq.Seq

  type cursor 'a = private {
6
    ghost mutable visited : seq 'a;
Mário Pereira's avatar
Mário Pereira committed
7 8
  }

9 10 11 12
  predicate permitted (cursor 'a)
  axiom permitted_empty: forall c: cursor 'a. c.visited = empty -> permitted c

  predicate complete  (cursor 'a)
Mário Pereira's avatar
Mário Pereira committed
13 14

  val next (c: cursor 'a) : 'a
15 16
    requires { not (complete c) }
    requires { permitted c }
Mário Pereira's avatar
Mário Pereira committed
17 18
    writes   { c.visited }
    ensures  { c.visited = snoc (old c).visited result }
19
    ensures  { permitted c }
Mário Pereira's avatar
Mário Pereira committed
20 21

  val has_next (c: cursor 'a) : bool
22 23
    requires { permitted c }
    ensures  { result <-> not (complete c) }
Mário Pereira's avatar
Mário Pereira committed
24 25

end
26

Mário Pereira's avatar
Mário Pereira committed
27
module ListCursor
28 29 30 31 32 33 34

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

  type cursor 'a = private {
Mário Pereira's avatar
Mário Pereira committed
35 36
    ghost mutable visited    : seq 'a;
    ghost         collection : list 'a;
37 38 39
  }

  predicate permitted (c: cursor 'a) =
Mário Pereira's avatar
Mário Pereira committed
40 41
    length c.visited <= length c.collection /\
    forall i. 0 <= i < length c.visited -> c.visited[i] = c.collection[i]
42 43

  predicate complete  (c: cursor 'a) =
Mário Pereira's avatar
Mário Pereira committed
44
    length c.visited = length c.collection
45 46 47 48

  val create (l: list 'a) : cursor 'a
    ensures { permitted result }
    ensures { result.visited = empty }
Mário Pereira's avatar
Mário Pereira committed
49
    ensures { result.collection = l }
50

Mário Pereira's avatar
Mário Pereira committed
51
  clone import Cursor as C with
52 53 54 55 56 57 58
    type cursor = cursor,
    predicate permitted = permitted,
    predicate complete  = complete,
    goal permitted_empty

end

59
module ArrayCursor
60 61

  use import array.Array
62
  use import array.ToSeq
63 64 65 66 67
  use import seq.Seq
  use import seq.OfList
  use import int.Int

  type cursor 'a = private {
68 69
    ghost mutable visited    : seq 'a;
    ghost         collection : seq 'a;
70 71 72
  }

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

  predicate complete  (c: cursor 'a) =
77
    length c.visited = length c.collection
78 79 80 81

  val create (a: array 'a) : cursor 'a
    ensures { permitted result }
    ensures { result.visited = empty }
82
    ensures { result.collection = to_seq a }
83

Mário Pereira's avatar
Mário Pereira committed
84
  clone import Cursor as C with
85 86 87 88 89 90
    type cursor = cursor,
    predicate permitted = permitted,
    predicate complete  = complete,
    goal permitted_empty

end