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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This method can be used to test compilation.
ghost method M()
{
ghost var im := imap[2:=3];
// test "in"
if(2 in im)
{
}
else
{ assert false; }
// test "!in"
if(3 !in im)
{
}
else
{ assert false; }
// dereference
if(im[2] == 3)
{
}
else
{ assert false; }
// test applicative nature of Map<U, V> in C#
if(im == imap[2 := 3])
{
}
else
{ assert false; }
}
lemma m()
{
ghost var a := imap i | i == 2 :: 3; var b := imap i | i == 3 :: 2;
assert a[b[3]] == 3;
}
lemma m2(a: imap<int, bool>, b: imap<int, bool>)
requires forall i | 0 <= i < 100 :: i in a && i in b && a[i] != b[i];
{
assert forall i | 0 <= i < 100 :: a[i] || b[i];
}
lemma m3(a: imap<int, int>)
requires forall i | 0 <= i < 100 :: i in a && a[i] == i*i;
{
assert a[20] == 400;
}
lemma m4()
{
ghost var a := imap i | i == 3 :: 9;
if(a[4] == 4) // UNSAFE, 4 not in the domain
{
m();
}
}
lemma m5(a: imap<int, int>)
requires 20 in a;
{
assert a[20] <= 0 || 0 < a[20];
}
lemma m7()
{
var a := imap[1:=1, 2:=4, 3:=9];
assert forall i | i in a :: a[i] == i * i;
assert 0 !in a;
assert 1 in a;
assert 2 in a;
assert 3 in a;
assert forall i | i < 1 || i > 3 :: i !in a;
}
function Update<K, V>(a:imap<K, V>, k:K, v:V):imap<K, V>
{
imap j | (j == k || j in a) :: (if j == k then v else a[j])
}
method m8()
{
ghost var a: imap<int,int> := imap i | false :: 0;
assert forall i :: i !in a; // check emptiness
var i,n := 0, 100;
while(i < n)
invariant 0 <= i <= n;
invariant forall i | i in a :: a[i] == i * i;
invariant forall k :: 0 <= k < i <==> k in a;
{
a := Update(a, i, i * i);
i := i + 1;
}
m3(a);
}
lemma m12()
{
ghost var x := imap i | 0 <= i < 10 :: i * 2;
assert 0 in x;
assert 1 in x;
assert 10 !in x;
assert x[0] == 0 && x[2] == 4;
}
/*
function domain<U, V>(m: imap<U,V>): set<U>
ensures forall i :: i in domain(m) <==> i in m;
{
set s | s in m // UNSAFE, m may have infinite domain
}
*/
method m13()
{
var s := {0, 1, 3, 4};
ghost var x := imap i | i in s :: i;
assert forall i | i in x :: x[i] == i;
// assert domain(x) == s;
}
class A { var x: int; }
method m15(b: set<A>)
requires forall a | a in b :: a != null;
{
ghost var m := imap a | a in b :: a.x;
var aa := new A;
assert aa !in m;
}
method minf()
{
ghost var m := imap i | i > 100 :: 2 * i;
assert 101 in m;
assert 99 !in m;
assert m[101] == 202;
assert forall i :: i > 200 ==> m[i] == 2 * i;
}
|
