From 75affe5a214df74d2927785d666fbe3d7871e867 Mon Sep 17 00:00:00 2001 From: rustanleino Date: Fri, 22 Oct 2010 01:34:13 +0000 Subject: Miscellaneous changes: * Also copy CodeContractExtender in PrepareBoogieZip.bat * Added some comments and a new program in Test/textbook * Included refinement keywords in Chalice emacs mode * Used assignment instead of spec statement in DuplicatesVideo.chalice --- Test/textbook/Answer | 4 ++++ Test/textbook/Bubble.bpl | 18 ++++++++++++++++-- Test/textbook/DutchFlag.bpl | 37 ++++++++++++++++++++++--------------- Test/textbook/Find.bpl | 29 ++++++++++++++--------------- Test/textbook/McCarthy-91.bpl | 12 ++++++++++++ Test/textbook/runtest.bat | 2 +- 6 files changed, 69 insertions(+), 33 deletions(-) create mode 100644 Test/textbook/McCarthy-91.bpl (limited to 'Test') 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 -- cgit v1.2.3