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
|
// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" > "%t"
// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:js "%s" >> "%t"
// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:go "%s" >> "%t"
// RUN: %diff "%s.expect" "%t"
class C {
var x: int
// for variety, the following tests the use of an instance Main method
method Main(ghost u: int) returns (ghost r: bool, ghost s: bool) {
print "hello, instance\n";
print "x is ", x, "\n";
Client();
}
}
iterator Iter<X(==)>(a: array<X>, stop: X) yields (x: X)
yield ensures |xs| <= a.Length
ensures |xs| <= a.Length
{
var i := 0;
while i < a.Length
invariant |xs| == i <= a.Length
{
if i % 2 == 0 {
yield a[i];
}
x := a[i];
if x == stop {
break;
}
if i % 2 == 1 {
yield;
}
i := i + 1;
}
}
method Client()
{
var a := new real[6](i => i as real);
var iter := new Iter(a, 2.4);
while true
invariant iter.Valid() && fresh(iter._new)
decreases a.Length - |iter.xs|
{
var more := iter.MoveNext();
if (!more) { break; }
print iter.x, " ";
}
print "\n";
iter := new Iter(a, 2.0);
while true
invariant iter.Valid() && fresh(iter._new)
decreases a.Length - |iter.xs|
{
var more := iter.MoveNext();
if (!more) { break; }
print iter.x, " ";
}
print "\n";
}
|
