From 72dba23b3ec67244cdf7c598a953bf4fdf32a001 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 18 Dec 2013 16:19:41 -0800 Subject: Added test3/GenericSort.dfy, which shows how modules can be used to write and use a sorting routine parameterized with a comparison function --- Test/dafny3/Answer | 34 ++++++----- Test/dafny3/GenericSort.dfy | 145 ++++++++++++++++++++++++++++++++++++++++++++ Test/dafny3/runtest.bat | 4 +- 3 files changed, 166 insertions(+), 17 deletions(-) create mode 100644 Test/dafny3/GenericSort.dfy (limited to 'Test/dafny3') 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, 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, 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, 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) + 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 -------------------- -- cgit v1.2.3