Initial set of files.

6 files changed, 204 insertions, 0 deletions

diff --git a/Test/textbook/Answer b/Test/textbook/Answer
new file mode 100644
index 00000000..9e2227dc
--- /dev/null
+++ b/Test/textbook/Answer
@@ -0,0 +1,12 @@
+

+------------------------------ Find.bpl ---------------------

+

+Boogie program verifier finished with 2 verified, 0 errors

+

+------------------------------ DutchFlag.bpl ---------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

+

+------------------------------ Bubble.bpl ---------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/textbook/Bubble.bpl b/Test/textbook/Bubble.bpl
new file mode 100644
index 00000000..51a8cefa
--- /dev/null
+++ b/Test/textbook/Bubble.bpl
@@ -0,0 +1,66 @@
+// Bubble sort, where specification says the output is a permutation of its input

+// Rustan Leino, 30 April 2009

+

+const N: int;

+axiom 0 <= N;

+

+var a: [int]int;

+

+procedure BubbleSort() returns (perm: [int]int)

+  modifies a;

+  // array is sorted

+  ensures (forall i, j: int :: 0 <= i && i <= j && j < N ==> a[i] <= a[j]);

+  // perm is a permutation

+  ensures (forall i: int :: 0 <= i && i < N ==> 0 <= perm[i] && perm[i] < N);

+  ensures (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);

+  // the final array is that permutation of the input array

+  ensures (forall i: int :: 0 <= i && i < N ==> a[i] == old(a)[perm[i]]);

+{

+  var n, p, tmp: int;

+

+  n := 0;

+  while (n < N)

+    invariant n <= N;

+    invariant (forall i: int :: 0 <= i && i < n ==> perm[i] == i);

+  {

+    perm[n] := n;

+    n := n + 1;

+  }

+

+  while (true)

+    invariant 0 <= n && n <= N;

+    // array is sorted from n onwards

+    invariant (forall i, k: int :: n <= i && i < N && 0 <= k && k < i ==> a[k] <= a[i]);

+    // perm is a permutation

+    invariant (forall i: int :: 0 <= i && i < N ==> 0 <= perm[i] && perm[i] < N);

+    invariant (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);

+    // the current array is that permutation of the input array

+    invariant (forall i: int :: 0 <= i && i < N ==> a[i] == old(a)[perm[i]]);

+  {

+    n := n - 1;

+    if (n < 0) {

+      break;

+    }

+

+    p := 0;

+    while (p < n)

+      invariant p <= n;

+      // array is sorted from n+1 onwards

+      invariant (forall i, k: int :: n+1 <= i && i < N && 0 <= k && k < i ==> a[k] <= a[i]);

+      // perm is a permutation

+      invariant (forall i: int :: 0 <= i && i < N ==> 0 <= perm[i] && perm[i] < N);

+      invariant (forall i, j: int :: 0 <= i && i < j && j < N ==> perm[i] != perm[j]);

+      // the current array is that permutation of the input array

+      invariant (forall i: int :: 0 <= i && i < N ==> a[i] == old(a)[perm[i]]);

+      // a[p] is at least as large as any of the first p elements

+      invariant (forall k: int :: 0 <= k && k < p ==> a[k] <= a[p]);

+    {

+      if (a[p+1] < a[p]) {

+        tmp := a[p];  a[p] := a[p+1];  a[p+1] := tmp;

+        tmp := perm[p];  perm[p] := perm[p+1];  perm[p+1] := tmp;

+      }

+

+      p := p + 1;

+    }

+  }

+}

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;

+}

diff --git a/Test/textbook/Find.bpl b/Test/textbook/Find.bpl
new file mode 100644
index 00000000..d84209e1
--- /dev/null
+++ b/Test/textbook/Find.bpl
@@ -0,0 +1,39 @@
+// This program is featured in KRML 168, the Marktoberdorf lecture notes

+// "A verifying compiler for a multi-threaded object-oriented language" by

+// Leino and Schulte.

+

+const K: int;

+function f(int) returns (int);

+axiom (exists k: int :: f(k) == K);

+

+procedure Find(a: int, b: int) returns (k: int);

+  requires a <= b;

+  requires (forall j: int :: a < j && j < b ==> f(j) != K);

+  ensures f(k) == K;

+

+implementation Find(a: int, b: int) returns (k: int)

+{

+  entry:

+    goto A, B, C;

+

+  A:

+    assume f(a) == K;  k := a;

+    return;

+

+  B:

+    assume f(b) == K;  k := b;

+    return;

+

+  C:

+    assume f(a) != K && f(b) != K;

+    call k := Find(a-1, b+1);

+    return;

+}

+

+procedure Main() returns (k: int)

+  ensures f(k) == K;

+{

+  entry:

+    call k := Find(0, 0);

+    return;

+}

diff --git a/Test/textbook/Output b/Test/textbook/Output
new file mode 100644
index 00000000..9e2227dc
--- /dev/null
+++ b/Test/textbook/Output
@@ -0,0 +1,12 @@
+

+------------------------------ Find.bpl ---------------------

+

+Boogie program verifier finished with 2 verified, 0 errors

+

+------------------------------ DutchFlag.bpl ---------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

+

+------------------------------ Bubble.bpl ---------------------

+

+Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/textbook/runtest.bat b/Test/textbook/runtest.bat
new file mode 100644
index 00000000..6e39e589
--- /dev/null
+++ b/Test/textbook/runtest.bat
@@ -0,0 +1,13 @@
+@echo off

+

+set BOOGIEDIR=..\..\Binaries

+set BPLEXE=%BOOGIEDIR%\Boogie.exe

+

+REM ======================

+REM ====================== Examples written in Boogie

+REM ======================

+for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl) do (

+  echo.

+  echo ------------------------------ %%f ---------------------

+  %BPLEXE% %* %%f

+)