summaryrefslogtreecommitdiff
path: root/Test/vstte2012/Two-Way-Sort.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/vstte2012/Two-Way-Sort.dfy')
-rw-r--r--Test/vstte2012/Two-Way-Sort.dfy58
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;
+ }
+ }
+}