diff options
| -rw-r--r-- | Source/Dafny/Cloner.cs | 91 | ||||
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 27 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 16 | ||||
| -rw-r--r-- | Test/dafny0/CoinductiveProofs.dfy | 61 | ||||
| -rw-r--r-- | Test/dafny0/CoinductiveProofs.dfy.expect | 65 | ||||
| -rw-r--r-- | Test/wishlist/tooltips-on-inductive-lemmas.dfy | 12 | ||||
| -rw-r--r-- | Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect | 7 |
7 files changed, 214 insertions, 65 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index c94c697d..45d8a2c9 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -715,7 +715,7 @@ namespace Microsoft.Dafny {
protected readonly Expression k;
protected readonly ErrorReporter reporter;
- readonly string suffix;
+ protected readonly string suffix;
protected FixpointCloner(Expression k, ErrorReporter reporter)
{
Contract.Requires(k != null);
@@ -724,6 +724,18 @@ namespace Microsoft.Dafny this.reporter = reporter;
this.suffix = string.Format("#[{0}]", Printer.ExprToString(k));
}
+ protected Expression CloneCallAndAddK(FunctionCallExpr e) {
+ Contract.Requires(e != null);
+ var receiver = CloneExpr(e.Receiver);
+ var args = new List<Expression>();
+ args.Add(k);
+ foreach (var arg in e.Args) {
+ args.Add(CloneExpr(arg));
+ }
+ var fexp = new FunctionCallExpr(Tok(e.tok), e.Name + "#", receiver, e.OpenParen, args);
+ reporter.Info(MessageSource.Cloner, e.tok, e.Name + suffix);
+ return fexp;
+ }
}
/// <summary>
@@ -733,6 +745,7 @@ namespace Microsoft.Dafny /// precondition (resp. postcondition) of the inductive lemma's (resp. colemma's) corresponding prefix lemma.
/// It is assumed that the source expression has been resolved. Note, the "k" given to the constructor
/// is not cloned with each use; it is simply used as is.
+ /// The resulting expression needs to be resolved by the caller.
/// </summary>
class FixpointLemmaSpecificationSubstituter : FixpointCloner
{
@@ -756,15 +769,7 @@ namespace Microsoft.Dafny } else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
if (friendlyCalls.Contains(e)) {
- var receiver = CloneExpr(e.Receiver);
- var args = new List<Expression>();
- args.Add(k);
- foreach (var arg in e.Args) {
- args.Add(CloneExpr(arg));
- }
- var fexp = new FunctionCallExpr(Tok(e.tok), e.Name + "#", receiver, e.OpenParen, args);
- reporter.Info(MessageSource.Cloner, e.tok, e.Name);
- return fexp;
+ return CloneCallAndAddK(e);
}
} else if (expr is BinaryExpr && isCoContext) {
var e = (BinaryExpr)expr;
@@ -774,7 +779,7 @@ namespace Microsoft.Dafny var B = CloneExpr(e.E1);
var teq = new TernaryExpr(Tok(e.tok), op, k, A, B);
var opString = op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!=";
- reporter.Info(MessageSource.Cloner, e.tok, opString);
+ reporter.Info(MessageSource.Cloner, e.tok, opString + suffix);
return teq;
}
}
@@ -803,19 +808,77 @@ namespace Microsoft.Dafny }
/// <summary>
- /// The task of the FixpointLemmaBodyCloner is to fill in the implicit _k-1 arguments in recursive inductive/co-lemma calls.
+ /// The task of the FixpointLemmaBodyCloner is to fill in the implicit _k-1 arguments in recursive inductive/co-lemma calls
+ /// and in calls to the focal predicates.
/// The source statement and the given "k" are assumed to have been resolved.
/// </summary>
class FixpointLemmaBodyCloner : FixpointCloner
{
readonly FixpointLemma context;
- public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, ErrorReporter reporter)
+ readonly ISet<FixpointPredicate> focalPredicates;
+ public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, ISet<FixpointPredicate> focalPredicates, ErrorReporter reporter)
: base(k, reporter)
{
Contract.Requires(context != null);
Contract.Requires(k != null);
Contract.Requires(reporter != null);
this.context = context;
+ this.focalPredicates = focalPredicates;
+ }
+ public override Expression CloneExpr(Expression expr) {
+ if (DafnyOptions.O.RewriteFocalPredicates) {
+ if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+#if DEBUG_PRINT
+ if (e.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => e.Function.Name == p.Name + "#")) {
+ Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e));
+ }
+#endif
+ // Note, we don't actually ever get here, because all calls will have been parsed as ApplySuffix.
+ // However, if something changes in the future (for example, some rewrite that changing an ApplySuffix
+ // to its resolved FunctionCallExpr), then we do want this code, so with the hope of preventing
+ // some error in the future, this case is included. (Of course, it is currently completely untested!)
+ var f = e.Function as FixpointPredicate;
+ if (f != null && focalPredicates.Contains(f)) {
+#if DEBUG_PRINT
+ var r = CloneCallAndAddK(e);
+ Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r));
+ return r;
+#else
+ return CloneCallAndAddK(e);
+#endif
+ }
+ } else if (expr is ApplySuffix) {
+ var apply = (ApplySuffix)expr;
+ if (!apply.WasResolved()) {
+ // Since we're assuming the enclosing statement to have been resolved, this ApplySuffix must
+ // be part of an ExprRhs that actually designates a method call. Such an ApplySuffix does
+ // not get listed as being resolved, but its components (like its .Lhs) are resolved.
+ var mse = (MemberSelectExpr)apply.Lhs.Resolved;
+ Contract.Assume(mse.Member is Method);
+ } else {
+ var fce = apply.Resolved as FunctionCallExpr;
+ if (fce != null) {
+#if DEBUG_PRINT
+ if (fce.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => fce.Function.Name == p.Name + "#")) {
+ Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce));
+ }
+#endif
+ var f = fce.Function as FixpointPredicate;
+ if (f != null && focalPredicates.Contains(f)) {
+#if DEBUG_PRINT
+ var r = CloneCallAndAddK(fce);
+ Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r));
+ return r;
+#else
+ return CloneCallAndAddK(fce);
+#endif
+ }
+ }
+ }
+ }
+ }
+ return base.CloneExpr(expr);
}
public override AssignmentRhs CloneRHS(AssignmentRhs rhs) {
var r = rhs as ExprRhs;
@@ -839,7 +902,7 @@ namespace Microsoft.Dafny apply.Args.ForEach(arg => args.Add(CloneExpr(arg)));
var applyClone = new ApplySuffix(Tok(apply.tok), lhsClone, args);
var c = new ExprRhs(applyClone);
- reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name);
+ reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name + suffix);
return c;
}
}
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 59d0eb2c..2d8756d2 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -65,11 +65,12 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; - public bool AutoTriggers = false; + public bool AutoTriggers = false;
+ public bool RewriteFocalPredicates = false;
public bool PrintTooltips = false; public bool PrintStats = false; public bool PrintFunctionCallGraph = false; - public bool WarnShadowing = false; + public bool WarnShadowing = false;
public bool IronDafny = #if ENABLE_IRONDAFNY true @@ -216,12 +217,20 @@ namespace Microsoft.Dafny case "printTooltips": PrintTooltips = true; - return true; + return true;
+
+ case "autoTriggers": {
+ int autoTriggers = 0;
+ if (ps.GetNumericArgument(ref autoTriggers, 2)) {
+ AutoTriggers = autoTriggers == 1;
+ }
+ return true;
+ } - case "autoTriggers": { - int autoTriggers = 0; - if (ps.GetNumericArgument(ref autoTriggers, 2)) { - AutoTriggers = autoTriggers == 1; + case "rewriteFocalPredicates": {
+ int rewriteFocalPredicates = 0;
+ if (ps.GetNumericArgument(ref rewriteFocalPredicates, 2)) {
+ RewriteFocalPredicates = rewriteFocalPredicates == 1; } return true; } @@ -369,6 +378,10 @@ namespace Microsoft.Dafny 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. 1 - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. + /rewriteFocalPredicates:<n> + 0 (default) - Don't rewrite predicates in the body of prefix lemmas. + 1 - In the body of prefix lemmas, rewrite any use of a focal predicate + P to P#[_k-1]. /optimize Produce optimized C# code, meaning: - selects optimized C# prelude by passing /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 36464925..7a540722 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1565,6 +1565,7 @@ namespace Microsoft.Dafny continue; // something went wrong during registration of the prefix lemma (probably a duplicated fixpoint-lemma name)
}
var k = prefixLemma.Ins[0];
+ var focalPredicates = new HashSet<FixpointPredicate>();
if (com is CoLemma) {
// compute the postconditions of the prefix lemma
Contract.Assume(prefixLemma.Ens.Count == 0); // these are not supposed to have been filled in before
@@ -1574,6 +1575,12 @@ namespace Microsoft.Dafny var subst = new FixpointLemmaSpecificationSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this.reporter, true);
var post = subst.CloneExpr(p.E);
prefixLemma.Ens.Add(new MaybeFreeExpression(post, p.IsFree));
+ foreach (var e in coConclusions) {
+ var fce = e as FunctionCallExpr;
+ if (fce != null) { // the other possibility is that "e" is a BinaryExpr
+ focalPredicates.Add((CoPredicate)fce.Function);
+ }
+ }
}
} else {
// compute the preconditions of the prefix lemma
@@ -1584,13 +1591,18 @@ namespace Microsoft.Dafny var subst = new FixpointLemmaSpecificationSubstituter(antecedents, new IdentifierExpr(k.tok, k.Name), this.reporter, false);
var pre = subst.CloneExpr(p.E);
prefixLemma.Req.Add(new MaybeFreeExpression(pre, p.IsFree));
+ foreach (var e in antecedents) {
+ var fce = (FunctionCallExpr)e; // we expect "antecedents" to contain only FunctionCallExpr's
+ focalPredicates.Add((InductivePredicate)fce.Function);
+ }
}
}
+ reporter.Info(MessageSource.Resolver, com.tok, string.Format("{0} specialized for {1}", com.PrefixLemma.Name, Util.Comma(focalPredicates, p => p.Name)));
// Compute the statement body of the prefix lemma
Contract.Assume(prefixLemma.Body == null); // this is not supposed to have been filled in before
if (com.Body != null) {
var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1));
- var subst = new FixpointLemmaBodyCloner(com, kMinusOne, this.reporter);
+ var subst = new FixpointLemmaBodyCloner(com, kMinusOne, focalPredicates, this.reporter);
var mainBody = subst.CloneBlockStmt(com.Body);
var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name));
var condBody = new IfStmt(com.BodyStartTok, mainBody.EndTok, kPositive, mainBody, null);
@@ -3571,7 +3583,7 @@ namespace Microsoft.Dafny var substituter = new Translator.AlphaConverting_Substituter(cs.Receiver, argsSubstMap, new Dictionary<TypeParameter, Type>(), new Translator(resolver.reporter));
foreach (var ens in cs.Method.Ens) {
var p = substituter.Substitute(ens.E); // substitute the call's actuals for the method's formals
- resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(p) + ";");
+ resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(p));
}
}
}
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<T> = Cons(head: T, tail: Stream)
@@ -12,6 +12,7 @@ copredicate Pos(s: Stream<int>) {
0 < s.head && Pos(s.tail)
}
+predicate FullPos(s: Stream<int>) { 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
diff --git a/Test/wishlist/tooltips-on-inductive-lemmas.dfy b/Test/wishlist/tooltips-on-inductive-lemmas.dfy deleted file mode 100644 index 1bd25437..00000000 --- a/Test/wishlist/tooltips-on-inductive-lemmas.dfy +++ /dev/null @@ -1,12 +0,0 @@ -// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-inductive lemma P()
- requires Q() { // WISH the tooltip for this was broken at some point between
- // revisions 94ee216fe0cd (1179) and bd779dda3b3d (1785)
- P();
-}
-
-inductive predicate Q() {
- Q()
-}
diff --git a/Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect b/Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect deleted file mode 100644 index 4d036eef..00000000 --- a/Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect +++ /dev/null @@ -1,7 +0,0 @@ -tooltips-on-inductive-lemmas.dfy(5,11): Info: Q
-tooltips-on-inductive-lemmas.dfy(7,2): Info: P
-tooltips-on-inductive-lemmas.dfy(11,2): Info: Q#[_k - 1]
-tooltips-on-inductive-lemmas.dfy(4,16): Info: P# {:induction _k}
-tooltips-on-inductive-lemmas.dfy(4,16): Info: P# decreases _k
-
-Dafny program verifier finished with 3 verified, 0 errors
|