diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 9 | ||||
| -rw-r--r-- | Test/dafny3/GenericSort.dfy | 6 |
2 files changed, 11 insertions, 4 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 0662d12b..224c5ffd 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -410,8 +410,13 @@ axiom (forall<T> s: Seq T, i: int, j: int :: 0 <= i && i < j && j <= Seq#Length(s) ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s) );
// Additional axioms about common things
-axiom Seq#Take(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][..0] == []
-axiom Seq#Drop(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][0..] == []
+axiom (forall<T> s: Seq T, n: int :: { Seq#Drop(s, n) }
+ n == 0 ==> Seq#Drop(s, n) == s);
+axiom (forall<T> s: Seq T, n: int :: { Seq#Take(s, n) }
+ n == 0 ==> Seq#Take(s, n) == Seq#Empty());
+axiom (forall<T> s: Seq T, m, n: int :: { Seq#Drop(Seq#Drop(s, m), n) }
+ 0 <= m && 0 <= n && m+n <= Seq#Length(s) ==>
+ Seq#Drop(Seq#Drop(s, m), n) == Seq#Drop(s, m+n));
// ---------------------------------------------------------------
// -- Axiomatization of Maps -------------------------------------
diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy index 5ae512de..10589e5a 100644 --- a/Test/dafny3/GenericSort.dfy +++ b/Test/dafny3/GenericSort.dfy @@ -1,4 +1,4 @@ -module TotalOrder {
+abstract module TotalOrder {
type T // the type to be compared
static predicate method Leq(a: T, b: T) // Leq(a,b) iff a <= b
// Three properties of total orders. Here, they are given as unproved
@@ -13,7 +13,7 @@ module TotalOrder { ensures Leq(a, b) || Leq(b, a);
}
-module Sort {
+abstract module Sort {
import O as TotalOrder // let O denote some module that has the members of TotalOrder
static predicate Sorted(a: array<O.T>, low: int, high: int)
@@ -141,5 +141,7 @@ module Client { assert IntSort.O.Leq(a[1], a[2]); // lemma
assert IntSort.O.Leq(a[2], a[3]); // lemma
assert a[..] == [I.T.Int(0), I.T.Int(1), I.T.Int(4), I.T.Int(6)];
+ // why not print out the result!
+ print a[..], "\n";
}
}
|