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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
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.
}
iterator yieldTesting() yields (a: int, b: int)
yield ensures a == 1 && b == 2;
{
a, b := 2, 1; // these are wrong
if (true)
{
var a, b := 3, 4;
yield 1, 2;// return updates non-shadowed, formal parameters correctly
}
}
|
