New logical encoding of types with Is and IsAlloc

3 files changed, 21 insertions, 12 deletions

diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
index 56f689da..ee56e14a 100644
--- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -208,6 +208,14 @@ class Node {
       decreases S - Visited;

     {

       p, steps, Visited := p.next, steps + 1, Visited + {p};

+

+      // with all: 3s

+      // without this: 20s

+      assert forall t :: 0 <= t < steps ==> Nexxxt(t, S) in Visited;

+      // without this: 5s

+      assert forall q :: q in (Visited - {null}) ==> exists t :: 0 <= t < steps && Nexxxt(t, S) == q;

+      // without this: >60s

+      assert forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S);

     }

     if (p == null) {

       A, B := steps, 1;

diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index 10004332..4b8c9b4c 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -41,13 +41,13 @@ function qreverse(l: List): List
 

 // Here are two lemmas about the List functions.

 

-ghost method Lemma_ConcatNil()

-  ensures forall xs :: concat(xs, Nil) == xs;

+ghost method Lemma_ConcatNil(xs : List)

+  ensures concat(xs, Nil) == xs;

 {

 }

 

-ghost method Lemma_RevCatCommute()

-  ensures forall xs, ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);

+ghost method Lemma_RevCatCommute(xs : List)

+  ensures forall ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);

 {

 }

 

@@ -64,7 +64,7 @@ ghost method Theorem_QReverseIsCorrect_Calc(l: List)
     revacc(l, Nil);

     { Lemma_Revacc_calc(l, Nil); }

     concat(reverse(l), Nil);

-    { Lemma_ConcatNil(); }

+    { Lemma_ConcatNil(reverse(l)); }

     reverse(l);

   }

 }

@@ -81,7 +81,7 @@ ghost method Lemma_Revacc_calc(xs: List, ys: List)
         concat(concat(reverse(xrest), Cons(x, Nil)), ys);

         // induction hypothesis: Lemma_Revacc_calc(xrest, Cons(x, Nil))

         concat(revacc(xrest, Cons(x, Nil)), ys);

-        { Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)

+        { Lemma_RevCatCommute(xrest); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)

         revacc(xrest, concat(Cons(x, Nil), ys));

         // def. concat (x2)

         revacc(xrest, Cons(x, ys));

@@ -102,7 +102,7 @@ ghost method Theorem_QReverseIsCorrect(l: List)
   Lemma_Revacc(l, Nil);

   assert revacc(l, Nil)

       == concat(reverse(l), Nil);

-  Lemma_ConcatNil();

+  Lemma_ConcatNil(reverse(l));

 }

 

 ghost method Lemma_Revacc(xs: List, ys: List)

@@ -120,7 +120,7 @@ ghost method Lemma_Revacc(xs: List, ys: List)
               concat(concat(reverse(xrest), Cons(x, Nil)), ys)

           == // induction hypothesis:  Lemma_Revacc(xrest, Cons(x, Nil))

               concat(revacc(xrest, Cons(x, Nil)), ys);

-          Lemma_RevCatCommute();  // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)

+          Lemma_RevCatCommute(xrest);  // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)

       assert concat(revacc(xrest, Cons(x, Nil)), ys)

           == revacc(xrest, concat(Cons(x, Nil), ys));

 

@@ -181,7 +181,7 @@ ghost method Lemma_Reverse_Length(xs: List)
         calc {

           length(Cons(x, Nil));

           // def. length

-          1 + length(Nil);

+          // 1 + length(Nil);  // ambigious type parameter

           // def. length

           1 + 0;

           1;

@@ -231,7 +231,7 @@ ghost method lemma_extensionality(xs: List, ys: List)
   ensures xs == ys;

 {

   match xs {

-    case Nil => 

+    case Nil =>

       calc {

         true;

         // (0)

@@ -255,7 +255,7 @@ ghost method lemma_extensionality(xs: List, ys: List)
               y;

             }

             Cons(y, xrest);

-            { 

+            {

               forall (j: nat | j < length(xrest)) {

                 calc {

                   ith(xrest, j);

@@ -265,7 +265,7 @@ ghost method lemma_extensionality(xs: List, ys: List)
                   ith(yrest, j);

                 }

               }

-              lemma_extensionality(xrest, yrest); 

+              lemma_extensionality(xrest, yrest);

             }

             Cons(y, yrest);

             ys;

diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy
index fdd73a1a..9bc95276 100644
--- a/Test/dafny2/TreeFill.dfy
+++ b/Test/dafny2/TreeFill.dfy
@@ -28,3 +28,4 @@ method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int)
       }

   }

 }

+