Added Dafny solutions to the VSTTE 2012 program verification competition

1 files changed, 58 insertions, 0 deletions

diff --git a/Test/vstte2012/Two-Way-Sort.dfy b/Test/vstte2012/Two-Way-Sort.dfy
new file mode 100644
index 00000000..49ff29b4
--- /dev/null
+++ b/Test/vstte2012/Two-Way-Sort.dfy
@@ -0,0 +1,58 @@
+// This method is a slight generalization of the

+// code provided in the problem statement since it

+// is generic in the type of the array elements.

+method swap<T>(a: array<T>, i: int, j: int)

+  requires a != null;

+  requires 0 <= i < j < a.Length;

+  modifies a;

+  ensures a[i] == old(a[j]);

+  ensures a[j] == old(a[i]);

+  ensures forall m :: 0 <= m < a.Length && m != i && m != j ==> a[m] == old(a[m]);

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

+{

+  var t := a[i];

+  a[i] := a[j];

+  a[j] := t;

+}

+

+// This method is a direct translation of the pseudo

+// code given in the problem statement. 

+// The first postcondition expresses that the resulting

+// array is sorted, that is, all occurrences of "false"

+// come before all occurrences of "true".

+// The second postcondition expresses that the post-state 

+// array is a permutation of the pre-state array. To express

+// this, we use Dafny's built-in multisets. The built-in 

+// function "multiset" takes an array and yields the 

+// multiset of the array elements.

+// Note that Dafny guesses a suitable ranking function

+// for the termination proof of the while loop.

+// We use the loop guard from the given pseudo-code.  However,

+// the program also verifies with the stronger guard "i < j"

+// (without changing any of the other specifications or

+// annotations).

+method two_way_sort(a: array<bool>)

+  requires a != null;

+  modifies a;

+  ensures forall m,n :: 0 <= m < n < a.Length ==> (!a[m] || a[n]);

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

+{

+  var i := 0;

+  var j := a.Length - 1;

+  while (i <= j)

+    invariant 0 <= i <= j + 1 <= a.Length;

+    invariant forall m :: 0 <= m < i ==> !a[m];

+    invariant forall n :: j < n < a.Length ==> a[n];

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

+  {

+    if (!a[i]) {

+      i := i+1;

+    } else if (a[j]) {

+      j := j-1;

+    } else {

+      swap(a, i, j);

+      i := i+1;

+      j := j-1;

+    }

+  }

+}