diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-12-04 17:30:00 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-12-04 17:30:00 -0800 |
| commit | b0b61083adb4b427974c772658cdc744da23f42b (patch) | |
| tree | ca08e2f2f4d9b62583177e8a0a0691eb8f353dee /Test/dafny0/CoPrefix.dfy | |
| parent | 8eb077dfd8515f26dc58754334d52f9c44a73e0c (diff) | |
Support for copredicates and prefix predicates in comethods.
(Missing from the co support are (prefix) equalities of codatatypes,
various restrictions on the use of co/prefix-predicates, and tactic
support for applying the (prefix-)induction automatically.)
Diffstat (limited to 'Test/dafny0/CoPrefix.dfy')
| -rw-r--r-- | Test/dafny0/CoPrefix.dfy | 115 |
1 files changed, 115 insertions, 0 deletions
diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy new file mode 100644 index 00000000..09dd2cc5 --- /dev/null +++ b/Test/dafny0/CoPrefix.dfy @@ -0,0 +1,115 @@ +// ----- Stream
+
+codatatype Stream = Nil | Cons(head: int, tail: Stream);
+
+function append(M: Stream, N: Stream): Stream
+{
+ match M
+ case Nil => N
+ case Cons(t, M') => Cons(t, append(M', N))
+}
+
+function zeros(): Stream
+{
+ Cons(0, zeros())
+}
+
+function ones(): Stream
+{
+ Cons(1, ones())
+}
+
+copredicate atmost(a: Stream, b: Stream)
+{
+ match a
+ case Nil => true
+ case Cons(h,t) => b.Cons? && h <= b.head && atmost(t, b.tail)
+}
+
+comethod Theorem0()
+ ensures atmost(zeros(), ones());
+{
+ // the following shows two equivalent ways to getting essentially the
+ // co-inductive hypothesis
+ if (*) {
+ Theorem0#[_k-1]();
+ } else {
+ Theorem0();
+ }
+}
+
+ghost method Theorem0_Manual()
+ ensures atmost(zeros(), ones());
+{
+ parallel (k: nat) {
+ Theorem0_Lemma(k);
+ }
+ assume (forall k: nat :: atmost#[k](zeros(), ones())) ==> atmost(zeros(), ones());
+}
+
+datatype Natural = Zero | Succ(Natural);
+
+comethod Theorem0_TerminationFailure_ExplicitDecreases(y: Natural)
+ ensures atmost(zeros(), ones());
+ decreases y;
+{
+ match (y) {
+ case Succ(x) =>
+ // this is just to show that the decreases clause does kick in
+ Theorem0_TerminationFailure_ExplicitDecreases#[_k](x);
+ case Zero =>
+ Theorem0_TerminationFailure_ExplicitDecreases#[_k](y); // error: failure to terminate
+ }
+ Theorem0_TerminationFailure_ExplicitDecreases#[_k-1](y);
+}
+
+comethod Theorem0_TerminationFailure_DefaultDecreases(y: Natural)
+ ensures atmost(zeros(), ones());
+{
+ match (y) {
+ case Succ(yy) =>
+ // this is just to show that the decreases clause does kick in
+ Theorem0_TerminationFailure_DefaultDecreases#[_k](yy);
+ case Zero =>
+ Theorem0_TerminationFailure_DefaultDecreases#[_k](y); // error: failure to terminate
+ }
+ Theorem0_TerminationFailure_DefaultDecreases#[_k-1](y);
+}
+
+ghost method {:induction true} Theorem0_Lemma(k: nat)
+ ensures atmost#[k](zeros(), ones());
+{
+}
+
+/** SOON
+comethod Theorem1()
+ ensures append(zeros(), ones()) == zeros();
+{
+ Theorem1();
+}
+** SOON */
+
+codatatype IList = ICons(head: int, tail: IList);
+
+function UpIList(n: int): IList
+{
+ ICons(n, UpIList(n+1))
+}
+
+copredicate Pos(s: IList)
+{
+ s.head > 0 && Pos(s.tail)
+}
+
+comethod Theorem2(n: int)
+ requires 1 <= n;
+ ensures Pos(UpIList(n));
+{
+ Theorem2(n+1);
+}
+
+comethod Theorem2_NotAProof(n: int)
+ requires 1 <= n;
+ ensures Pos(UpIList(n));
+{ // error: this is not a proof
+}
|