diff options
| author |  Rustan Leino <unknown> | 2016-03-01 16:24:26 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2016-03-01 16:24:26 -0800 |
| commit | f48f5e1cef6482557d3f90677c5e41b75b2092b4 (patch) | |
| tree | 0e21f7f7443b799c87c9295bbbd2bb8be3352ec4 | |
| parent | 2144154dc66b8d83792dd4395d3059c97d044e01 (diff) | |
Added test case to go with the recent fix of Issue #49 (changeset f354709009a5).
| -rw-r--r-- | Test/dafny4/Bug49.dfy | 74 | ||||
| -rw-r--r-- | Test/dafny4/Bug49.dfy.expect | 8 |
2 files changed, 82 insertions, 0 deletions
diff --git a/Test/dafny4/Bug49.dfy b/Test/dafny4/Bug49.dfy new file mode 100644 index 00000000..887938d6 --- /dev/null +++ b/Test/dafny4/Bug49.dfy @@ -0,0 +1,74 @@ +// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main()
+{
+ print apply(i => i + 1, 5), "\n";
+ print mapply(map[5 := 6], 5), "\n";
+ var f;
+ print five(f), "\n";
+}
+
+// -----
+// test that the definition axiom for function "apply" is available
+
+function method apply(f:int->int, a:int): int
+ reads f.reads
+ requires f.requires(a)
+{
+ f(a)
+}
+
+lemma TestPost()
+ ensures apply(i => i + 1, 5) == 6
+{
+}
+
+lemma M() {
+ assert apply(i => i + 1, 5) == 6;
+}
+
+lemma TestPre()
+ requires apply(i => i + 1, 5) == 6
+{
+}
+
+lemma TestPreCaller()
+{
+ TestPre();
+}
+
+// -----
+// test that the above thing for arrows also works for maps
+
+function method mapply(m: map<int,int>, a:int): int
+ requires a in m
+{
+ m[a]
+}
+
+lemma TestMPost()
+ ensures mapply(map[5 := 6], 5) == 6
+{
+}
+
+lemma N() {
+ assert mapply(map[5 := 6], 5) == 6;
+}
+
+// -----
+// test that g's result is known to be $Is'ed and $IsAlloc'ed
+
+function method five(f:int->int): int { 5 }
+
+lemma P() {
+ var f := i => i + 1;
+ assert five(f) == 5;
+}
+
+lemma Q(g: real->int->int)
+ requires g.requires(0.0)
+{
+ var f := g(0.0);
+ assert five(f) == 5;
+}
diff --git a/Test/dafny4/Bug49.dfy.expect b/Test/dafny4/Bug49.dfy.expect new file mode 100644 index 00000000..653dda07 --- /dev/null +++ b/Test/dafny4/Bug49.dfy.expect @@ -0,0 +1,8 @@ +
+Dafny program verifier finished with 21 verified, 0 errors
+Program compiled successfully
+Running...
+
+6 +6 +5 |