diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-07-09 22:12:23 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-07-09 22:12:23 -0700 |
| commit | ff77f212d935859502939249c5a1596790c61a87 (patch) | |
| tree | 220794d5619ec6dfbdbc6e43d1a9a36cd677398a /Test | |
| parent | e6c93427a01f67a780c4227a27cddd5d38a9672d (diff) | |
Dafny: More work on the coinduction principle
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 9 | ||||
| -rw-r--r-- | Test/dafny0/CoPredicates.dfy | 48 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 3 |
3 files changed, 59 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7879483d..e1ab158f 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1289,6 +1289,15 @@ Execution trace: Dafny program verifier finished with 5 verified, 2 errors
+-------------------- CoPredicates.dfy --------------------
+CoPredicates.dfy(35,1): Error BP5003: A postcondition might not hold on this return path.
+CoPredicates.dfy(34,11): Related location: This is the postcondition that might not hold.
+CoPredicates.dfy(20,22): Related location: Related location
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 11 verified, 1 error
+
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(32,13): Error: assertion violation
Execution trace:
diff --git a/Test/dafny0/CoPredicates.dfy b/Test/dafny0/CoPredicates.dfy new file mode 100644 index 00000000..b4da4792 --- /dev/null +++ b/Test/dafny0/CoPredicates.dfy @@ -0,0 +1,48 @@ +codatatype Stream<T> = Cons(head: T, tail: Stream);
+
+function Upward(n: int): Stream<int>
+{
+ Cons(n, Upward(n + 1))
+}
+
+copredicate Pos(s: Stream<int>)
+{
+ 0 < s.head && Pos(s.tail)
+}
+
+function Doubles(n: int): Stream<int>
+{
+ Cons(2*n, Doubles(n + 1))
+}
+
+copredicate Even(s: Stream<int>)
+{
+ s.head % 2 == 0 && Even(s.tail)
+}
+
+ghost method Lemma0(n: int)
+ ensures Even(Doubles(n));
+{
+}
+
+function UpwardBy2(n: int): Stream<int>
+{
+ Cons(n, UpwardBy2(n + 2))
+}
+
+ghost method Lemma1(n: int)
+ ensures Even(UpwardBy2(2*n)); // error: this is true, but Dafny can't prove it
+{
+}
+
+function U2(n: int): Stream<int>
+ requires n % 2 == 0;
+{
+ UpwardBy2(n)
+}
+
+ghost method Lemma2(n: int)
+ ensures Even(UpwardBy2(2*n)); // this is true, but Dafny can't prove it
+{
+ assert Even(U2(2*n)); // ... thanks to this lemma
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index d352cf44..60b544c7 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -16,7 +16,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy ModulesCycle.dfy Modules0.dfy Modules1.dfy BadFunction.dfy
Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
- TypeParameters.dfy Datatypes.dfy Coinductive.dfy Corecursion.dfy
+ TypeParameters.dfy Datatypes.dfy
+ Coinductive.dfy Corecursion.dfy CoPredicates.dfy
TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy
LoopModifies.dfy Refinement.dfy RefinementErrors.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
|