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

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