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
|
class N
{
var i: int;
method newN(n: N)
requires n != null;
modifies this, n;
{
n.i := 1;
i := 1;
}
method safe(n: N)
requires n != null;
modifies this;
{
i := n.i;
}
}
method m(v: int, n: N) returns (r: int)
modifies n;
ensures r == v;
{
r := v; // implict return still works.
}
method testing1() returns (a: int, b: set<int>)
{
return 1, {1, 2, 3}; // type checking
}
method testing2() returns (a: int, b: int)
ensures a == 1 && b == 2;
{
a, b := 2, 1;
return b, a; // test of parallel assignment.
}
method testing3() returns (a: int, b: int)
ensures a == 1 && b == 2;
{
a, b := 2, 1; // these are wrong
if (true)
{
var a, b := 3, 4;
return 1, 2;// return updates non-shadowed, formal parameters correctly
}
}
method testing4(nnn: N) returns (n: N)
requires nnn != null;
{
return new N.safe(nnn); // only modifies 'this', which is the fresh N
}
method testing5() returns (r: int)
ensures r == 2;
{
r := 2;
return; // sanity check.
}
|