Dafny: added let expressions (syntax: "var x := E0; E1")

Dafny: firmed up semantics of assert/assume expressions (the condition is now good for all program control paths that pass through the expression)
Dafny: various implementation clean-ups

1 files changed, 29 insertions, 1 deletions

diff --git a/Test/dafny0/PredExpr.dfy b/Test/dafny0/PredExpr.dfy
index 740c2308..96561ebd 100644
--- a/Test/dafny0/PredExpr.dfy
+++ b/Test/dafny0/PredExpr.dfy
@@ -1,3 +1,16 @@
+function SimpleAssert(n: int): int

+  ensures n < 100;

+{

+  assert n == 58;  // error: assert violation

+  n  // but postcondition is fine

+}

+

+function SimpleAssume(n: int): int

+  ensures n < 100;

+{

+  assume n == 58; n  // all is fine

+}

+

 function Subonacci(n: nat): nat

 {

   if 2 <= n then

@@ -18,7 +31,7 @@ function F(n: int): nat
 function G(n: int, b: bool): nat

 {

   if b then

-    Subonacci(assume 0 <= n; n)

+    Subonacci(assume 0 <= n; n) + n  // the last n is also affected by the assume

   else

     Subonacci(n)  // error: n may not be a nat

 }

@@ -49,3 +62,18 @@ function method FuncMeth(): int {
                       // PredicateExpr is not included in compilation

   15

 }

+

+method M5(a: int, b: int)

+{

+  var k := if a < 0 then

+             assume b < 0; 5

+           else

+             5;

+  if (*) {

+    assert a == -7 ==> b < 0;

+    assert b < 0;  // error: this condition does not hold on every path here

+  } else {

+    assert assume a == -7; b < 0;  // note, this is different than the ==> above

+    assert b < 0;  // this condition does hold on all paths to here

+  }

+}