diff options
Diffstat (limited to 'Test/textbook')
| -rw-r--r-- | Test/textbook/Answer | 4 | ||||
| -rw-r--r-- | Test/textbook/Bubble.bpl | 18 | ||||
| -rw-r--r-- | Test/textbook/DutchFlag.bpl | 37 | ||||
| -rw-r--r-- | Test/textbook/Find.bpl | 29 | ||||
| -rw-r--r-- | Test/textbook/McCarthy-91.bpl | 12 | ||||
| -rw-r--r-- | Test/textbook/runtest.bat | 2 |
6 files changed, 69 insertions, 33 deletions
diff --git a/Test/textbook/Answer b/Test/textbook/Answer index 538109f5..50e96aca 100644 --- a/Test/textbook/Answer +++ b/Test/textbook/Answer @@ -14,3 +14,7 @@ Boogie program verifier finished with 1 verified, 0 errors ------------------------------ DivMod.bpl ---------------------
Boogie program verifier finished with 2 verified, 0 errors
+
+------------------------------ McCarthy-91.bpl ---------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/textbook/Bubble.bpl b/Test/textbook/Bubble.bpl index 51a8cefa..80ecc9a0 100644 --- a/Test/textbook/Bubble.bpl +++ b/Test/textbook/Bubble.bpl @@ -1,11 +1,25 @@ -// Bubble sort, where specification says the output is a permutation of its input
-// Rustan Leino, 30 April 2009
+// Bubble Sort, where the specification says the output is a permutation of
+// the input.
+// Introduce a constant 'N' and postulate that it is non-negative
const N: int;
axiom 0 <= N;
+// Declare a map from integers to integers. In the procedure below, 'a' will be
+// treated as an array of 'N' elements, indexed from 0 to less than 'N'.
var a: [int]int;
+// This procedure implements Bubble Sort. One of the postconditions says that,
+// in the final state of the procedure, the array is sorted. The other
+// postconditions say that the final array is a permutation of the initial
+// array. To write that part of the specification, the procedure returns that
+// permutation mapping. That is, out-parameter 'perm' injectively maps the
+// numbers [0..N) to [0..N), as stated by the second and third postconditions.
+// The final postcondition says that 'perm' describes how the elements in
+// 'a' moved: what is now at index 'i' used to be at index 'perm[i]'.
+// Note, the specification says nothing about the elements of 'a' outside the
+// range [0..N). Moreover, Boogie does not prove that the program will terminate.
+
procedure BubbleSort() returns (perm: [int]int)
modifies a;
// array is sorted
diff --git a/Test/textbook/DutchFlag.bpl b/Test/textbook/DutchFlag.bpl index 34065b7d..03fd2317 100644 --- a/Test/textbook/DutchFlag.bpl +++ b/Test/textbook/DutchFlag.bpl @@ -1,3 +1,11 @@ +// The partition step of Quick Sort picks a 'pivot' element from a specified subsection
+// of a given integer array. It then partially sorts the elements of the array so that
+// elements smaller than the pivot end up to the left of the pivot and elements larger
+// than the pivot end up to the right of the pivot. Finally, the index of the pivot is
+// returned.
+// The procedure below always picks the first element of the subregion as the pivot.
+// The specification of the procedure talks about the ordering of the elements, but
+// does not say anything about keeping the multiset of elements the same.
var A: [int]int;
const N: int;
@@ -10,22 +18,22 @@ procedure Partition(l: int, r: int) returns (result: int) 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;
+ var pv, i, j, tmp: int;
+
+ 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;
+ // The following loop iterates while 'i < j'. In each iteration,
+ // one of the three alternatives (A, B, or C) is chosen in such
+ // a way that the assume statements will evaluate to true.
LoopHead:
+ // The following the assert statements give the loop invariant
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;
@@ -58,5 +66,4 @@ procedure Partition(l: int, r: int) returns (result: int) exit:
assume i == j;
result := i;
- return;
}
diff --git a/Test/textbook/Find.bpl b/Test/textbook/Find.bpl index d84209e1..effedf92 100644 --- a/Test/textbook/Find.bpl +++ b/Test/textbook/Find.bpl @@ -1,39 +1,38 @@ -// 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.
-
+// Declare a constant 'K' and a function 'f' and postulate that 'K' is
+// in the image of 'f'
const K: int;
function f(int) returns (int);
axiom (exists k: int :: f(k) == K);
-procedure Find(a: int, b: int) returns (k: int);
+// This procedure will find a domain value 'k' that 'f' maps to 'K'. It will
+// do that by recursively enlarging the range where no such domain value exists.
+// Note, Boogie does not prove termination.
+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;
+ goto A, B, C; // nondeterministically choose one of these 3 goto targets
A:
- assume f(a) == K; k := a;
+ assume f(a) == K; // assume we get here only if 'f' maps 'a' to 'K'
+ k := a;
return;
B:
- assume f(b) == K; k := b;
+ assume f(b) == K; // assume we get here only if 'f' maps 'b' to 'K'
+ k := b;
return;
C:
- assume f(a) != K && f(b) != K;
+ assume f(a) != K && f(b) != K; // neither of the two above
call k := Find(a-1, b+1);
return;
}
+// This procedure shows one way to call 'Find'
procedure Main() returns (k: int)
ensures f(k) == K;
{
- entry:
- call k := Find(0, 0);
- return;
+ call k := Find(0, 0);
}
diff --git a/Test/textbook/McCarthy-91.bpl b/Test/textbook/McCarthy-91.bpl new file mode 100644 index 00000000..899a7ff1 --- /dev/null +++ b/Test/textbook/McCarthy-91.bpl @@ -0,0 +1,12 @@ +// McCarthy 91 function
+procedure F(n: int) returns (r: int)
+ ensures 100 < n ==> r == n - 10;
+ ensures n <= 100 ==> r == 91;
+{
+ if (100 < n) {
+ r := n - 10;
+ } else {
+ call r := F(n + 11);
+ call r := F(r);
+ }
+}
diff --git a/Test/textbook/runtest.bat b/Test/textbook/runtest.bat index bdfdd7d5..265aa071 100644 --- a/Test/textbook/runtest.bat +++ b/Test/textbook/runtest.bat @@ -6,7 +6,7 @@ set BPLEXE=%BOOGIEDIR%\Boogie.exe REM ======================
REM ====================== Examples written in Boogie
REM ======================
-for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl) do (
+for %%f in (Find.bpl DutchFlag.bpl Bubble.bpl DivMod.bpl McCarthy-91.bpl) do (
echo.
echo ------------------------------ %%f ---------------------
%BPLEXE% %* %%f
|