From f3cfd7a9994af3518655bc4d1d77eeb3619b0999 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 28 Aug 2015 21:05:19 -0700 Subject: Implement workarounds for some tests that fail with /autoTriggers. The issues here are mostly with induction (wrt. to trigger selection and quantifier splitting) and with expressions like P(i, j-1) where no good choices are available. --- Test/dafny1/Induction.dfy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'Test/dafny1') diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 3445dab9..e2cd4ade 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -53,7 +53,7 @@ class IntegerInduction { } lemma DoItAllInOneGo() - ensures (forall n :: 0 <= n ==> + ensures (forall n {:split false} :: 0 <= n ==> // WISH reenable quantifier splitting here. This will only work once we generate induction hypotheses at the Dafny level. SumOfCubes(n) == Gauss(n) * Gauss(n) && 2 * Gauss(n) == n*(n+1)); { @@ -148,11 +148,11 @@ class IntegerInduction { // Proving the "<==" case is simple; it's the "==>" case that requires induction. // The example uses an attribute that requests induction on just "j". However, the proof also // goes through by applying induction on both bound variables. - function method IsSorted(s: seq): bool - ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]); + function method IsSorted(s: seq): bool //WISH remove autotriggers false + ensures IsSorted(s) ==> (forall i,j {:induction j} {:autotriggers false} :: 0 <= i < j < |s| ==> s[i] <= s[j]); ensures (forall i,j :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]) ==> IsSorted(s); { - (forall i :: 1 <= i && i < |s| ==> s[i-1] <= s[i]) + (forall i {:nowarn} :: 1 <= i && i < |s| ==> s[i-1] <= s[i]) } } -- cgit v1.2.3