diff options
author | 2014-03-19 19:08:04 +0100 | |
---|---|---|
committer | 2014-03-19 19:08:04 +0100 | |
commit | 73d20fd1f40d380f10a4a62cb8853137e340514a (patch) | |
tree | 859ce823e99fddc674757fe5d50d93b2cd11ae5c /Test/dafny0 | |
parent | 24d83b6c4fde22c8fefad80618be22d383f6d6d0 (diff) |
Propagate literals through equality operations.
Diffstat (limited to 'Test/dafny0')
-rw-r--r-- | Test/dafny0/Answer | 2 | ||||
-rw-r--r-- | Test/dafny0/Computations.dfy | 25 |
2 files changed, 24 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 09936f86..06f4e9e9 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2067,7 +2067,7 @@ Dafny program verifier finished with 1 verified, 4 errors -------------------- Computations.dfy --------------------
-Dafny program verifier finished with 49 verified, 0 errors
+Dafny program verifier finished with 58 verified, 0 errors
-------------------- ComputationsNeg.dfy --------------------
ComputationsNeg.dfy(4,3): Error: failure to decrease termination measure
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;
+}
|