diff options
Diffstat (limited to 'Test/dafny3')
-rw-r--r-- | Test/dafny3/Dijkstra.dfy | 2 | ||||
-rw-r--r-- | Test/dafny3/GenericSort.dfy | 4 | ||||
-rw-r--r-- | Test/dafny3/InfiniteTrees.dfy | 5 | ||||
-rw-r--r-- | Test/dafny3/OpaqueTrees.dfy | 2 |
4 files changed, 6 insertions, 7 deletions
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
|