Implemented resolution, verification, and (poorly performing) compilation of existential if guards.

Fixed bugs in ghost checks involving comprehensions and attributes.
Added SubstituteBoundedPool method.

1 files changed, 34 insertions, 1 deletions

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index a2b96996..7f9169da 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny "%s" > "%t"

+// RUN: %dafny /compile:3 "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 // The tests in this file are designed to run through the compiler.  They contain

@@ -43,6 +43,8 @@ module CoRecursion {
   //   40

   //   41

   //   42

+  //   9

+  //   9

   method Main() {

     var m := 17;

     var cell := new Cell;

@@ -58,6 +60,37 @@ module CoRecursion {
       print l.car, "\n";

       l := l.cdr;

     }

+    var nio := OneLess(0, 10);

+    print nio, "\n";

+    nio := OneLess'(0, 10);

+    print nio, "\n";

+  }

+

+  method OneLess(lo: int, hi: int) returns (m: int)

+    requires lo < hi

+    // This method ensures m == hi - 1, but we don't care to prove it

+    decreases hi - lo

+  {

+    if y :| lo < y < hi {

+      m := OneLess(y, hi);

+    } else {

+      m := lo;

+    }

+  }

+

+  method OneLess'(lo: int, hi: int) returns (m: int)

+    requires lo < hi

+    // This method ensures m == hi - 1, but we don't care to prove it

+    decreases hi - lo

+  {

+    if {

+      case y :| lo < y < hi =>

+        m := OneLess'(y, hi);

+      case lo+1 < hi =>

+        m := OneLess'(lo+1, hi);

+      case lo + 1 == hi =>

+        m := lo;

+    }

   }

 }