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
|
method {:tailrecursion} A(q: int) returns (x: int, ghost y: bool, z: nat)
{
if (q < 10) {
x, y, z := 15, true, 20;
} else {
ghost var u;
x, u, z := A(q-1);
y := !u;
}
}
method {:tailrecursion} B(q: int) returns (x: int, ghost y: bool, z: nat)
{
if (q < 10) {
x, y, z := 15, true, 20;
} else {
ghost var u;
x, u, z := B(q-1); // error: not a tail call, because it is followed by an increment to x
y, x := !u, x + 1;
}
}
method C(q: int) returns (x: int)
decreases *;
{
x := C(q-1);
}
method D(q: int) returns (x: int)
decreases *; // error: not allowed, because the method is not tail recursive
{
x := D(q-1);
x := x + 1;
}
method E0(q: int) returns (x: int)
decreases *; // error: not allowed, because the method is not tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)
{
x := E1(q-1);
}
method E1(q: int) returns (x: int)
decreases *; // error: not allowed, because the method is not tail recursive (since mutually recursive methods are currently not recognized as being tail recursive)
{
x := E0(q);
}
method F0(q: int) returns (x: int)
decreases *; // fine, but no 'decreases' spec is needed at all here
{
x := D(q);
}
method F1(q: int) returns (x: int)
decreases 5; // since this is okay (that is, you can--for no particular reason--add a 'decreases' clause to a non-recursive method), the 'decreases *' above is also allowed
{
x := D(q);
}
method {:tailrecursion} G0(q: int) returns (x: int)
decreases *;
{
x := D(q);
}
method {:tailrecursion false} G1(q: int) returns (x: int)
decreases *; // error: even though there is no recursion in this method's body, the annotation specifically says "not tail recursive", so (the easiest thing to do in the Resolver was to) generate an error
{
x := D(q);
}
method H0(q: int) returns (x: int)
decreases *; // fine, but no 'decreases' spec is needed at all here
method {:tailrecursion} H1(q: int) returns (x: int)
decreases *; // fine, but no 'decreases' spec is needed at all here
method H2(q: int) returns (x: int)
decreases 5; // fine, but no 'decreases' spec is needed at all here
class {:autocontracts} MyAutoContractClass {
var left: MyAutoContractClass;
predicate Valid() { true }
method {:tailrecursion} VisitLeft(val: int)
{
if left != null {
left.VisitLeft(val); // this is a tail call, because what :autocontracts appends is ghost
}
}
}
method {:tailrecursion} OtherTailCall(n: int) {
ghost var x := 12;
if n > 0 {
OtherTailCall(n-1); // tail call
}
x := 14;
{ x := 13; }
ghost var h := 15;
if n < h*30 { } // this is a ghost statement as well
if n < 230 { } // and this can be (and is) considered ghost as well
if (*) { x := x + 1; } // this, too
}
|
