summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-10-19 18:35:52 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-10-19 18:35:52 -0700
commit253ace40ff7f3382f1f413020069fcaae7a966e0 (patch)
treed969df8ac8f3bdca2b66a7e8d5fc18eb27d26a65 /Test
parent2cf94d77a65e9e585baee7d43a8424227d3fe773 (diff)
Dafny: fixed performance-buggy translation of exists, and also added some other features in SplitExpr (such as induction on existential quantifiers)
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy8
1 files changed, 1 insertions, 7 deletions
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
index d846269d..774008b8 100644
--- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -231,12 +231,7 @@ class Node {
requires 0 <= a && 1 <= b;
requires forall k,l :: 0 <= k < l < a ==> Nexxxt(k, S) != Nexxxt(l, S);
requires Nexxxt(a, S) == null || Nexxxt(a, S).Nexxxt(b, S) == Nexxxt(a, S);
- // The next line most straightforwardly expresses the postcondition of this method:
- // ensures exists T :: 0 <= T <= a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
- // However, Dafny does an unfortunate (I would say performance-buggy) translation of existential
- // quantifiers, which the alternative formulation of "exists x :: P(x)" as
- // "(forall x :: !P(x)) ==> false" works around. This translation issue should be fixed.
- ensures (forall T :: !(0 <= T <= a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S))) ==> false;
+ ensures exists T :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
{
if (Nexxxt(a, S) == null) {
Lemma_NullIsTerminal(1+2*a, S);
@@ -276,7 +271,6 @@ class Node {
i, t, vt, h := i+1, t+1, vt+1, h+2;
}
assert a <= t < a + b && Nexxxt(t, S) == Nexxxt(1 + 2*t, S);
- assert exists T :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);
}
}