diff options
author | Dan Rosén <danr@chalmers.se> | 2014-08-12 14:44:55 -0700 |
---|---|---|
committer | Dan Rosén <danr@chalmers.se> | 2014-08-12 14:44:55 -0700 |
commit | e2d1b7891526c90e26a790a9783aed8f69a57450 (patch) | |
tree | 986d95d64662104c8eac9a5321ea7e99faedc665 /Test/hofs/Compilation.dfy | |
parent | 8797f054f44d114147562689d80c9970d8ea4f82 (diff) |
Compile lambda functions and apply expressions, and change let expr compilation
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"; +} + |