diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-02 18:18:07 -0800 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-03-02 18:18:07 -0800 |
| commit | 42297fe53a0e433a6d913be2ec5c067264a17f68 (patch) | |
| tree | 22da0dc2f699bedb86c31f98bea130cda9920d76 /Test/dafny0 | |
| parent | f2d02cf07f597ebda226a0e55d3d2e5faf9c85b9 (diff) | |
| parent | b07e5b62739645a6a3a4018b41c0e8690f0e10ff (diff) | |
Merge
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/LetExpr.dfy | 40 |
2 files changed, 43 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e5dc3ba2..9995c817 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1445,7 +1445,7 @@ Execution trace: (0,0): anon0
(0,0): anon11_Then
-Dafny program verifier finished with 13 verified, 2 errors
+Dafny program verifier finished with 19 verified, 2 errors
-------------------- Predicates.dfy --------------------
Predicates.dfy[B](18,5): Error BP5003: A postcondition might not hold on this return path.
@@ -1719,7 +1719,7 @@ Execution trace: (0,0): anon0
(0,0): anon11_Then
-Dafny program verifier finished with 13 verified, 2 errors
+Dafny program verifier finished with 19 verified, 2 errors
out.tmp.dfy(10,12): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -1728,4 +1728,4 @@ Execution trace: (0,0): anon0
(0,0): anon11_Then
-Dafny program verifier finished with 13 verified, 2 errors
+Dafny program verifier finished with 19 verified, 2 errors
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index 48e4810b..11bf4fbe 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.dfy @@ -107,3 +107,43 @@ method PMain(a: array<int>) 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
+}
|