From 60208673a25423e378cc7e9672d5acf9fd6f58bc Mon Sep 17 00:00:00 2001
From: Dan Rosén <danr@chalmers.se>
Date: Mon, 7 Jul 2014 15:09:33 -0700
Subject: New logical encoding of types with Is and IsAlloc

---
 .../COST-verif-comp-2011-4-FloydCycleDetect.dfy    |  8 ++++++++
 Test/dafny2/Calculations.dfy                       | 24 +++++++++++-----------
 Test/dafny2/TreeFill.dfy                           |  1 +
 3 files changed, 21 insertions(+), 12 deletions(-)

(limited to 'Test/dafny2')

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)
       }
   }
 }
+
-- 
cgit v1.2.3