From 2b2050060b9eb8cb123af6df942ebebe7fe6d52c Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 24 Jul 2015 21:12:30 -0700 Subject: Renamed "ghost method" to "lemma" in a couple of test files --- Test/dafny1/Induction.dfy | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'Test/dafny1/Induction.dfy') diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 28171896..3445dab9 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -22,7 +22,7 @@ class IntegerInduction { // Here is one proof. It uses a lemma, which is proved separately. - ghost method Theorem0(n: int) + lemma Theorem0(n: int) requires 0 <= n; ensures SumOfCubes(n) == Gauss(n) * Gauss(n); { @@ -32,7 +32,7 @@ class IntegerInduction { } } - ghost method Lemma(n: int) + lemma Lemma(n: int) requires 0 <= n; ensures 2 * Gauss(n) == n*(n+1); { @@ -42,7 +42,7 @@ class IntegerInduction { // Here is another proof. It states the lemma as part of the theorem, and // thus proves the two together. - ghost method Theorem1(n: int) + lemma Theorem1(n: int) requires 0 <= n; ensures SumOfCubes(n) == Gauss(n) * Gauss(n); ensures 2 * Gauss(n) == n*(n+1); @@ -52,24 +52,24 @@ class IntegerInduction { } } - ghost method DoItAllInOneGo() + lemma DoItAllInOneGo() ensures (forall n :: 0 <= n ==> SumOfCubes(n) == Gauss(n) * Gauss(n) && 2 * Gauss(n) == n*(n+1)); { } - // The following two ghost methods are the same as the previous two, but + // The following two lemmas are the same as the previous two, but // here no body is given--and the proof still goes through (thanks to // Dafny's ghost-method induction tactic). - ghost method Lemma_Auto(n: int) + lemma Lemma_Auto(n: int) requires 0 <= n; ensures 2 * Gauss(n) == n*(n+1); { } - ghost method Theorem1_Auto(n: int) + lemma Theorem1_Auto(n: int) requires 0 <= n; ensures SumOfCubes(n) == Gauss(n) * Gauss(n); ensures 2 * Gauss(n) == n*(n+1); @@ -79,7 +79,7 @@ class IntegerInduction { // Here is another proof. It makes use of Dafny's induction heuristics to // prove the lemma. - ghost method Theorem2(n: int) + lemma Theorem2(n: int) requires 0 <= n; ensures SumOfCubes(n) == Gauss(n) * Gauss(n); { @@ -90,7 +90,7 @@ class IntegerInduction { } } - ghost method M(n: int) + lemma M(n: int) requires 0 <= n; { assume (forall k :: 0 <= k && k < n ==> 2 * Gauss(k) == k*(k+1)); // manually assume the induction hypothesis @@ -99,7 +99,7 @@ class IntegerInduction { // Another way to prove the lemma is to supply a postcondition on the Gauss function - ghost method Theorem3(n: int) + lemma Theorem3(n: int) requires 0 <= n; ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n); { @@ -117,14 +117,14 @@ class IntegerInduction { // Finally, with the postcondition of GaussWithPost, one can prove the entire theorem by induction - ghost method Theorem4() + lemma Theorem4() ensures (forall n :: 0 <= n ==> SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n)); { // look ma, no hints! } - ghost method Theorem5(n: int) + lemma Theorem5(n: int) requires 0 <= n; ensures SumOfCubes(n) == GaussWithPost(n) * GaussWithPost(n); { -- cgit v1.2.3 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/VerifyThis2015/Problem2.dfy | 2 +- Test/dafny0/Array.dfy | 4 +++- Test/dafny0/ComputationsNeg.dfy | 2 +- Test/dafny0/MultiSets.dfy | 5 ++++- Test/dafny1/Induction.dfy | 8 ++++---- Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy | 4 ++-- Test/dafny3/InductionVsCoinduction.dfy | 2 +- 7 files changed, 16 insertions(+), 11 deletions(-) (limited to 'Test/dafny1/Induction.dfy') diff --git a/Test/VerifyThis2015/Problem2.dfy b/Test/VerifyThis2015/Problem2.dfy index 1c7deffd..86b4a019 100644 --- a/Test/VerifyThis2015/Problem2.dfy +++ b/Test/VerifyThis2015/Problem2.dfy @@ -315,7 +315,7 @@ lemma GcdDecrease(a: int, b: int) ensures Gcd(a, b) == Gcd(a - b, b) { var k := Gcd(a - b, b); - assert DividesBoth(k, a-b, b) && forall m :: DividesBoth(m, a-b, b) ==> m <= k; + assert DividesBoth(k, a-b, b) && forall m, mm :: mm == a - b ==> DividesBoth(m, mm, b) ==> m <= k; // WISH: auto-generate 'mm' var n := DividesProperty(k, a-b); assert n*k == a-b; var p := DividesProperty(k, b); diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 391ca5f7..309e9248 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" class A { @@ -327,3 +327,5 @@ module DtypeRegression { } } } + +// WISH: autoTriggers disabled because of induction diff --git a/Test/dafny0/ComputationsNeg.dfy b/Test/dafny0/ComputationsNeg.dfy index 0c539117..b9425d64 100644 --- a/Test/dafny0/ComputationsNeg.dfy +++ b/Test/dafny0/ComputationsNeg.dfy @@ -16,7 +16,7 @@ predicate ThProperty(step: nat, t: Nat, r: nat) { match t case Zero => true - case Succ(o) => step>0 && exists ro:nat :: ThProperty(step-1, o, ro) + case Succ(o) => step>0 && exists ro:nat, ss :: ss == step-1 ==> ThProperty(ss, o, ro) // WISH: auto-generate ss } ghost method test_ThProperty() ensures ThProperty(10, Succ(Zero), 0); diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index 3535f857..ba075fc3 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" method test1() @@ -295,3 +295,6 @@ lemma Set_and_Multiset_Cardinalities(x: int, y: int) assert |multiset{x,y}| == 2; } } + +// AutoTriggers explicitly removed, as simplifications of set expressions such +// as x in {1,2} cause invalid terms to appear in the triggers 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]) } } diff --git a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy index 72a22cfd..4c702674 100644 --- a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy +++ b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy @@ -93,8 +93,8 @@ method Search(a: array) returns (p: int, q: int) invariant forall j :: 0 <= j < d.Length ==> (d[j] == -1 && forall k :: 0 <= k < i ==> a[k] != j) || (0 <= d[j] < i && a[d[j]] == j); - invariant p == q ==> IsDuplicate(a, p); - invariant forall k :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k]; + invariant p == q ==> IsDuplicate(a, p); //WISH remove the trigger on the next line + invariant forall k {:trigger old(a[k])} :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k]; decreases a.Length - i; { var k := d[a[i]]; diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy index 89fa6cc8..0074b742 100644 --- a/Test/dafny3/InductionVsCoinduction.dfy +++ b/Test/dafny3/InductionVsCoinduction.dfy @@ -80,7 +80,7 @@ lemma SAppendIsAssociative(a:Stream, b:Stream, c:Stream) { forall k:nat { SAppendIsAssociativeK(k, a, b, c); } // assert for clarity only, postcondition follows directly from it - assert (forall k:nat :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c))); + assert (forall k:nat {:autotriggers false} :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c))); //FIXME: Should Dafny generate a trigger here? If so then which one? } // Equivalent proof using the colemma syntax. -- cgit v1.2.3