diff options
Diffstat (limited to 'Test/dafny0/LetExpr.dfy')
| -rw-r--r-- | Test/dafny0/LetExpr.dfy | 149 |
1 files changed, 0 insertions, 149 deletions
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy deleted file mode 100644 index 11bf4fbe..00000000 --- a/Test/dafny0/LetExpr.dfy +++ /dev/null @@ -1,149 +0,0 @@ -method M0(n: int)
- requires var f := 100; n < f; requires var t, f := true, false; (t && f) || n < 100;
-{
- 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;
- }
-}
-
-// ---------- lemmas ----------
-
-method Theorem0(n: int)
- requires 1 <= n;
- ensures 1 <= Fib(n);
-{
- if (n < 3) {
- } else {
- Theorem0(n-2);
- Theorem0(n-1);
- }
-}
-
-ghost method Theorem1(n: int)
- requires 1 <= n;
- ensures 1 <= Fib(n);
-{
- // in a ghost method, the induction tactic takes care of it
-}
-
-function Theorem2(n: int): int
- requires 1 <= n;
- ensures 1 <= Fib(n);
-{
- if n < 3 then 5 else
- var x := Theorem2(n-2);
- var y := Theorem2(n-1);
- x + y
-}
-
-function Theorem3(n: int): int
- requires 1 <= n;
- ensures 1 <= Fib(n);
-{
- if n < 3 then 5 else
- var x := Theorem3(n-2);
- var y := Theorem3(n-1);
- 5
-}
|