Merge

7 files changed, 35 insertions, 33 deletions

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index 0940d9e7..374555b0 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -3,7 +3,7 @@
 

 method FindZero(a: array<int>) returns (r: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

-  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

   ensures 0 <= r ==> r < a.Length && a[r] == 0;

   ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;

 {

@@ -20,7 +20,7 @@ method FindZero(a: array<int>) returns (r: int)
 

 lemma Lemma(a: array<int>, k: int, m: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

-  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

   requires 0 <= k;

   requires k < a.Length ==> m <= a[k];

   ensures forall i :: k <= i < k+m && i < a.Length ==> a[i] != 0;

@@ -36,7 +36,7 @@ lemma Lemma(a: array<int>, k: int, m: int)
 

 method FindZero_GhostLoop(a: array<int>) returns (r: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

-  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  requires forall i {:nowarn} :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

   ensures 0 <= r ==> r < a.Length && a[r] == 0;

   ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;

 {

@@ -63,7 +63,7 @@ method FindZero_GhostLoop(a: array<int>) returns (r: int)
 

 method FindZero_Assert(a: array<int>) returns (r: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

-  requires forall i :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];

+  requires forall i {:nowarn} :: 0 <= i-1 && i < a.Length ==> a[i-1]-1 <= a[i];

   ensures 0 <= r ==> r < a.Length && a[r] == 0;

   ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != 0;

 {

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<int>): bool

-    ensures IsSorted(s) ==> (forall i,j {:induction j} :: 0 <= i && i < j && j < |s| ==> s[i] <= s[j]);

+  function method IsSorted(s: seq<int>): 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/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index 319bb8d0..bd654db5 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -83,12 +83,12 @@ lemma LemmaOne(n: int)
 {

 }

 

-lemma LemmaAll_Neg()

-  ensures forall n :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

+lemma LemmaAll_Neg() //FIXME I don't understand the comment below; what trigger?

+  ensures forall n {:nowarn} :: NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

 {

 }

 

-lemma LemmaOne_Neg(n: int)

+lemma LemmaOne_Neg(n: int) //FIXME What trigger?

   ensures NegFac(-n) <= -1;  // error: fails to verify because of the minus in the trigger

 {

 }

diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect
index 5de0ace6..7da5e2ec 100644
--- a/Test/dafny1/MoreInduction.dfy.expect
+++ b/Test/dafny1/MoreInduction.dfy.expect
@@ -1,5 +1,6 @@
 MoreInduction.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.

 MoreInduction.dfy(77,10): Related location: This is the postcondition that might not hold.

+MoreInduction.dfy(77,32): Related location

 Execution trace:

     (0,0): anon0

 MoreInduction.dfy(83,0): Error BP5003: A postcondition might not hold on this return path.

@@ -8,6 +9,7 @@ Execution trace:
     (0,0): anon0

 MoreInduction.dfy(88,0): Error BP5003: A postcondition might not hold on this return path.

 MoreInduction.dfy(87,10): Related location: This is the postcondition that might not hold.

+MoreInduction.dfy(87,43): Related location

 Execution trace:

     (0,0): anon0

 MoreInduction.dfy(93,0): Error BP5003: A postcondition might not hold on this return path.

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 94223cba..3d2a5d78 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -12,7 +12,7 @@ class PriorityQueue {
     reads this, Repr;

   {

     MostlyValid() &&

-    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])

+    (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])

   }

 

   predicate MostlyValid()

@@ -50,8 +50,8 @@ class PriorityQueue {
   method SiftUp(k: int)

     requires 1 <= k && k <= n;

     requires MostlyValid();

-    requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);

-    requires (forall j :: 1 <= j && j <= n ==> j/2 != k);  // k is a leaf

+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);

+    requires (forall j {:nowarn} :: 1 <= j && j <= n ==> j/2 != k);  // k is a leaf

     modifies a;

     ensures Valid();

   {

@@ -59,8 +59,8 @@ class PriorityQueue {
     assert MostlyValid();

     while (1 < i)

       invariant i <= k && MostlyValid();

-      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       if (a[i/2] <= a[i]) {

         return;

@@ -85,8 +85,8 @@ class PriorityQueue {
   method SiftDown(k: int)

     requires 1 <= k;

     requires MostlyValid();

-    requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);

-    requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);

+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);

+    requires (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);

     // Alternatively, the line above can be expressed as:

     //     requires (forall j :: 1 <= k/2 && j/2 == k && j <= n ==> a[j/2/2] <= a[j]);

     modifies a;

@@ -95,8 +95,8 @@ class PriorityQueue {
     var i := k;

     while (2*i <= n)  // while i is not a leaf

       invariant 1 <= i && MostlyValid();

-      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);

     {

       var smallestChild;

       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {

@@ -127,7 +127,7 @@ class PriorityQueue_Alternative {
     reads this, Repr;

   {

     MostlyValid() &&

-    (forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])

+    (forall j {:nowarn} :: 2 <= j && j <= n ==> a[j/2] <= a[j])

   }

 

   predicate MostlyValid()

@@ -164,7 +164,7 @@ class PriorityQueue_Alternative {
 

   method SiftUp()

     requires MostlyValid();

-    requires (forall j :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);

+    requires (forall j {:nowarn} :: 2 <= j && j <= n && j != n ==> a[j/2] <= a[j]);

     modifies a;

     ensures Valid();

   {

@@ -172,8 +172,8 @@ class PriorityQueue_Alternative {
     assert MostlyValid();

     while (1 < i)

       invariant i <= n && MostlyValid();

-      invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       if (a[i/2] <= a[i]) {

         return;

@@ -197,15 +197,15 @@ class PriorityQueue_Alternative {
 

   method SiftDown()

     requires MostlyValid();

-    requires (forall j :: 4 <= j && j <= n ==> a[j/2] <= a[j]);

+    requires (forall j {:nowarn} :: 4 <= j && j <= n ==> a[j/2] <= a[j]);

     modifies a;

     ensures Valid();

   {

     var i := 1;

     while (2*i <= n)  // while i is not a leaf

       invariant 1 <= i && MostlyValid();

-      invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

-      invariant (forall j :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);

+      invariant (forall j {:nowarn} :: 1 <= j/2/2 && j/2 == i && j <= n ==> a[j/2/2] <= a[j]);

     {

       var smallestChild;

       if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {

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))