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
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
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)
{
x := D(q-1);
x := x + 1;
}
method {:tailrecursion} E0(q: int) returns (x: int) // 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 {:tailrecursion} E1(q: int) returns (x: int) // 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
{
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) // the annotation tells the compiler not to tail-call optimize
decreases *;
{
x := G1(q);
}
method H0(q: int) returns (x: int)
decreases *; // fine
method {:tailrecursion} H1(q: int) returns (x: int)
decreases *; // fine
method H2(q: int) returns (x: int)
decreases 5; // fine
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
}
|
