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

1 files changed, 12 insertions, 0 deletions

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);

+  }

+}