blob: 2319078a979f5cc0481f0830a2b17c3b575b9969 (
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
73
74
75
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
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};
}
}
|
