summaryrefslogtreecommitdiff
path: root/Test/dafny3/SetIterations.dfy
blob: 8b095b5fe58b5ca142c162ebf94ef76146faa428 (plain)
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
function Count<T>(s: set<T>): int
{
  if s == {} then 0 else
    var x :| x in s;  // let x be such that "x in s"
    1 + Count(s - {x})
}

method Copy<T>(s: set<T>) returns (t: set<T>)
  ensures s == t;
{
  t := {};
  var r := s;
  while (r != {})
    invariant s == r + t;
    decreases r;
  {
    var x :| x in r;
    r, t := r - {x}, t + {x};
  }
}

method CopyFaster<T>(s: set<T>) returns (t: set<T>)
  ensures s == t;
{
  t := {};
  var r := s;
  while (r != {})
    invariant s == r + t;
    decreases r;
  {
    var p :| p != {} && p <= r;  // pick a nonempty subset of r
    r, t := r - p, t + p;
  }
}

method CopyFastest<T>(s: set<T>) returns (t: set<T>)
  ensures s == t;
{
  t := s;  // :)
}

iterator Iter<T>(s: set<T>) yields (x: T)
  yield ensures x in s && x !in xs[..|xs|-1];
  ensures s == set z | z in xs;
{
  var r := s;
  while (r != {})
    invariant forall z :: z in xs ==> x !in r;  // r and xs are disjoint
    invariant s == r + set z | z in xs;
  {
    var y :| y in r;
    r, x := r - {y}, y;
    yield;
    assert y == xs[|xs|-1];  // needed as a lemma to prove loop invariant
  }
}

method UseIterToCopy<T>(s: set<T>) returns (t: set<T>)
  ensures s == t;
{
  t := {};
  var m := new Iter(s);
  while (true)
    invariant m.Valid() && fresh(m._new);
    invariant t == set z | z in m.xs;
    decreases s - t;
  {
    var more := m.MoveNext();
    if (!more) { break; }
    t := t + {m.x};
  }
}