Initial set of files.

1 files changed, 62 insertions, 0 deletions

diff --git a/Test/textbook/DutchFlag.bpl b/Test/textbook/DutchFlag.bpl
new file mode 100644
index 00000000..34065b7d
--- /dev/null
+++ b/Test/textbook/DutchFlag.bpl
@@ -0,0 +1,62 @@
+

+var A: [int]int;

+const N: int;

+

+procedure Partition(l: int, r: int) returns (result: int)

+  requires 0 <= l && l+2 <= r && r <= N;

+  modifies A;

+  ensures l <= result && result < r;

+  ensures (forall k: int, j: int :: l <= k && k < result && result <= j && j < r  ==>  A[k] <= A[j]);

+  ensures (forall k: int :: l <= k && k < result  ==>  A[k] <= old(A)[l]);

+  ensures (forall k: int :: result <= k && k < r  ==>  old(A)[l] <= A[k]);

+{

+  var pv: int;

+  var i: int;

+  var j: int;

+  var tmp: int;

+

+  start:

+    pv := A[l];

+    i := l;

+    j := r-1;

+    // swap A[l] and A[j]

+    tmp := A[l];

+    A[l] := A[j];

+    A[j] := tmp;

+    goto LoopHead;

+

+  LoopHead:

+    assert (forall k: int :: l <= k && k < i  ==>  A[k] <= pv);

+    assert (forall k: int :: j <= k && k < r  ==>  pv <= A[k]);

+    assert l <= i && i <= j && j < r;

+    goto A, B, C, exit;

+

+  A:

+    assume i < j;

+    assume A[i] <= pv;

+    i := i + 1;

+    goto LoopHead;

+

+  B:

+    assume i < j;

+    assume pv <= A[j-1];

+    j := j - 1;

+    goto LoopHead;

+

+  C:

+    assume i < j;

+    assume A[j-1] < pv && pv < A[i];

+    // swap A[j-1] and A[i]

+    tmp := A[i];

+    A[i] := A[j-1];

+    A[j-1] := tmp;

+    assert A[i] < pv && pv < A[j-1];

+    i := i + 1;

+    j := j - 1;

+    goto LoopHead;

+

+  exit:

+    assume i == j;

+    result := i;

+    return;

+}