Improvements in sequence axioms to make checking more automatic.

Minor changes in a test file.

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";

   }

 }