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
|
// RUN: %dafny /compile:3 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class Ref<A> {
var val : A;
}
method Main() {
// simple
print "1 = ", (x => x)(1), "\n";
print "3 = ", (x => y => x + y)(1)(2), "\n";
print "3 = ", ((x,y) => y + x)(1,2), "\n";
print "0 = ", (() => 0)(), "\n";
// local variable
var y := 1;
var f := x => x + y;
print "3 = ", f(2), "\n";
print "4 = ", f(3), "\n";
y := 2;
print "3 = ", f(2), "\n";
print "4 = ", f(3), "\n";
// reference
var z := new Ref<int>;
z.val := 1;
f := x reads z requires z != null => x + z.val;
print "3 = ", f(2), "\n";
print "4 = ", f(3), "\n";
z.val := 2;
print "4 = ", f(2), "\n";
print "5 = ", f(3), "\n";
// loop
f := x => x;
y := 10;
while (y > 0)
invariant forall x :: f.requires(x);
invariant forall x :: f.reads(x) == {};
{
f := x => f(x+y);
y := y - 1;
}
print "55 = ", f(0), "\n";
// substitution test
print "0 = ", (x => var y:=x;y)(0), "\n";
print "1 = ", (y => (x => var y:=x;y))(0)(1), "\n";
}
|
