diff options
| -rw-r--r-- | Test/VSComp2010/Problem2-Invert.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/Rippling.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny1/SchorrWaite.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny4/NipkowKlein-chapter7.dfy | 4 |
4 files changed, 10 insertions, 8 deletions
diff --git a/Test/VSComp2010/Problem2-Invert.dfy b/Test/VSComp2010/Problem2-Invert.dfy index 274d86de..0cf93061 100644 --- a/Test/VSComp2010/Problem2-Invert.dfy +++ b/Test/VSComp2010/Problem2-Invert.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %dafny /compile:0 /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// VSComp 2010, problem 2, compute the inverse 'B' of a permutation 'A' and prove that 'B' is
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 4d1761b1..d888a5cc 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -550,7 +550,7 @@ lemma P54() ensures forall m, n :: minus(add(m, n), n) == m;
{
// the proof of this theorem follows from two lemmas:
- assert forall m, n :: minus(add(n, m), n) == m;
+ assert forall m, n {:autotriggers false} :: minus(add(n, m), n) == m; // FIXME: Why does Autotriggers false make things verify?
assert forall m, n :: add(m, n) == add(n, m);
}
@@ -559,7 +559,7 @@ lemma P65() {
if (*) {
// the proof of this theorem follows from two lemmas:
- assert forall i, m :: less(i, Suc(add(i, m))) == True;
+ assert forall i, m {:autotriggers false} :: less(i, Suc(add(i, m))) == True; // FIXME: Why does Autotriggers false make things verify?
assert forall m, n :: add(m, n) == add(n, m);
} else {
// a different way to prove it uses the following lemma:
@@ -572,7 +572,7 @@ lemma P67() {
if (*) {
// the proof of this theorem follows from two lemmas:
- assert forall m, n :: leq(n, add(n, m)) == True;
+ assert forall m, n {:autotriggers false} :: leq(n, add(n, m)) == True; // FIXME: Why does Autotriggers false make things verify?
assert forall m, n :: add(m, n) == add(n, m);
} else {
// a different way to prove it uses the following lemma:
diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy index b29a6829..50210eb1 100644 --- a/Test/dafny1/SchorrWaite.dfy +++ b/Test/dafny1/SchorrWaite.dfy @@ -180,7 +180,7 @@ class Main { ensures forall n :: n in S && n.marked ==>
forall ch :: ch in n.children && ch != null ==> ch.marked
// every marked node was reachable from 'root' in the pre-state:
- ensures forall n :: n in S && n.marked ==> old(Reachable(root, n, S))
+ ensures forall n {:autotriggers false} :: n in S && n.marked ==> old(Reachable(root, n, S))
// the structure of the graph has not changed:
ensures forall n :: n in S ==>
n.childrenVisited == old(n.childrenVisited) &&
@@ -207,7 +207,7 @@ class Main { forall j :: 0 <= j < n.childrenVisited ==>
n.children[j] == null || n.children[j].marked
invariant forall n :: n in stackNodes ==> n.childrenVisited < |n.children|
- invariant forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
+ invariant forall n {:autotriggers false} :: n in S && n.marked && n !in stackNodes && n != t ==>
forall ch :: ch in n.children && ch != null ==> ch.marked
invariant forall n :: n in S && n !in stackNodes && n != t ==>
n.childrenVisited == old(n.childrenVisited)
@@ -219,7 +219,7 @@ class Main { // every marked node is reachable:
invariant !fresh(path); // needed to show 'path' worthy as argument to old(Reachable(...))
invariant old(ReachableVia(root, path, t, S));
- invariant forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> !fresh(pth)
+ invariant forall n, pth {:nowarn} :: n in S && n.marked && pth == n.pathFromRoot ==> !fresh(pth)
invariant forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>
old(ReachableVia(root, pth, n, S))
invariant forall n :: n in S && n.marked ==> old(Reachable(root, n, S))
diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy b/Test/dafny4/NipkowKlein-chapter7.dfy index e694fc4b..aae94550 100644 --- a/Test/dafny4/NipkowKlein-chapter7.dfy +++ b/Test/dafny4/NipkowKlein-chapter7.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /rprint:"%t.rprint" /autoTriggers:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This file is a Dafny encoding of chapter 7 from "Concrete Semantics: With Isabelle/HOL" by
@@ -360,3 +360,5 @@ lemma lemma_7_18(c: com, s: state) BigStep_SmallStepStar_Same(c, s, s');
}
}
+
+// Autotriggers:0 added as this file relies on proving a property of the form body(f) == f
|