Added test3/GenericSort.dfy, which shows how modules can be used to write and use a sorting routine parameterized with a comparison function

3 files changed, 166 insertions, 17 deletions

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 5b7357e6..9e8ac835 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -1,60 +1,64 @@
-

+
 -------------------- Iter.dfy --------------------

 

 Dafny program verifier finished with 15 verified, 0 errors

-

+
 -------------------- Streams.dfy --------------------

 

 Dafny program verifier finished with 52 verified, 0 errors

-

+
 -------------------- Dijkstra.dfy --------------------

 

 Dafny program verifier finished with 12 verified, 0 errors

-

+
 -------------------- CachedContainer.dfy --------------------

 

 Dafny program verifier finished with 47 verified, 0 errors

-

+
 -------------------- SimpleInduction.dfy --------------------

 

 Dafny program verifier finished with 12 verified, 0 errors

-

+
 -------------------- SimpleCoinduction.dfy --------------------

 

 Dafny program verifier finished with 31 verified, 0 errors

-

+
 -------------------- CalcExample.dfy --------------------

 

 Dafny program verifier finished with 6 verified, 0 errors

-

+
 -------------------- InductionVsCoinduction.dfy --------------------

 

 Dafny program verifier finished with 20 verified, 0 errors

-

+
 -------------------- Zip.dfy --------------------

 

 Dafny program verifier finished with 24 verified, 0 errors

-

+
 -------------------- SetIterations.dfy --------------------

 

 Dafny program verifier finished with 13 verified, 0 errors

-

+
 -------------------- Paulson.dfy --------------------

 

 Dafny program verifier finished with 28 verified, 0 errors

-

+
 -------------------- Filter.dfy --------------------

 

 Dafny program verifier finished with 43 verified, 0 errors

-

+
 -------------------- WideTrees.dfy --------------------

 

 Dafny program verifier finished with 10 verified, 0 errors

-

+
 -------------------- InfiniteTrees.dfy --------------------

 

 Dafny program verifier finished with 88 verified, 0 errors

-

+
 -------------------- OpaqueTrees.dfy --------------------

 

 Dafny program verifier finished with 6 verified, 0 errors

+
+-------------------- GenericSort.dfy --------------------

+

+Dafny program verifier finished with 36 verified, 0 errors

diff --git a/Test/dafny3/GenericSort.dfy b/Test/dafny3/GenericSort.dfy
new file mode 100644
index 00000000..5ae512de
--- /dev/null
+++ b/Test/dafny3/GenericSort.dfy
@@ -0,0 +1,145 @@
+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

+  // lemmas, that is, as axioms.

+  static lemma Antisymmetry(a: T, b: T)

+    requires Leq(a, b) && Leq(b, a);

+    ensures a == b;

+  static lemma Transitivity(a: T, b: T, c: T)

+    requires Leq(a, b) && Leq(b, c);

+    ensures Leq(a, c);

+  static lemma Totality(a: T, b: T)

+    ensures Leq(a, b) || Leq(b, a);

+}

+

+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)

+    requires a != null && 0 <= low <= high <= a.Length;

+    reads a;

+    // The body of the predicate is hidden outside the module, but the postcondition is

+    // "exported" (that is, visible, known) outside the module.  Here, we choose the

+    // export the following property:

+    ensures Sorted(a, low, high) ==> forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j]);

+  {

+    forall i, j :: low <= i < j < high ==> O.Leq(a[i], a[j])

+  }

+

+  // In the insertion sort routine below, it's more convenient to keep track of only that

+  // neighboring elements of the array are sorted...

+  static predicate NeighborSorted(a: array<O.T>, low: int, high: int)

+    requires a != null && 0 <= low <= high <= a.Length;

+    reads a;

+  {

+    forall i :: low < i < high ==> O.Leq(a[i-1], a[i])

+  }

+  // ...but we show that property to imply all pairs to be sorted.  The proof of this

+  // lemma uses the transitivity property.

+  static lemma NeighborSorted_implies_Sorted(a: array<O.T>, low: int, high: int)

+    requires a != null && 0 <= low <= high <= a.Length;

+    requires NeighborSorted(a, low, high);

+    ensures Sorted(a, low, high);

+    decreases high - low;

+  {

+    if low != high {

+      NeighborSorted_implies_Sorted(a, low+1, high);

+      forall j | low+1 < j < high

+      {

+        O.Transitivity(a[low], a[low+1], a[j]);

+      }

+    }

+  }

+

+  // Standard insertion sort method

+  static method InsertionSort(a: array<O.T>)

+    requires a != null;

+    modifies a;

+    ensures Sorted(a, 0, a.Length);

+    ensures multiset(a[..]) == old(multiset(a[..]));

+  {

+    if a.Length == 0 { return; }

+    var i := 1;

+    while i < a.Length

+      invariant 0 < i <= a.Length;

+      invariant NeighborSorted(a, 0, i);

+      invariant multiset(a[..]) == old(multiset(a[..]));

+    {

+      var j := i;

+      while 0 < j && !O.Leq(a[j-1], a[j])

+        invariant 0 <= j <= i;

+        invariant NeighborSorted(a, 0, j);

+        invariant NeighborSorted(a, j, i+1);

+        invariant 0 < j < i ==> O.Leq(a[j-1], a[j+1]);

+        invariant multiset(a[..]) == old(multiset(a[..]));

+      {

+        // The proof of correctness uses the totality property here.

+        // It implies that if two elements are not previously in

+        // sorted order, they will be after swapping them.

+        O.Totality(a[j-1], a[j]);

+        a[j], a[j-1] := a[j-1], a[j];

+        j := j - 1;

+      }

+      i := i + 1;

+    }

+    NeighborSorted_implies_Sorted(a, 0, a.Length);

+  }

+}

+

+// Natural ordering of the integers

+module IntOrder refines TotalOrder {

+  // Instantiate type T with a datatype wrapper around an integer.

+  // (If there were type synonyms, we could perhaps have written just "type T = int".)

+  datatype T = Int(i: int)

+  // Define the ordering on these integers

+  static predicate method Leq ...

+    ensures Leq(a, b) ==> a.i <= b.i;

+  {

+    a.i <= b.i

+  }

+  // The three required properties of the order are proved here as lemmas.

+  // The proofs are automatic and don't require any further assistance.

+  static lemma Antisymmetry ... { }

+  static lemma Transitivity ... { }

+  static lemma Totality ... { }

+}

+

+// Another example of a TotalOrder. Now we can sort pairs of integers.

+// Lexiographic ordering of pairs of integers

+module IntLexOrder refines TotalOrder {

+  datatype T = Int(i: int, j: int)

+  static predicate method Leq ... {

+    if a.i < b.i then true

+    else if a.i == b.i then a.j <= b.j

+    else false

+  }

+  static lemma Antisymmetry ... { }

+  static lemma Transitivity ... { }

+  static lemma Totality ... { }

+}

+

+

+// A test harness.

+module Client {

+  module IntSort refines Sort {  // this creates a new sorting module, like Sort by fully revealing O to be IntOrder

+    import O = IntOrder

+  }

+  import I = IntOrder

+  method Main() {

+     var a := new I.T[4];

+     a[0] := I.T.Int(6);  // alternatively, we could have written the RHS as:  IntSort.O.T.Int(6)

+     a[1] := I.T.Int(1);

+     a[2] := I.T.Int(0);

+     a[3] := I.T.Int(4);

+     // These are now the elements of the array:

+     assert a[..] == [I.T.Int(6), I.T.Int(1), I.T.Int(0), I.T.Int(4)];

+     // Call the sorting routine to sort the array

+     IntSort.InsertionSort(a);

+     // Check the answer

+     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

+     assert a[..] == [I.T.Int(0), I.T.Int(1), I.T.Int(4), I.T.Int(6)];

+  }

+}

diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index 40992f28..8abf2bd3 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -4,14 +4,14 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-%DAFNY_EXE% /compile:0 /verifySeparately %* Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy OpaqueTrees.dfy

+%DAFNY_EXE% /compile:0 /verifySeparately %* Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy OpaqueTrees.dfy GenericSort.dfy

 

 rem for %%f in (

 rem   Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy

 rem   SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy

 rem   InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy

 rem   Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy

-rem   OpaqueTrees.dfy

+rem   OpaqueTrees.dfy GenericSort.dfy

 rem ) do (

 rem   echo.

 rem   echo -------------------- %%f --------------------