From 1885f7d7d1fb9bd6ceb8220450dbb5d890501337 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 2 Oct 2015 15:26:56 -0700 Subject: Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/lemmas (this fixes an item from the wishlist). Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?). Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1]. --- Test/dafny0/CoinductiveProofs.dfy | 61 ++++++++++++++++++++++++++++-- Test/dafny0/CoinductiveProofs.dfy.expect | 65 ++++++++++++++++++++++---------- 2 files changed, 103 insertions(+), 23 deletions(-) (limited to 'Test/dafny0') diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy index d990ae51..0dce8af9 100644 --- a/Test/dafny0/CoinductiveProofs.dfy +++ b/Test/dafny0/CoinductiveProofs.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /rewriteFocalPredicates:1 "%s" > "%t" // RUN: %diff "%s.expect" "%t" codatatype Stream = Cons(head: T, tail: Stream) @@ -12,6 +12,7 @@ copredicate Pos(s: Stream) { 0 < s.head && Pos(s.tail) } +predicate FullPos(s: Stream) { Pos(s) } // a way in the test file to sidestep focal-predicate rewrites colemma {:induction false} PosLemma0(n: int) requires 1 <= n; @@ -26,7 +27,25 @@ colemma {:induction false} PosLemma1(n: int) { PosLemma1(n + 1); if (*) { - assert Pos(Upward(n + 1)); // error: cannot conclude this here, because we only have prefix predicates + assert FullPos(Upward(n + 1)); // error: cannot conclude this here, because we only have prefix predicates + } +} + +colemma {:induction false} PosLemma2(n: int) + requires 1 <= n; + ensures Pos(Upward(n)); +{ + PosLemma2(n + 1); + if (*) { + assert Pos(Upward(n + 1)); // Pos gets rewritten to Pos#[_k-1], which does hold + } else if (*) { + assert Pos#[_k-1](Upward(n + 1)); // explicitly saying Pos#[_k-1] also holds + } else if (*) { + assert Pos#[_k](Upward(n + 1)); // error: this is not known to hold for _k and n+1 + } else if (*) { + assert Pos#[_k](Upward(n)); // but it does hold with Pos#[_k] and n (which is the postcondition of the prefix lemma) + } else if (*) { + assert Pos#[_k+1](Upward(n)); // error: this is too much to ask for } } @@ -65,13 +84,29 @@ colemma {:induction false} AlwaysLemma_X1(s: Stream) { AlwaysLemma_X1(s); // this is the right proof } +predicate FullX(s: Stream) { X(s) } // a way in the test file to sidestep focal-predicate rewrites colemma {:induction false} AlwaysLemma_X2(s: Stream) ensures X(s); { AlwaysLemma_X2(s); if (*) { - assert X(s); // error: cannot conclude the full predicate here + assert FullX(s); // error: cannot conclude the full predicate here + } +} + +colemma {:induction false} AlwaysLemma_X3(s: Stream) + ensures X(s); +{ + AlwaysLemma_X3(s); + if (*) { + assert X(s); // holds, because it gets rewritten to X#[_k-1] + } else if (*) { + assert X#[_k-1](s); // explicitly saying X#[_k-1] also holds + } else if (*) { + assert X#[_k](s); // in fact, X#[_k] holds, too (which is the postcondition of the prefix lemma) + } else if (*) { + assert X#[_k+1](s); // as it turns out, this holds too, since the definition of X makes X#[_k+1] equal X#[_k] } } @@ -79,6 +114,7 @@ copredicate Y(s: Stream) // this is equivalent to always returning 'true' { Y(s.tail) } +predicate FullY(s: Stream) { Y(s) } // a way in the test file to sidestep focal-predicate rewrites colemma {:induction false} AlwaysLemma_Y0(s: Stream) ensures Y(s); // prove that Y(s) really is always 'true' @@ -97,7 +133,24 @@ colemma {:induction false} AlwaysLemma_Y2(s: Stream) { AlwaysLemma_Y2(s.tail); if (*) { - assert Y(s.tail); // error: not provable here + assert FullY(s.tail); // error: not provable here + } +} + +colemma {:induction false} AlwaysLemma_Y3(s: Stream) + ensures Y(s); +{ + AlwaysLemma_Y3(s.tail); + if (*) { + assert Y(s.tail); // this holds, because it's rewritten to Y#[_k-1] + } else if (*) { + assert Y#[_k-1](s.tail); + } else if (*) { + assert Y#[_k](s.tail); // error: not known to hold for _k and s.tail + } else if (*) { + assert Y#[_k](s); // this is also the postcondition of the prefix lemma + } else if (*) { + assert Y#[_k+1](s); // error: this is too much to ask for } } diff --git a/Test/dafny0/CoinductiveProofs.dfy.expect b/Test/dafny0/CoinductiveProofs.dfy.expect index 2a5a2b0b..c4f4c405 100644 --- a/Test/dafny0/CoinductiveProofs.dfy.expect +++ b/Test/dafny0/CoinductiveProofs.dfy.expect @@ -1,50 +1,77 @@ -CoinductiveProofs.dfy(29,11): Error: assertion violation +CoinductiveProofs.dfy(30,11): Error: assertion violation +CoinductiveProofs.dfy(15,36): Related location CoinductiveProofs.dfy(13,16): Related location Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then -CoinductiveProofs.dfy(59,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(58,10): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(54,2): Related location +CoinductiveProofs.dfy(44,11): Error: assertion violation +CoinductiveProofs.dfy(13,16): Related location +Execution trace: + (0,0): anon0 + (0,0): anon13_Then + (0,0): anon16_Then +CoinductiveProofs.dfy(48,11): Error: assertion violation +CoinductiveProofs.dfy(13,16): Related location +Execution trace: + (0,0): anon0 + (0,0): anon13_Then + (0,0): anon18_Then +CoinductiveProofs.dfy(78,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(77,10): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(73,2): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(74,11): Error: assertion violation -CoinductiveProofs.dfy(54,2): Related location +CoinductiveProofs.dfy(94,11): Error: assertion violation +CoinductiveProofs.dfy(87,29): Related location +CoinductiveProofs.dfy(73,2): Related location Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then -CoinductiveProofs.dfy(91,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(90,10): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(80,2): Related location +CoinductiveProofs.dfy(127,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(126,10): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(115,2): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(100,11): Error: assertion violation -CoinductiveProofs.dfy(80,2): Related location +CoinductiveProofs.dfy(136,11): Error: assertion violation +CoinductiveProofs.dfy(117,29): Related location +CoinductiveProofs.dfy(115,2): Related location Execution trace: (0,0): anon0 (0,0): anon5_Then (0,0): anon6_Then -CoinductiveProofs.dfy(111,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(110,10): Related location: This is the postcondition that might not hold. -CoinductiveProofs.dfy(106,2): Related location +CoinductiveProofs.dfy(149,11): Error: assertion violation +CoinductiveProofs.dfy(115,2): Related location +Execution trace: + (0,0): anon0 + (0,0): anon13_Then + (0,0): anon16_Then +CoinductiveProofs.dfy(153,11): Error: assertion violation +CoinductiveProofs.dfy(115,2): Related location +Execution trace: + (0,0): anon0 + (0,0): anon13_Then + (0,0): anon18_Then +CoinductiveProofs.dfy(164,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(163,10): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(159,2): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(150,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(149,21): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(203,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(202,21): Related location: This is the postcondition that might not hold. CoinductiveProofs.dfy(4,23): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -CoinductiveProofs.dfy(156,0): Error BP5003: A postcondition might not hold on this return path. -CoinductiveProofs.dfy(155,21): Related location: This is the postcondition that might not hold. +CoinductiveProofs.dfy(209,0): Error BP5003: A postcondition might not hold on this return path. +CoinductiveProofs.dfy(208,21): Related location: This is the postcondition that might not hold. CoinductiveProofs.dfy(4,23): Related location Execution trace: (0,0): anon0 (0,0): anon3_Then -Dafny program verifier finished with 35 verified, 8 errors +Dafny program verifier finished with 42 verified, 12 errors -- cgit v1.2.3