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, 109 insertions, 0 deletions

diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy
new file mode 100644
index 00000000..703813d2
--- /dev/null
+++ b/Test/dafny0/LetExpr.dfy
@@ -0,0 +1,109 @@
+method M0(n: int)

+  requires var f := 100; n < f;

+{

+  assert n < 200;

+  assert 0 <= n;  // error

+}

+

+method M1()

+{

+  assert var f := 54; var g := f + 1; g == 55;

+}

+

+method M2()

+{

+  assert var f := 54; var f := f + 1; f == 55;

+}

+

+function method Fib(n: nat): nat

+{

+  if n < 2 then n else Fib(n-1) + Fib(n-2)

+}

+

+method M3(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6;

+  ensures (r + var t := r; t*2) == 3*r;

+{

+  assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3);

+

+  {

+    var x,y := Fib(8), Fib(11);

+    assume x == 21;

+    assert Fib(7) == 3 ==> Fib(9) == 24;

+    assume Fib(1000) == 1000;

+    assume Fib(9) - Fib(8) == 13;

+    assert Fib(9) <= Fib(10);

+    assert y == 89;

+  }

+

+  assert Fib(1000) == 1000;  // does it still know this?

+

+  parallel (i | 0 <= i < a.Length) ensures true; {

+    var j := i+1;

+    assert j < a.Length ==> a[i] == a[j];

+  }

+}

+

+// M4 is pretty much the same as M3, except with things rolled into expressions.

+method M4(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= i < a.Length ==> a[i] == 6;

+  ensures (r + var t := r; t*2) == 3*r;

+{

+  assert Fib(2) + Fib(4) == Fib(0) + Fib(1) + Fib(2) + Fib(3);

+  assert

+    var x,y := Fib(8), Fib(11);

+    assume x == 21;

+    assert Fib(7) == 3 ==> Fib(9) == 24;

+    assume Fib(1000) == 1000;

+    assume Fib(9) - Fib(8) == 13;

+    assert Fib(9) <= Fib(10);

+    y == 89;

+  assert Fib(1000) == 1000;  // still known, because the assume was on the path here

+  assert forall i :: 0 <= i < a.Length ==> var j := i+1; j < a.Length ==> a[i] == a[j];

+}

+

+var index: int;

+method P(a: array<int>) returns (b: bool, ii: int)

+  requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;

+  modifies this, a;

+  ensures ii == index;

+  // The following uses a variable with a non-old definition inside an old expression:

+  ensures 0 <= index < a.Length && old(a[ii]) == 19;

+  ensures 0 <= index < a.Length && var newIndex := index; old(a[newIndex]) == 19;

+  // The following places both the variable and the body inside an old:

+  ensures b ==> old(var oldIndex := index; 0 <= oldIndex < a.Length && a[oldIndex] == 17);

+  // Here, the definition of the variable is old, and it's used both inside and

+  // inside an old expression:

+  ensures var oi := old(index); oi == index ==> a[oi] == 21 && old(a[oi]) == 19;

+{

+  b := 0 <= index < a.Length && a[index] == 17;

+  var i, j := 0, -1;

+  while (i < a.Length)

+    invariant 0 <= i <= a.Length;

+    invariant forall k :: 0 <= k < i ==> a[k] == 21;

+    invariant forall k :: i <= k < a.Length ==> a[k] == old(a[k]);

+    invariant (0 <= j < i && old(a[j]) == 19) ||

+              (j == -1 && exists k :: i <= k < a.Length && a[k] == 19);

+  {

+    if (a[i] == 19) { j := i; }

+    i, a[i] := i + 1, 21;

+  }

+  index := j;

+  ii := index;

+}

+

+method PMain(a: array<int>)

+  requires a != null && exists k :: 0 <= k < a.Length && a[k] == 19;

+  modifies this, a;

+{

+  var s := a[..];

+  var b17, ii := P(a);

+  assert s == old(a[..]);

+  assert s[index] == 19;

+  if (*) {

+    assert a[index] == 19;  // error (a can have changed in P)

+  } else {

+    assert b17 ==> 0 <= old(index) < a.Length && old(a[index]) == 17;

+    assert index == old(index) ==> a[index] == 21 && old(a[index]) == 19;

+  }

+}