1 files changed, 14 insertions, 15 deletions
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);
 }