diff options
author | 2014-08-13 00:42:38 -0700 | |
---|---|---|
committer | 2014-08-13 00:42:38 -0700 | |
commit | 9f24fd54271e0e70aba494905416f58ff0348c7c (patch) | |
tree | 3d059a0abd1f71a4d99387e261ae2829e1bf2262 /Test/hofs/Compilation.dfy | |
parent | 7456be76add1e5d52001657df80d0e3cb00d5065 (diff) | |
parent | bc4e2c251a29902d7421f313aa3c55ba203d1608 (diff) |
Merge
Diffstat (limited to 'Test/hofs/Compilation.dfy')
-rw-r--r-- | Test/hofs/Compilation.dfy | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/Test/hofs/Compilation.dfy b/Test/hofs/Compilation.dfy new file mode 100644 index 00000000..c3132db2 --- /dev/null +++ b/Test/hofs/Compilation.dfy @@ -0,0 +1,48 @@ + +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"; +} + |