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
|
// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
method Main() {
var c := new MyClass;
c.arr := new int[10,20];
c.K0(3, 12);
c.K1(3, 12);
c.K2(3, 12);
c.K3(3, 12);
c.K4(12);
c.M();
c.N();
c.P();
c.Q();
}
class MyClass
{
var arr: array2<int>;
method K0(i: int, j: int)
requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;
modifies arr;
{
forall k | k in {-3, 4} {
arr[i,j] := 50;
}
}
method K1(i: int, j: int)
requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;
// note the absence of a modifies clause
{
forall k: int | k in {} {
arr[i,j] := k; // fine, since control will never reach here
}
}
method K2(i: int, j: int)
requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;
modifies arr;
{
forall k: int | k in {-3, 4} {
// The following would have been an error (since this test file tests
// compilation, we don't include the test here):
// arr[i,j] := k; // error: k can take on more than one value
}
}
method K3(i: int, j: int)
requires arr != null && 0 <= i < arr.Length0 && 0 <= j < arr.Length1;
modifies arr;
{
forall k: nat | k in {-3, 4} && k <= i {
arr[k,j] := 50; // fine, since k:nat is at least 0
}
}
method K4(j: int)
requires arr != null && 0 <= j < arr.Length1;
modifies arr;
{
forall i, k: nat | 0 <= i < arr.Length0 && k in {-3, 4} {
arr[i,j] := k; // fine, since k can only take on one value
}
}
method M()
{
var ar := new int [3,3];
var S: set<int> := {2,0};
forall k | k in S {
ar[k,1]:= 0;
}
forall k, j | k in S && j in S {
ar[k,j]:= 0;
}
}
method N() {
var ar := new int[3, 3];
ar[2,2] := 0;
}
method P() {
var ar := new int[3];
var prev := ar[..];
var S: set<int> := {};
forall k | k in S {
ar[k] := 0;
}
assert ar[..] == prev;
}
method Q() {
var ar := new int[3,3];
var S: set<int> := {1,2};
forall k | k in S {
ar[0,0] := 0;
}
assert ar[0,0] == 0;
}
}
|
