summaryrefslogtreecommitdiff
path: root/Test/textbook/McCarthy-91.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/textbook/McCarthy-91.bpl')
-rw-r--r--Test/textbook/McCarthy-91.bpl28
1 files changed, 14 insertions, 14 deletions
diff --git a/Test/textbook/McCarthy-91.bpl b/Test/textbook/McCarthy-91.bpl
index 6bfbcb04..b4244b8d 100644
--- a/Test/textbook/McCarthy-91.bpl
+++ b/Test/textbook/McCarthy-91.bpl
@@ -1,14 +1,14 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// 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);
- }
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// 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);
+ }
+}