summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Dan Rosen <danr@chalmers.se>2014-07-07 17:37:29 -0700
committerGravatar Dan Rosen <danr@chalmers.se>2014-07-07 17:37:29 -0700
commit79eae1e70e52bde8acfbfb2a09a0560c7319b224 (patch)
tree6dd209ac08a7207882e876e3659204314d256a9d /Test
parent661faf59f8e1003cdbf339260d1293e8dd77f2df (diff)
Tidy up two files in test suite
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny3/GenericSort.dfy4
-rw-r--r--Test/dafny4/GHC-MergeSort.dfy25
2 files changed, 6 insertions, 23 deletions
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
index 36967ab2..53d98bc2 100644
--- a/Test/dafny3/GenericSort.dfy
+++ b/Test/dafny3/GenericSort.dfy
@@ -1,3 +1,6 @@
+// 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
@@ -137,7 +140,6 @@ 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/dafny4/GHC-MergeSort.dfy b/Test/dafny4/GHC-MergeSort.dfy
index e9b36adf..e06773eb 100644
--- a/Test/dafny4/GHC-MergeSort.dfy
+++ b/Test/dafny4/GHC-MergeSort.dfy
@@ -384,8 +384,8 @@ lemma sorted_reverse(xs: List<G>, ys: List<G>)
lemma sorted_insertInMiddle(xs: List<G>, a: G, ys: List<G>)
requires sorted(reverse(xs, ys));
- requires forall y :: y in multiset_of(xs) ==> Below(y, a); // another precondition
- requires forall y :: y in multiset_of(ys) ==> Below(a, y); // this is the precondition
+ requires forall y :: y in multiset_of(xs) ==> Below(y, a);
+ requires forall y :: y in multiset_of(ys) ==> Below(a, y);
ensures sorted(reverse(xs, Cons(a, ys)));
{
match xs {
@@ -398,7 +398,7 @@ lemma sorted_insertInMiddle(xs: List<G>, a: G, ys: List<G>)
{ sorted_replaceSuffix(xs', Cons(b, ys), Cons(a, ys)); }
sorted(reverse(xs', Cons(a, ys)));
{ sorted_reverse(xs', Cons(b, ys));
- sorted_insertInMiddle(xs', b, Cons(a, ys)); } // a precondition might not hold
+ sorted_insertInMiddle(xs', b, Cons(a, ys)); }
sorted(reverse(xs', Cons(b, Cons(a, ys))));
}
}
@@ -416,25 +416,6 @@ lemma sorted_replaceSuffix(xs: List<G>, ys: List<G>, zs: List<G>)
ensures Below(a, b);
{
sorted_reverse(xs', Cons(c, ys));
- /*
- assert a in multiset_of(xs);
- if (b in multiset_of(Cons(c, ys))) {
- sorted_reverse(xs', Cons(c, ys));
- } else {
- assert b !in multiset_of(Cons(c, ys));
- assert multiset_of(Cons(c,ys)) == multiset{c} + multiset_of(ys);
- var mc := multiset{c};
- assert b !in mc;
- assert b !in multiset{c};
- assert b !in multiset_of(ys);
- assert b !in multiset{c} && b !in multiset_of(ys);
- assert b !in multiset{c} + multiset_of(ys);
- assert b != c;
- assert b in multiset_of(zs);
- // use requires 409
- }
- // assume b != c;
- */
}
sorted_replaceSuffix(xs', Cons(c, ys), Cons(c, zs));
}