diff options
| author |  Nada Amin <namin@alum.mit.edu> | 2014-03-19 19:08:04 +0100 |
|---|---|---|
| committer | Nada Amin <namin@alum.mit.edu> | 2014-03-19 19:08:04 +0100 |
| commit | 73d20fd1f40d380f10a4a62cb8853137e340514a (patch) | |
| tree | 859ce823e99fddc674757fe5d50d93b2cd11ae5c /Test/dafny0/Computations.dfy | |
| parent | 24d83b6c4fde22c8fefad80618be22d383f6d6d0 (diff) | |
Propagate literals through equality operations.
Diffstat (limited to 'Test/dafny0/Computations.dfy')
| -rw-r--r-- | Test/dafny0/Computations.dfy | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy index d3c42af5..0481fe96 100644 --- a/Test/dafny0/Computations.dfy +++ b/Test/dafny0/Computations.dfy @@ -155,8 +155,29 @@ function power(b: int, n: nat): int {
if (n==0) then 1 else b*power(b, n-1)
}
-
ghost method test_power()
ensures power(power(2, 3), 1+power(2, 2))==32768;
{
-}
\ No newline at end of file +}
+
+function fib(n: nat): nat
+{
+ if (n<2) then n else fib(n-1)+fib(n-2)
+}
+ghost method test_fib()
+ ensures fib(12)==144;
+{
+}
+ghost method test_fib1(k: nat)
+ ensures k==12 ==> fib(k)==144;
+{
+}
+ghost method test_fib2(k: nat)
+ ensures 12<=k && k<=12 ==> fib(k)==144;
+{
+}
+ghost method test_fib3(k: nat, m: nat)
+{
+ var y := 12;
+ assert y <= k && k < y + m && m == 1 ==> fib(k)==144;
+}
|