diff options
Diffstat (limited to 'Test/dafny0/Use.dfy')
| -rw-r--r-- | Test/dafny0/Use.dfy | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy index 7a963382..502c4222 100644 --- a/Test/dafny0/Use.dfy +++ b/Test/dafny0/Use.dfy @@ -210,20 +210,18 @@ class Recursive { method F0()
{
- assert Fib(2) == 1; // error (does not know about Fib for the recursive calls)
+ assert Fib(3) == 2; // error (does not know about Fib for the recursive calls)
}
method F1()
{
assert Fib(0) == 0;
- assert Fib(1) == 1;
- assert Fib(2) == 1; // now it knows
+ assert Fib(3) == 2; // now it knows
}
method F2()
{
- assert Fib(0) == 0;
- use Fib(1);
- assert Fib(2) == 1; // now it knows, too
+ use Fib(0);
+ assert Fib(3) == 2; // now it knows, too
}
}
|