summaryrefslogtreecommitdiff
path: root/Test/dafny0/LetExpr.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0/LetExpr.dfy')
-rw-r--r--Test/dafny0/LetExpr.dfy109
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;
+ }
+}