From b0b61083adb4b427974c772658cdc744da23f42b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 4 Dec 2012 17:30:00 -0800 Subject: 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.) --- Test/dafny0/Answer | 28 +++++++--- Test/dafny0/CoPrefix.dfy | 115 ++++++++++++++++++++++++++++++++++++++ Test/dafny0/CoResolution.dfy | 43 ++++++++++++++ Test/dafny0/CoinductiveProofs.dfy | 6 +- Test/dafny0/runtest.bat | 2 +- 5 files changed, 182 insertions(+), 12 deletions(-) create mode 100644 Test/dafny0/CoPrefix.dfy create mode 100644 Test/dafny0/CoResolution.dfy (limited to 'Test/dafny0') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 072339b3..97e7c870 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1342,17 +1342,31 @@ CoResolution.dfy(41,9): Error: a call to a prefix predicate/method in this conte CoResolution.dfy(42,4): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign) 13 resolution/type errors detected in CoResolution.dfy +-------------------- CoPrefix.dfy -------------------- +CoPrefix.dfy(61,7): Error: failure to decrease termination measure +Execution trace: + (0,0): anon0 + (0,0): anon5_Else + (0,0): anon6_Then +CoPrefix.dfy(74,7): Error: failure to decrease termination measure +Execution trace: + (0,0): anon0 + (0,0): anon5_Else + (0,0): anon6_Then +CoPrefix.dfy(114,1): Error BP5003: A postcondition might not hold on this return path. +CoPrefix.dfy(113,11): Related location: This is the postcondition that might not hold. +CoPrefix.dfy(101,17): Related location: Related location +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 17 verified, 3 errors + -------------------- CoinductiveProofs.dfy -------------------- CoinductiveProofs.dfy(26,12): Error: assertion violation CoinductiveProofs.dfy(10,17): Related location: Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(33,1): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(32,11): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(10,17): Related location: Related location -Execution trace: - (0,0): anon0 CoinductiveProofs.dfy(56,1): Error BP5003: A postcondition might not hold on this return path. CoinductiveProofs.dfy(55,11): Related location: This is the postcondition that might not hold. CoinductiveProofs.dfy(51,3): Related location: Related location @@ -1380,16 +1394,14 @@ Execution trace: (0,0): anon0 CoinductiveProofs.dfy(147,1): Error BP5003: A postcondition might not hold on this return path. CoinductiveProofs.dfy(146,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(1,24): Related location: Related location Execution trace: (0,0): anon0 CoinductiveProofs.dfy(153,1): Error BP5003: A postcondition might not hold on this return path. CoinductiveProofs.dfy(152,22): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(1,24): Related location: Related location Execution trace: (0,0): anon0 -Dafny program verifier finished with 31 verified, 9 errors +Dafny program verifier finished with 32 verified, 8 errors -------------------- TypeAntecedents.dfy -------------------- TypeAntecedents.dfy(32,13): Error: assertion violation 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 +} diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy new file mode 100644 index 00000000..233a818b --- /dev/null +++ b/Test/dafny0/CoResolution.dfy @@ -0,0 +1,43 @@ +copredicate P(b: bool) +{ + !b && Q(null) +} + +copredicate Q(a: array) +{ + a == null && P(true) +} + +//copredicate A() { B() } +//predicate B() { A() } // error: SCC of a copredicate must include only copredicates + +copredicate D() + reads this; // error: copredicates are not allowed to have a reads clause -- WHY NOT? +{ + true +} + +copredicate S(d: set) +{ + this.S#(d) && // error: the call to S# must give an explicit depth argument + S#(d) && // error: the call to S# must give an explicit depth argument + this.Undeclared#(d) && // error: 'Undeclared#' is undeclared, and depth argument is left implicit + this.Undeclared#[5](d) && // error: 'Undeclared#' is undeclared + Undeclared#(d) && // error: 'Undeclared#' is undeclared, and depth argument is left implicit + Undeclared#[5](d) && // error: 'Undeclared#' is undeclared + this.S#[5](d) && + S#[5](d) && + S#(5, d) && // error: the '5' here does not give the depth argument + S#[_k](d) // error: _k is not an identifier in scope +} + +comethod CM(d: set) +{ + var b; + b := this.S#[5](d) && this.S#(d + d); // error: cannot rely on implicit depth argument here + b := S#[5](d) && S#(d + d); // error: cannot rely on implicit depth argument here + this.CM#[5](d); + CM#[5](d); + this.CM#(d + d); // error: must give an explicit depth argument + CM#(d + d); // error: must give an explicit depth argument +} diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy index c56f9b36..ddb23b5b 100644 --- a/Test/dafny0/CoinductiveProofs.dfy +++ b/Test/dafny0/CoinductiveProofs.dfy @@ -23,18 +23,18 @@ comethod PosLemma1(n: int) { PosLemma1(n + 1); if (*) { - assert Pos(Upward(n + 1)); // error: cannot conclude this here, because we only have a certificate + assert Pos(Upward(n + 1)); // error: cannot conclude this here, because we only have prefix predicates } } comethod Outside_CoMethod_Caller_PosLemma(n: int) requires 1 <= n; ensures Pos(Upward(n)); -{ // error: this comethod is supposed to produce a certificate, but instead it establishes the real deal - // (which currently produces a complaint from Dafny) +{ assert Upward(n).tail == Upward(n + 1); // follows from one unrolling of the definition of Upward PosLemma0(n + 1); assert Pos(Upward(n+1)); // this follows directly from the previous line, because it isn't a recursive call + // ... and it implies the prefix predicate we're supposed to establish } method Outside_Method_Caller_PosLemma(n: int) diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index fd5349f4..82d4bebd 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -18,7 +18,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy TypeParameters.dfy Datatypes.dfy Coinductive.dfy Corecursion.dfy CoResolution.dfy - CoinductiveProofs.dfy + CoPrefix.dfy CoinductiveProofs.dfy TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy LoopModifies.dfy Refinement.dfy RefinementErrors.dfy ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy -- cgit v1.2.3