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 | 9c332a2e3580d05b1557fa4548901d8df4b423a1 (patch) | |
| tree | 74ab8075f78680943a6ed2762e97261c95d6cd3e /Test/dafny0/CoPredicates.dfy | |
| parent | 3cfc61ac1212e28136a10f35ac1b1e8de743e7d2 (diff) | |
Dafny: More work on the coinduction principle
Diffstat (limited to 'Test/dafny0/CoPredicates.dfy')
| -rw-r--r-- | Test/dafny0/CoPredicates.dfy | 48 |
1 files changed, 48 insertions, 0 deletions
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
+}
|