diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-10-29 16:59:46 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-10-29 16:59:46 -0700 |
| commit | c8452b274087624140cb7f2424b321de54fcb41a (patch) | |
| tree | 6dd73ee0dc98d9c6997e39b6e109a1d5e4c02a74 /Test/dafny1/Induction.dfy | |
| parent | e7bf7ffb17f0c4022c3df81b4fe33df440723c37 (diff) | |
Dafny induction:
* implemented induction tactic for result-less, non-mutating ghost methods
* refine heuristics for determining if a variables is usefully passed to a recursive function
* disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy)
* added command-line flags /induction and /inductionHeuristic (everything is on by default)
Diffstat (limited to 'Test/dafny1/Induction.dfy')
| -rw-r--r-- | Test/dafny1/Induction.dfy | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 15cc1ffe..3585dde6 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -56,6 +56,23 @@ class IntegerInduction { {
}
+ // The following two ghost methods are the same as the previous two, but
+ // here no body is given--and the proof still goes through (thanks to
+ // Dafny's ghost-method induction tactic).
+
+ ghost method Lemma_Auto(n: int)
+ requires 0 <= n;
+ ensures 2 * Gauss(n) == n*(n+1);
+ {
+ }
+
+ ghost method Theorem1_Auto(n: int)
+ requires 0 <= n;
+ ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
+ ensures 2 * Gauss(n) == n*(n+1);
+ {
+ }
+
// Here is another proof. It makes use of Dafny's induction heuristics to
// prove the lemma.
|