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

---
 Test/dafny3/Dijkstra.dfy      | 2 +-
 Test/dafny3/GenericSort.dfy   | 4 +---
 Test/dafny3/InfiniteTrees.dfy | 5 +++--
 Test/dafny3/OpaqueTrees.dfy   | 2 +-
 4 files changed, 6 insertions(+), 7 deletions(-)

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
index e90687e0..acc29ccd 100644
--- a/Test/dafny3/Dijkstra.dfy
+++ b/Test/dafny3/Dijkstra.dfy
@@ -65,7 +65,7 @@ ghost method lemma_pong(n: nat)
   <==  { lemma_monotonicity_0(n + 1, f(n)); }
     f(f(n)) < f(n + 1);
   ==  // P with m := n
-    true;        
+    true;
   }
 }
 
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
index 53d98bc2..36967ab2 100644
--- a/Test/dafny3/GenericSort.dfy
+++ b/Test/dafny3/GenericSort.dfy
@@ -1,6 +1,3 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
 abstract module TotalOrder {
   type T // the type to be compared
   static predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b
@@ -140,6 +137,7 @@ module Client {
      // Call the sorting routine to sort the array
      IntSort.InsertionSort(a);
      // Check the answer
+//     assert IntSort.Sorted(a, 0, a.Length);
      assert IntSort.O.Leq(a[0], a[1]);  // lemma
      assert IntSort.O.Leq(a[1], a[2]);  // lemma
      assert IntSort.O.Leq(a[2], a[3]);  // lemma
diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy
index 030443c0..516a9e4e 100644
--- a/Test/dafny3/InfiniteTrees.dfy
+++ b/Test/dafny3/InfiniteTrees.dfy
@@ -38,7 +38,7 @@ lemma Tail_Lemma2(s: Stream, n: nat)
 
 // Co-predicate IsNeverEndingStream(s) answers whether or not s ever contains Nil.
 
-copredicate IsNeverEndingStream(s: Stream)
+copredicate IsNeverEndingStream<S>(s: Stream<S>)
 {
   match s
   case Nil => false
@@ -247,7 +247,8 @@ lemma ValidPath_Lemma(p: Stream<int>)
     match p {
       case Nil =>
       case Cons(index, tail) =>  // proof by contradiction
-        Tail_Lemma1(Nil, 0, index);
+        var nil : Stream<Tree> := Nil;
+        Tail_Lemma1(nil, 0, index);
     }
   }
 }
diff --git a/Test/dafny3/OpaqueTrees.dfy b/Test/dafny3/OpaqueTrees.dfy
index 53540c1d..432d107a 100644
--- a/Test/dafny3/OpaqueTrees.dfy
+++ b/Test/dafny3/OpaqueTrees.dfy
@@ -10,7 +10,7 @@ function {:opaque} size(t: Tree): nat
   case Node(left, right) => 1 + size(left) + size(right)
 }
 
-function {:opaque} mirror(t: Tree): Tree
+function {:opaque} mirror<T>(t: Tree<T>): Tree<T>
 {
   match t
   case Leaf(_) => t
-- 
cgit v1.2.3