why3/stdlib/cursor.mlw at master · EasyCrypt/why3 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
(** {1 Cursors} *)

module Cursor

  use seq.Seq

  type cursor 'a = private {
    ghost mutable visited : seq 'a;
  }

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

  predicate complete  (cursor 'a)

  val next (c: cursor 'a) : 'a
    requires { not (complete c) }
    requires { permitted c }
    writes   { c.visited }
    ensures  { c.visited = snoc (old c).visited result }
    ensures  { permitted c }

  val has_next (c: cursor 'a) : bool
    requires { permitted c }
    ensures  { result <-> not (complete c) }

end

module ListCursor

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

  type cursor 'a = private {
    ghost mutable visited    : seq 'a;
    ghost         collection : list 'a;
  }

  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

  val create (l: list 'a) : cursor 'a
    ensures { permitted result }
    ensures { result.visited = empty }
    ensures { result.collection = l }

  clone Cursor as C with
    type cursor = cursor,
    predicate permitted = permitted,
    predicate complete  = complete,
    goal permitted_empty

end

module ArrayCursor

  use array.Array
  use array.ToSeq
  use seq.Seq
  use seq.OfList
  use int.Int

  type cursor 'a = private {
    ghost mutable visited    : seq 'a;
    ghost         collection : seq 'a;
  }

  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

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

  clone Cursor as C with
    type cursor = cursor,
    predicate permitted = permitted,
    predicate complete  = complete,
    goal permitted_empty

end