diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-11-03 18:14:16 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-11-03 18:14:16 -0700 |
| commit | d3491c3581c9e146116417d15b753b1fa65240cc (patch) | |
| tree | 31037941ca84734f4a838325506c0eb6a4bade0f /Test/dafny1/MoreInduction.dfy | |
| parent | c8452b274087624140cb7f2424b321de54fcb41a (diff) | |
Added some Dafny and Boogie test cases, including Turing's factorial program, Hoare's classic FIND, and some induction tests for negative integers
Diffstat (limited to 'Test/dafny1/MoreInduction.dfy')
| -rw-r--r-- | Test/dafny1/MoreInduction.dfy | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy index efba0963..84c32fb3 100644 --- a/Test/dafny1/MoreInduction.dfy +++ b/Test/dafny1/MoreInduction.dfy @@ -61,3 +61,37 @@ ghost method Lemma<X>(list: List<X>, ext: List<X>) }
}
}
+
+// ---------------------------------------------
+
+function NegFac(n: int): int
+ decreases -n;
+{
+ if -1 <= n then -1 else - NegFac(n+1) * n
+}
+
+ghost method LemmaAll()
+ ensures forall n :: NegFac(n) <= -1; // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
+{
+}
+
+ghost method LemmaOne(n: int)
+ ensures NegFac(n) <= -1; // error: induction heuristic does not give a useful well-founded order, and thus this fails to verify
+{
+}
+
+ghost method LemmaAll_Neg()
+ ensures forall n :: NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
+{
+}
+
+ghost method LemmaOne_Neg(n: int)
+ ensures NegFac(-n) <= -1; // error: fails to verify because of the minus in the trigger
+{
+}
+
+ghost method LemmaOneWithDecreases(n: int)
+ ensures NegFac(n) <= -1; // here, the programmer gives a good well-founded order, so this verifies
+ decreases -n;
+{
+}
|