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 | |
| 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')
| -rw-r--r-- | Test/dafny1/Answer | 20 | ||||
| -rw-r--r-- | Test/dafny1/MoreInduction.dfy | 34 |
2 files changed, 52 insertions, 2 deletions
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer index d53ae14b..ab10d944 100644 --- a/Test/dafny1/Answer +++ b/Test/dafny1/Answer @@ -88,8 +88,24 @@ Dafny program verifier finished with 33 verified, 0 errors Dafny program verifier finished with 141 verified, 0 errors
-------------------- MoreInduction.dfy --------------------
-
-Dafny program verifier finished with 8 verified, 0 errors
+MoreInduction.dfy(75,1): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(74,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+MoreInduction.dfy(80,1): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(79,21): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+MoreInduction.dfy(85,1): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(84,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+MoreInduction.dfy(90,1): Error BP5003: A postcondition might not hold on this return path.
+MoreInduction.dfy(89,22): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 15 verified, 4 errors
-------------------- Celebrity.dfy --------------------
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;
+{
+}
|