summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-10-29 16:59:46 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-10-29 16:59:46 -0700
commitc8452b274087624140cb7f2424b321de54fcb41a (patch)
tree6dd73ee0dc98d9c6997e39b6e109a1d5e4c02a74
parente7bf7ffb17f0c4022c3df81b4fe33df440723c37 (diff)
Dafny induction:
* implemented induction tactic for result-less, non-mutating ghost methods * refine heuristics for determining if a variables is usefully passed to a recursive function * disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy) * added command-line flags /induction and /inductionHeuristic (everything is on by default)
Diffstat
-rw-r--r--Dafny/Compiler.cs10
-rw-r--r--Dafny/Dafny.atg1
-rw-r--r--Dafny/DafnyAst.cs19
-rw-r--r--Dafny/Parser.cs1
-rw-r--r--Dafny/Resolver.cs53
-rw-r--r--Dafny/Translator.cs555
-rw-r--r--Test/dafny0/Answer8
-rw-r--r--Test/dafny0/Parallel.dfy11
-rw-r--r--Test/dafny0/ParallelResolveErrors.dfy64
-rw-r--r--Test/dafny1/Answer4
-rw-r--r--Test/dafny1/Induction.dfy17
-rw-r--r--Test/dafny1/Rippling.dfy141
12 files changed, 671 insertions, 213 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 9938d30a..61b0398f 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -959,13 +959,9 @@ namespace Microsoft.Dafny {
// ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) ));
// }
Indent(indent + n * IndentAmount);
- wr.Write("if (");
- if (s.Range == null) {
- wr.Write("true");
- } else {
- TrExpr(s.Range);
- }
- wr.WriteLine(") {");
+ wr.Write("if ");
+ TrParenExpr(s.Range);
+ wr.WriteLine(" {");
Indent(indent + (n + 1) * IndentAmount);
wr.Write("{0}.Add(new System.Tuple<{1}>(", ingredients, tupleTypeArgs);
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 9de1421b..fa857aad 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -922,6 +922,7 @@ ParallelStmt<out Statement/*!*/ s>
"parallel" (. x = t; .)
"("
QuantifierDomain<out bvars, out attrs, out range>
+ (. if (range == null) { range = new LiteralExpr(x, true); } .)
")"
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 88862483..bf8eb6b0 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1040,6 +1040,19 @@ namespace Microsoft.Dafny {
}
}
+ /// <summary>
+ /// A "ThisSurrogate" is used during translation time to make the treatment of the receiver more similar to
+ /// the treatment of other in-parameters.
+ /// </summary>
+ public class ThisSurrogate : Formal
+ {
+ public ThisSurrogate(IToken tok, Type type)
+ : base(tok, "this", type, true, false) {
+ Contract.Requires(tok != null);
+ Contract.Requires(type != null);
+ }
+ }
+
public class BoundVar : NonglobalVariable {
public override bool IsMutable {
get {
@@ -2009,7 +2022,6 @@ namespace Microsoft.Dafny {
: base(tok) { // represents the Dafny literal "null"
Contract.Requires(tok != null);
this.Value = null;
-
}
public LiteralExpr(IToken tok, BigInteger n)
@@ -2018,7 +2030,6 @@ namespace Microsoft.Dafny {
Contract.Requires(0 <= n.Sign);
this.Value = n;
-
}
public LiteralExpr(IToken tok, int n) :base(tok){
@@ -2297,7 +2308,9 @@ namespace Microsoft.Dafny {
public override IEnumerable<Expression> SubExpressions {
get {
- yield return Receiver;
+ if (!Function.IsStatic) {
+ yield return Receiver;
+ }
foreach (var e in Args) {
yield return e;
}
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 57f4c46e..2fc50c37 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -1233,6 +1233,7 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t;
Expect(33);
QuantifierDomain(out bvars, out attrs, out range);
+ if (range == null) { range = new LiteralExpr(x, true); }
Expect(34);
while (la.kind == 29 || la.kind == 31) {
isFree = false;
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 5d806aa9..a4d99bd0 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -785,8 +785,36 @@ namespace Microsoft.Dafny {
ResolveAttributes(m.Attributes, false);
// ... continue resolving specification
+ bool twoState = true;
+ if (m.Mod.Count == 0 && m.Outs.Count == 0) {
+ // In this special case, the current translation of parallel Call statements would be unsound.
+ // The reason is that the parallel Call statement does not advance the heap, so there had better
+ // not be any way to say that the post-heap is definitely different than the pre-heap. For example,
+ // the following program, is permitted, would unsoundly verify:
+ // ghost static method M(y: int)
+ // ensures exists o: object :: o != null && fresh(o);
+ // {
+ // var p := new object;
+ // }
+ // method Main() {
+ // parallel (x) { M(x); }
+ // assert false;
+ // }
+ // In fact, here is another method M that together with Main above would yield unsound verification:
+ // class C { ghost var data: int; }
+ // ghost static method M(y: int)
+ // ensures exists c: C :: c != null && c.data != old(c.data);
+ // {
+ // var c := new C;
+ // c.data := c.data + 1;
+ // }
+ // So, it seems best just to disallow two-state postconditions in these cases. Perhaps the error
+ // message will not explain enough of the reasons for this restriction, but the restriction does
+ // not seem to rule out any useful programs.
+ twoState = false;
+ }
foreach (MaybeFreeExpression e in m.Ens) {
- ResolveExpression(e.E, true);
+ ResolveExpression(e.E, twoState);
Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(e.E.Type, Type.Bool)) {
Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type);
@@ -1490,15 +1518,13 @@ namespace Microsoft.Dafny {
}
ResolveType(v.tok, v.Type);
}
- if (s.Range != null) {
- ResolveExpression(s.Range, true);
- Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(s.Range.Type, Type.Bool)) {
- Error(stmt, "range restriction in parallel statement must be of type bool (instead got {0})", s.Range.Type);
- }
+ ResolveExpression(s.Range, true);
+ Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(s.Range.Type, Type.Bool)) {
+ Error(stmt, "range restriction in parallel statement must be of type bool (instead got {0})", s.Range.Type);
}
foreach (var ens in s.Ens) {
- ResolveExpression(ens.E, true);
+ ResolveExpression(ens.E, false); // Note, two-state features are not allowed (see the resolution of method postconditions in this file, and see the X_ examples in Test/dafny0/ParallelResolveErrors.dfy)
Contract.Assert(ens.E.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(ens.E.Type, Type.Bool)) {
Error(ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type);
@@ -1546,7 +1572,11 @@ namespace Microsoft.Dafny {
s.Kind = ParallelStmt.ParBodyKind.Call;
} else {
s.Kind = ParallelStmt.ParBodyKind.Proof;
- Warning(s.Tok, "the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause");
+ if (s.Body is BlockStmt && ((BlockStmt)s.Body).Body.Count == 0) {
+ // an empty statement, so don't produce any warning
+ } else {
+ Warning(s.Tok, "the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause");
+ }
}
}
CheckParallelBodyRestrictions(s.Body, s.Kind == ParallelStmt.ParBodyKind.Assign);
@@ -3248,13 +3278,14 @@ namespace Microsoft.Dafny {
/// <summary>
/// Tries to find a bounded pool for each of the bound variables "bvars" of "expr". If this process
/// fails, then "null" is returned and the bound variables for which the process fails are added to "missingBounds".
- /// Requires "e" to be successfully resolved.
+ /// Requires "expr" to be successfully resolved.
/// </summary>
List<QuantifierExpr.BoundedPool> DiscoverBounds(IToken tok, List<BoundVar> bvars, Expression expr, bool polarity, List<BoundVar> missingBounds) {
Contract.Requires(tok != null);
Contract.Requires(bvars != null);
Contract.Requires(missingBounds != null);
- Contract.Requires(expr.Type != null); // a sanity check (but not a complete proof) that "e" has been resolved
+ Contract.Requires(expr != null);
+ Contract.Requires(expr.Type != null); // a sanity check (but not a complete proof) that "expr" has been resolved
Contract.Ensures(
(Contract.Result<List<QuantifierExpr.BoundedPool>>() != null &&
Contract.Result<List<QuantifierExpr.BoundedPool>>().Count == bvars.Count &&
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 61f3dad3..a6198625 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -479,6 +479,22 @@ namespace Microsoft.Dafny {
i++;
}
}
+
+ // Add:
+ // function $IsA#Dt(d: DatatypeType): bool {
+ // Dt.Ctor0?(d) || Dt.Ctor1?(d) || ...
+ // }
+ var cases_dBv = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d", predef.DatatypeType), true);
+ var cases_dId = new Bpl.IdentifierExpr(dt.tok, cases_dBv.Name, predef.DatatypeType);
+ Bpl.Expr cases_body = null;
+ foreach (DatatypeCtor ctor in dt.Ctors) {
+ var disj = FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, cases_dId);
+ cases_body = cases_body == null ? disj : Bpl.Expr.Or(cases_body, disj);
+ }
+ var cases_resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
+ var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.Name, new Bpl.VariableSeq(cases_dBv), cases_resType);
+ cases_fn.Body = cases_body;
+ sink.TopLevelDeclarations.Add(cases_fn);
}
void CreateBoundVariables(List<Formal/*!*/>/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List<Bpl.Expr/*!*/>/*!*/ args)
@@ -1022,8 +1038,124 @@ namespace Microsoft.Dafny {
ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok);
Bpl.VariableSeq localVariables = new Bpl.VariableSeq();
GenerateImplPrelude(m, inParams, outParams, builder, localVariables);
+
Bpl.StmtList stmts;
if (!wellformednessProc) {
+ if (3 <= CommandLineOptions.Clo.DafnyInduction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) {
+ var posts = new List<Expression>();
+ m.Ens.ForEach(mfe => posts.Add(mfe.E));
+ var allIns = new List<Formal>();
+ if (!m.IsStatic) {
+ allIns.Add(new ThisSurrogate(m.tok, Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass)));
+ }
+ allIns.AddRange(m.Ins);
+ var inductionVars = ApplyInduction(allIns, m.Attributes, posts, delegate(System.IO.TextWriter wr) { wr.Write(m.FullName); });
+ if (inductionVars.Count != 0) {
+ // Let the parameters be this,x,y of the method M and suppose ApplyInduction returns this,y.
+ // Also, let Pre be the precondition and VF be the decreases clause.
+ // Then, insert into the method body what amounts to:
+ // assume case-analysis-on-parameter[[ y' ]];
+ // parallel (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) {
+ // this'.M(x, y');
+ // }
+ // Generate bound variables for the parallel statement, and a substitution for the Pre and VF
+
+ // assume case-analysis-on-parameter[[ y' ]];
+ foreach (var inFormal in m.Ins) {
+ var dt = inFormal.Type.AsDatatype;
+ if (dt != null) {
+ var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.Name, Bpl.Type.Bool));
+ var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.UniqueName, TrType(inFormal.Type));
+ builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new Bpl.ExprSeq(f))));
+ }
+ }
+
+ var parBoundVars = new List<BoundVar>();
+ Expression receiverReplacement = null;
+ var substMap = new Dictionary<IVariable, Expression>();
+ foreach (var iv in inductionVars) {
+ BoundVar bv;
+ IdentifierExpr ie;
+ CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out ie);
+ parBoundVars.Add(bv);
+ if (iv is ThisSurrogate) {
+ Contract.Assert(receiverReplacement == null && substMap.Count == 0); // the receiver comes first, if at all
+ receiverReplacement = ie;
+ } else {
+ substMap.Add(iv, ie);
+ }
+ }
+
+ // Generate a CallStmt for the recursive call
+ Expression recursiveCallReceiver;
+ if (receiverReplacement != null) {
+ recursiveCallReceiver = receiverReplacement;
+ } else if (m.IsStatic) {
+ recursiveCallReceiver = new StaticReceiverExpr(m.tok, (ClassDecl)m.EnclosingClass); // this also resolves it
+ } else {
+ recursiveCallReceiver = new ImplicitThisExpr(m.tok);
+ recursiveCallReceiver.Type = Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass); // resolve here
+ }
+ var recursiveCallArgs = new List<Expression>();
+ foreach (var inFormal in m.Ins) {
+ Expression inE;
+ if (substMap.TryGetValue(inFormal, out inE)) {
+ recursiveCallArgs.Add(inE);
+ } else {
+ var ie = new IdentifierExpr(inFormal.tok, inFormal.Name);
+ ie.Var = inFormal; // resolve here
+ ie.Type = inFormal.Type; // resolve here
+ recursiveCallArgs.Add(ie);
+ }
+ }
+ var recursiveCall = new CallStmt(m.tok, new List<Expression>(), recursiveCallReceiver, m.Name, recursiveCallArgs);
+ recursiveCall.Method = m; // resolve here
+
+ Expression parRange = new LiteralExpr(m.tok, true);
+ parRange.Type = Type.Bool; // resolve here
+ if (receiverReplacement != null) {
+ // add "this' != null" to the range
+ var nil = new LiteralExpr(receiverReplacement.tok);
+ nil.Type = receiverReplacement.Type; // resolve here
+ var neqNull = new BinaryExpr(receiverReplacement.tok, BinaryExpr.Opcode.Neq, receiverReplacement, nil);
+ neqNull.ResolvedOp = BinaryExpr.ResolvedOpcode.NeqCommon; // resolve here
+ neqNull.Type = Type.Bool; // resolve here
+ parRange = DafnyAnd(parRange, neqNull);
+ }
+ foreach (var pre in m.Req) {
+ if (!pre.IsFree) {
+ parRange = DafnyAnd(parRange, Substitute(pre.E, receiverReplacement, substMap));
+ }
+ }
+ // construct an expression (generator) for: VF' << VF
+ ExpressionConverter decrCheck = delegate(Dictionary<IVariable, Expression> decrSubstMap) {
+ var decrToks = new List<IToken>();
+ var decrTypes = new List<Type>();
+ var decrCallee = new List<Bpl.Expr>();
+ var decrCaller = new List<Bpl.Expr>();
+ bool decrInferred; // we don't actually care
+ foreach (var ee in MethodDecreasesWithDefault(m, out decrInferred)) {
+ decrToks.Add(ee.tok);
+ decrTypes.Add(ee.Type);
+ decrCaller.Add(etran.TrExpr(ee));
+ Expression es = Substitute(ee, receiverReplacement, substMap);
+ es = Substitute(es, null, decrSubstMap);
+ decrCallee.Add(etran.TrExpr(es));
+ }
+ return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, etran, null, null, false, true);
+ };
+
+#if VERIFY_CORRECTNESS_OF_TRANSLATION_PARALLEL_RANGE
+ var definedness = new Bpl.StmtListBuilder();
+ var exporter = new Bpl.StmtListBuilder();
+ TrParallelCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
+ // All done, so put the two pieces together
+ builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
+#else
+ TrParallelCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
+#endif
+ }
+ }
// translate the body of the method
Contract.Assert(m.Body != null); // follows from method precondition and the if guard
stmts = TrStmt2StmtList(builder, m.Body, localVariables, etran);
@@ -1555,6 +1687,7 @@ namespace Microsoft.Dafny {
Expression precond = Substitute(p, e.Receiver, substMap);
r = BplAnd(r, etran.TrExpr(precond));
}
+ // TODO: if this is a recursive call, also conjoin the well-ordering predicate
return r;
} else if (expr is DatatypeValue) {
DatatypeValue dtv = (DatatypeValue)expr;
@@ -1788,6 +1921,23 @@ namespace Microsoft.Dafny {
return total;
}
+ Expression DafnyAnd(Expression a, Expression b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ Contract.Ensures(Contract.Result<Expression>() != null);
+
+ if (LiteralExpr.IsTrue(a)) {
+ return b;
+ } else if (LiteralExpr.IsTrue(b)) {
+ return a;
+ } else {
+ BinaryExpr and = new BinaryExpr(a.tok, BinaryExpr.Opcode.And, a, b);
+ and.ResolvedOp = BinaryExpr.ResolvedOpcode.And; // resolve here
+ and.Type = Type.Bool; // resolve here
+ return and;
+ }
+ }
+
Bpl.Expr BplAnd(Bpl.Expr a, Bpl.Expr b) {
Contract.Requires(a != null);
Contract.Requires(b != null);
@@ -2282,10 +2432,7 @@ namespace Microsoft.Dafny {
if (prefix == null) {
prefix = guardConjunct;
} else {
- BinaryExpr and = new BinaryExpr(tok, BinaryExpr.Opcode.And, prefix, guardConjunct);
- and.ResolvedOp = BinaryExpr.ResolvedOpcode.And; // resolve here
- and.Type = Type.Bool; // resolve here
- prefix = and;
+ prefix = DafnyAnd(prefix, guardConjunct);
}
}
}
@@ -2353,6 +2500,20 @@ namespace Microsoft.Dafny {
}
}
+ void CloneVariableAsBoundVar(IToken tok, IVariable iv, string prefix, out BoundVar bv, out IdentifierExpr ie) {
+ Contract.Requires(tok != null);
+ Contract.Requires(iv != null);
+ Contract.Requires(prefix != null);
+ Contract.Ensures(Contract.ValueAtReturn(out bv) != null);
+ Contract.Ensures(Contract.ValueAtReturn(out ie) != null);
+
+ bv = new BoundVar(tok, prefix + otherTmpVarCount, iv.Type);
+ otherTmpVarCount++; // use this counter, but for a Dafny name (the idea being that the number and the initial "_" in the name might avoid name conflicts)
+ ie = new IdentifierExpr(tok, bv.Name);
+ ie.Var = bv; // resolve here
+ ie.Type = bv.Type; // resolve here
+ }
+
Bpl.Constant GetClass(TopLevelDecl cl)
{
Contract.Requires(cl != null);
@@ -3208,7 +3369,7 @@ namespace Microsoft.Dafny {
var s0 = (CallStmt)s.S0;
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
- TrParallelCall(s, s0, definedness, exporter, locals, etran);
+ TrParallelCall(s.Tok, s.BoundVars, s.Range, null, s0, definedness, exporter, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok)));
builder.Add(CaptureState(stmt.Tok));
@@ -3347,11 +3508,9 @@ namespace Microsoft.Dafny {
// }
var substMap = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);
- if (s.Range != null) {
- Expression range = Substitute(s.Range, null, substMap);
- TrStmt_CheckWellformed(range, definedness, locals, etran, false);
- definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(range)));
- }
+ Expression range = Substitute(s.Range, null, substMap);
+ TrStmt_CheckWellformed(range, definedness, locals, etran, false);
+ definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(range)));
var lhs = Substitute(s0.Lhs.Resolved, null, substMap);
TrStmt_CheckWellformed(lhs, definedness, locals, etran, false);
@@ -3378,10 +3537,8 @@ namespace Microsoft.Dafny {
// check for duplicate LHSs
var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran);
var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime);
- if (s.Range != null) {
- Expression range = Substitute(s.Range, null, substMapPrime);
- definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));
- }
+ range = Substitute(s.Range, null, substMapPrime);
+ definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));
// assume !(x == x' && y == y');
Bpl.Expr eqs = Bpl.Expr.True;
foreach (var bv in s.BoundVars) {
@@ -3421,9 +3578,7 @@ namespace Microsoft.Dafny {
Bpl.Expr oldHeapOF = ExpressionTranslator.ReadHeap(s.Tok, prevHeap, o, f);
Bpl.VariableSeq xBvars = new Bpl.VariableSeq();
var xBody = etran.TrBoundVariables(s.BoundVars, xBvars);
- if (s.Range != null) {
- xBody = BplAnd(xBody, prevEtran.TrExpr(s.Range));
- }
+ xBody = BplAnd(xBody, prevEtran.TrExpr(s.Range));
Bpl.Expr xObj, xField;
GetObjFieldDetails(s0.Lhs.Resolved, prevEtran, out xObj, out xField);
xBody = BplAnd(xBody, Bpl.Expr.Eq(o, xObj));
@@ -3438,9 +3593,7 @@ namespace Microsoft.Dafny {
// $Heap[ Object(x,y)[$Heap:=oldHeap], Field(x,y)[$Heap:=oldHeap] ] == G[$Heap:=oldHeap] ));
xBvars = new Bpl.VariableSeq();
Bpl.Expr xAnte = etran.TrBoundVariables(s.BoundVars, xBvars);
- if (s.Range != null) {
- xAnte = BplAnd(xAnte, prevEtran.TrExpr(s.Range));
- }
+ xAnte = BplAnd(xAnte, prevEtran.TrExpr(s.Range));
var rhs = ((ExprRhs)s0.Rhs).Expr;
var g = prevEtran.TrExpr(rhs);
GetObjFieldDetails(s0.Lhs.Resolved, prevEtran, out xObj, out xField);
@@ -3459,7 +3612,20 @@ namespace Microsoft.Dafny {
}
}
- void TrParallelCall(ParallelStmt s, CallStmt s0, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
+ delegate Bpl.Expr ExpressionConverter(Dictionary<IVariable, Expression> substMap);
+
+ void TrParallelCall(IToken tok, List<BoundVar> boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0,
+ Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
+ Contract.Requires(tok != null);
+ Contract.Requires(boundVars != null);
+ Contract.Requires(range != null);
+ // additionalRange is allowed to be null
+ Contract.Requires(s0 != null);
+ // definedness is allowed to be null
+ Contract.Requires(exporter != null);
+ Contract.Requires(locals != null);
+ Contract.Requires(etran != null);
+
// Translate:
// parallel (x,y | Range(x,y)) {
// E(x,y) . M( Args(x,y) );
@@ -3470,58 +3636,64 @@ namespace Microsoft.Dafny {
// havoc x,y;
// CheckWellformed( Range );
// assume Range(x,y);
+ // assume additionalRange;
// Tr( Call );
// assume false;
// } else {
- // assume (forall x,y :: Range(x,y) ==> Post( E(x,y), Args(x,y) ));
+ // assume (forall x,y :: Range(x,y) && additionalRange ==> Post( E(x,y), Args(x,y) ));
// }
// where Post(this,args) is the postcondition of method M.
- // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals
- // here (rather than a TrBoundVariables). However, there is currently no way to apply
- // a substMap to a statement (in particular, to s.Body), so that doesn't work here.
- Bpl.VariableSeq bvars = new Bpl.VariableSeq();
- var ante = etran.TrBoundVariables(s.BoundVars, bvars, true);
- locals.AddRange(bvars);
- var havocIds = new Bpl.IdentifierExprSeq();
- foreach (Bpl.Variable bv in bvars) {
- havocIds.Add(new Bpl.IdentifierExpr(s.Tok, bv));
- }
- definedness.Add(new Bpl.HavocCmd(s.Tok, havocIds));
- definedness.Add(new Bpl.AssumeCmd(s.Tok, ante));
- if (s.Range != null) {
- TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false);
- definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));
- }
+ if (definedness != null) {
+ // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals
+ // here (rather than a TrBoundVariables). However, there is currently no way to apply
+ // a substMap to a statement (in particular, to s.Body), so that doesn't work here.
+ Bpl.VariableSeq bvars = new Bpl.VariableSeq();
+ var ante = etran.TrBoundVariables(boundVars, bvars, true);
+ locals.AddRange(bvars);
+ var havocIds = new Bpl.IdentifierExprSeq();
+ foreach (Bpl.Variable bv in bvars) {
+ havocIds.Add(new Bpl.IdentifierExpr(tok, bv));
+ }
+ definedness.Add(new Bpl.HavocCmd(tok, havocIds));
+ definedness.Add(new Bpl.AssumeCmd(tok, ante));
+ TrStmt_CheckWellformed(range, definedness, locals, etran, false);
+ definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));
+ if (additionalRange != null) {
+ var es = additionalRange(new Dictionary<IVariable, Expression>());
+ definedness.Add(new Bpl.AssumeCmd(es.tok, es));
+ }
- TrStmt(s0, definedness, locals, etran);
+ TrStmt(s0, definedness, locals, etran);
- definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
+ definedness.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.False));
+ }
// Now for the other branch, where the postcondition of the call is exported.
+ {
+ var bvars = new Bpl.VariableSeq();
+ Dictionary<IVariable, Expression> substMap;
+ var ante = etran.TrBoundVariablesRename(boundVars, bvars, out substMap);
+ ante = BplAnd(ante, etran.TrExpr(Substitute(range, null, substMap)));
+ if (additionalRange != null) {
+ ante = BplAnd(ante, additionalRange(substMap));
+ }
- bvars = new Bpl.VariableSeq();
- Dictionary<IVariable, Expression> substMap;
- ante = etran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap);
- if (s.Range != null) {
- var range = Substitute(s.Range, null, substMap);
- ante = BplAnd(ante, etran.TrExpr(range));
- }
+ var argsSubstMap = new Dictionary<IVariable, Expression>(); // maps formal arguments to actuals
+ Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);
+ for (int i = 0; i < s0.Method.Ins.Count; i++) {
+ argsSubstMap.Add(s0.Method.Ins[i], s0.Args[i]);
+ }
+ Bpl.Expr post = Bpl.Expr.True;
+ foreach (var ens in s0.Method.Ens) {
+ var p = Substitute(ens.E, s0.Receiver, argsSubstMap); // substitute the call's actuals for the method's formals
+ p = Substitute(p, null, substMap); // substitute the renamed bound variables for the declared ones
+ post = BplAnd(post, etran.TrExpr(p));
+ }
- var argsSubstMap = new Dictionary<IVariable, Expression>(); // maps formal arguments to actuals
- Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);
- for (int i = 0; i < s0.Method.Ins.Count; i++) {
- argsSubstMap.Add(s0.Method.Ins[i], s0.Args[i]);
+ Bpl.Expr qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post));
+ exporter.Add(new Bpl.AssumeCmd(tok, qq));
}
- Bpl.Expr post = Bpl.Expr.True;
- foreach (var ens in s0.Method.Ens) {
- var p = Substitute(ens.E, s0.Receiver, argsSubstMap); // substitute the call's actuals for the method's formals
- p = Substitute(p, null, substMap); // substitute the renamed bound variables for the declared ones
- post = BplAnd(post, etran.TrExpr(p));
- }
-
- Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, bvars, Bpl.Expr.Imp(ante, post));
- exporter.Add(new Bpl.AssumeCmd(s.Tok, qq));
}
void TrParallelProof(ParallelStmt s, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
@@ -3557,10 +3729,8 @@ namespace Microsoft.Dafny {
}
definedness.Add(new Bpl.HavocCmd(s.Tok, havocIds));
definedness.Add(new Bpl.AssumeCmd(s.Tok, ante));
- if (s.Range != null) {
- TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false);
- definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));
- }
+ TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false);
+ definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));
TrStmt(s.Body, definedness, locals, etran);
@@ -3584,11 +3754,8 @@ namespace Microsoft.Dafny {
bvars = new Bpl.VariableSeq();
Dictionary<IVariable, Expression> substMap;
ante = etran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap);
- if (s.Range != null) {
- var range = Substitute(s.Range, null, substMap);
- TrStmt_CheckWellformed(range, definedness, locals, etran, false);
- ante = BplAnd(ante, etran.TrExpr(range));
- }
+ var range = Substitute(s.Range, null, substMap);
+ ante = BplAnd(ante, etran.TrExpr(range));
Bpl.Expr post = Bpl.Expr.True;
foreach (var ens in s.Ens) {
@@ -4148,7 +4315,7 @@ namespace Microsoft.Dafny {
Contract.Requires(etran != null);
Contract.Requires(predef != null);
Contract.Requires(types.Count == ee0.Count && ee0.Count == ee1.Count);
- Contract.Requires((builder != null) == (suffixMsg != null));
+ Contract.Requires(builder == null || suffixMsg != null);
Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
int N = types.Count;
@@ -6268,7 +6435,7 @@ namespace Microsoft.Dafny {
} else if ((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) {
var e = (QuantifierExpr)expr;
var inductionVariables = ApplyInduction(e);
- if (inductionVariables.Count != 0) {
+ if (2 <= CommandLineOptions.Clo.DafnyInduction && inductionVariables.Count != 0) {
// From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation
// (forall n :: (forall k :: k < n ==> P(k)) ==> P(n))
// For an existential (exists n :: P(n)), it is
@@ -6360,12 +6527,30 @@ namespace Microsoft.Dafny {
}
}
- List<BoundVar> ApplyInduction(QuantifierExpr e)
+ List<BoundVar> ApplyInduction(QuantifierExpr e) {
+ return ApplyInduction(e.BoundVars, e.Attributes, new List<Expression>() { e.LogicalBody() },
+ delegate(System.IO.TextWriter wr) { new Printer(Console.Out).PrintExpression(e); });
+ }
+
+ delegate void TracePrinter(System.IO.TextWriter wr);
+
+ /// <summary>
+ /// Return a subset of "boundVars" (in the order giving in "boundVars") to which to apply induction to,
+ /// according to :induction attributes in "attributes" and heuristically interesting subexpressions of
+ /// "searchExprs".
+ /// </summary>
+ List<VarType> ApplyInduction<VarType>(List<VarType> boundVars, Attributes attributes, List<Expression> searchExprs, TracePrinter tracePrinter) where VarType : class, IVariable
{
- Contract.Requires(e != null);
- Contract.Ensures(Contract.Result<List<BoundVar>>() != null);
+ Contract.Requires(boundVars != null);
+ Contract.Requires(searchExprs != null);
+ Contract.Requires(tracePrinter != null);
+ Contract.Ensures(Contract.Result<List<VarType>>() != null);
+
+ if (CommandLineOptions.Clo.DafnyInduction == 0) {
+ return new List<VarType>(); // don't apply induction
+ }
- for (var a = e.Attributes; a != null; a = a.Prev) {
+ for (var a = attributes; a != null; a = a.Prev) {
if (a.Name == "induction") {
// Here are the supported forms of the :induction attribute.
// :induction -- apply induction to all bound variables
@@ -6382,26 +6567,44 @@ namespace Microsoft.Dafny {
if (arg != null && arg.Value is bool && !(bool)arg.Value) {
if (CommandLineOptions.Clo.Trace) {
Console.Write("Suppressing automatic induction for: ");
- new Printer(Console.Out).PrintExpression(e);
+ tracePrinter(Console.Out);
Console.WriteLine();
}
- return new List<BoundVar>();
+ return new List<VarType>();
}
}
// Handle {:induction L}
if (a.Args.Count != 0) {
- var L = new List<BoundVar>();
+ // check that all attribute arguments refer to bound variables; otherwise, go to default_form
+ var argsAsVars = new List<VarType>();
foreach (var arg in a.Args) {
- var id = arg.E.Resolved as IdentifierExpr;
- var bv = id == null ? null : id.Var as BoundVar;
- if (bv != null && e.BoundVars.Contains(bv)) {
- // add to L, but don't add duplicates
- if (!L.Contains(bv)) {
- L.Add(bv);
+ var theArg = arg.E.Resolved;
+ if (theArg is ThisExpr) {
+ foreach (var bv in boundVars) {
+ if (bv is ThisSurrogate) {
+ argsAsVars.Add(bv);
+ goto TRY_NEXT_ATTRIBUTE_ARGUMENT;
+ }
+ }
+ } else if (theArg is IdentifierExpr) {
+ var id = (IdentifierExpr)theArg;
+ var bv = id.Var as VarType;
+ if (bv != null && boundVars.Contains(bv)) {
+ argsAsVars.Add(bv);
+ goto TRY_NEXT_ATTRIBUTE_ARGUMENT;
}
- } else {
- goto USE_DEFAULT_FORM;
+ }
+ // the attribute argument was not one of the possible induction variables
+ goto USE_DEFAULT_FORM;
+ TRY_NEXT_ATTRIBUTE_ARGUMENT:
+ ;
+ }
+ // so, all attribute arguments are variables; add them to L in the order of the bound variables (not necessarily the order in the attribute)
+ var L = new List<VarType>();
+ foreach (var bv in boundVars) {
+ if (argsAsVars.Contains(bv)) {
+ L.Add(bv);
}
}
if (CommandLineOptions.Clo.Trace) {
@@ -6411,7 +6614,7 @@ namespace Microsoft.Dafny {
sep = ", ";
}
Console.Write(" of: ");
- new Printer(Console.Out).PrintExpression(e);
+ tracePrinter(Console.Out);
Console.WriteLine();
}
return L;
@@ -6421,20 +6624,24 @@ namespace Microsoft.Dafny {
// We have the {:induction} case, or something to be treated in the same way
if (CommandLineOptions.Clo.Trace) {
Console.Write("Applying requested induction on all bound variables of: ");
- new Printer(Console.Out).PrintExpression(e);
+ tracePrinter(Console.Out);
Console.WriteLine();
}
- return e.BoundVars;
+ return boundVars;
}
}
+ if (CommandLineOptions.Clo.DafnyInduction < 2) {
+ return new List<VarType>(); // don't apply induction
+ }
+
// consider automatically applying induction
- var inductionVariables = new List<BoundVar>();
- foreach (var n in e.BoundVars) {
- if (!n.Type.IsTypeParameter && VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) {
+ var inductionVariables = new List<VarType>();
+ foreach (var n in boundVars) {
+ if (!n.Type.IsTypeParameter && searchExprs.Exists(expr => VarOccursInArgumentToRecursiveFunction(expr, n))) {
if (CommandLineOptions.Clo.Trace) {
Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);
- new Printer(Console.Out).PrintExpression(e);
+ tracePrinter(Console.Out);
Console.WriteLine();
}
inductionVariables.Add(n);
@@ -6447,57 +6654,136 @@ namespace Microsoft.Dafny {
/// <summary>
/// Returns 'true' iff
/// there is a subexpression of 'expr' of the form 'F(...n...)' where 'F' is a recursive function
- /// and 'n' appears in an "elevated" subexpression of some argument to 'F',
+ /// and 'n' appears in an "elevated" subexpression of some decreases-contributing argument to 'F',
+ /// "elevated" essentially means "top-level or top-level under a + or -".
+ /// Variations, where a higher number means a more discriminating (and, consequently,
+ /// more complicated) heuristic:
+ /// * DafnyInductionHeuristic==0: always return 'true' no matter what
+ /// * DafnyInductionHeuristic==1: replace "elevated" by "any", and look at all arguments to 'F'
+ /// * DafnyInductionHeuristic==2: look at all arguments to 'F'
+ /// * DafnyInductionHeuristic==3: as stated above
+ /// Parameter 'n' is allowed to be a ThisSurrogate.
+ /// </summary>
+ bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {
+ switch (CommandLineOptions.Clo.DafnyInductionHeuristic) {
+ case 0: return true;
+ case 1: return VarOccursInArgumentToRecursiveFunction(expr, n, n);
+ default: return VarOccursInArgumentToRecursiveFunction(expr, n, null);
+ }
+ }
+
+ /// <summary>
+ /// Returns 'true' iff
+ /// there is a subexpression of 'expr' of the form 'F(...n...)' where 'F' is a recursive function
+ /// and 'n' appears in an "elevated" subexpression of some decreases-contributing argument to 'F',
/// or
/// 'p' is non-null and 'p' appears in an "elevated" subexpression of 'expr'.
+ /// Variations:
+ /// * DafnyInductionHeuristic LESS 2: replace "elevated" by "any"
+ /// * DafnyInductionHeuristic LESS 3: look at all arguments to 'F'
/// Requires that 'p' is either 'null' of 'n'.
+ /// Parameters 'n' and 'p' are allowed to be a ThisSurrogate.
/// </summary>
- static bool VarOccursInArgumentToRecursiveFunction(Expression expr, BoundVar n, BoundVar p) {
+ bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, IVariable p) {
Contract.Requires(expr != null);
Contract.Requires(n != null);
+ Contract.Requires(p == null || p == n);
+
+ var pForNotElevated = CommandLineOptions.Clo.DafnyInductionHeuristic < 2 ? p : null;
- if (expr is LiteralExpr || expr is WildcardExpr || expr is ThisExpr || expr is BoogieWrapper) {
+ if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) {
return false;
+ } else if (expr is ThisExpr) {
+ return p is ThisSurrogate;
} else if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
return p != null && e.Var == p;
} else if (expr is DisplayExpression) {
var e = (DisplayExpression)expr;
- return e.Elements.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, null)); // subexpressions are not "elevated"
+ return e.Elements.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, pForNotElevated)); // subexpressions are not "elevated"
} else if (expr is FieldSelectExpr) {
var e = (FieldSelectExpr)expr;
- return VarOccursInArgumentToRecursiveFunction(e.Obj, n, null); // subexpressions are not "elevated"
+ return VarOccursInArgumentToRecursiveFunction(e.Obj, n, pForNotElevated); // subexpressions are not "elevated"
} else if (expr is SeqSelectExpr) {
var e = (SeqSelectExpr)expr;
- p = e.SelectOne ? null : p;
- return VarOccursInArgumentToRecursiveFunction(e.Seq, n, null) || // this subexpression is not "elevated"
- (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, p)) || // this one is, if the SeqSelectExpr denotes a range
- (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, p)); // ditto
+ var q = e.SelectOne ? pForNotElevated : p;
+ return VarOccursInArgumentToRecursiveFunction(e.Seq, n, pForNotElevated) || // this subexpression is not "elevated"
+ (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) || // this one is, if the SeqSelectExpr denotes a range
+ (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q)); // ditto
} else if (expr is SeqUpdateExpr) {
var e = (SeqUpdateExpr)expr;
return VarOccursInArgumentToRecursiveFunction(e.Seq, n, p) || // this subexpression is "elevated"
- VarOccursInArgumentToRecursiveFunction(e.Index, n, null) || // but this one
- VarOccursInArgumentToRecursiveFunction(e.Value, n, null); // and this one are not
+ VarOccursInArgumentToRecursiveFunction(e.Index, n, pForNotElevated) || // but this one
+ VarOccursInArgumentToRecursiveFunction(e.Value, n, pForNotElevated); // and this one are not
} else if (expr is MultiSelectExpr) {
var e = (MultiSelectExpr)expr;
// subexpressions are not "elevated"
- return VarOccursInArgumentToRecursiveFunction(e.Array, n, null) ||
- e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, null));
+ return VarOccursInArgumentToRecursiveFunction(e.Array, n, pForNotElevated) ||
+ e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, pForNotElevated));
} else if (expr is FunctionCallExpr) {
var e = (FunctionCallExpr)expr;
// For recursive functions: arguments are "elevated"
// For non-recursive function: arguments are "elevated" if the call is
- if (e.Function.IsRecursive) {
- p = n;
+ var rec = e.Function.IsRecursive;
+ bool inferredDecreases; // we don't actually care
+ var decr = FunctionDecreasesWithDefault(e.Function, out inferredDecreases);
+ bool variantArgument;
+ if (CommandLineOptions.Clo.DafnyInductionHeuristic < 3) {
+ variantArgument = rec;
+ } else {
+ // The receiver is considered to be "variant" if the function is recursive and the receiver participates
+ // in the effective decreases clause of the function. The receiver participates if it's a free variable
+ // of a term in the explicit decreases clause.
+ variantArgument = rec && decr.Exists(ee => ContainsFreeVariable(ee, true, null));
+ }
+ if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument ? n : p)) {
+ return true;
+ }
+#if DEBUG_TRACE
+ if (rec && !variantArgument) {
+ // rec is true, but variantArgument is not. So, we passed in "p" whereas under the previous approach, we would have passed in "n".
+ if (n != p) {
+ // We can now say more precisely: we passed in "null", whereas the previous approach would have passed in "n"
+ if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, n)) {
+ // Moreover, passing in "null" instead of "n" actually made a difference here
+ Console.WriteLine("DEBUG: rec is true but variantArgument is not (this), and it made a difference");
+ }
+ }
+ }
+#endif
+ Contract.Assert(e.Function.Formals.Count == e.Args.Count);
+ for (int i = 0; i < e.Function.Formals.Count; i++) {
+ var f = e.Function.Formals[i];
+ var exp = e.Args[i];
+ if (CommandLineOptions.Clo.DafnyInductionHeuristic < 3) {
+ variantArgument = rec;
+ } else {
+ // The argument position is considered to be "variant" if the function is recursive and the argument participates
+ // in the effective decreases clause of the function. The argument participates if it's a free variable
+ // of a term in the explicit decreases clause.
+ variantArgument = rec && decr.Exists(ee => ContainsFreeVariable(ee, false, f));
+ }
+ if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument ? n : p)) {
+ return true;
+ }
+#if DEBUG_TRACE
+ if (rec && !variantArgument) {
+ // rec is true, but variantArgument is not. So, we passed in "p" whereas under the previous approach, we would have passed in "n".
+ if (n != p) {
+ // We can now say more precisely: we passed in "null", whereas the previous approach would have passed in "n"
+ if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, n)) {
+ // Moreover, passing in "null" instead of "n" actually made a difference here
+ Console.WriteLine("DEBUG: rec is true but variantArgument is not ({0}), and it made a difference", f.Name);
+ }
+ }
+ }
+#endif
}
- return VarOccursInArgumentToRecursiveFunction(e.Receiver, n, p) ||
- e.Args.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, p));
+ return false;
} else if (expr is DatatypeValue) {
var e = (DatatypeValue)expr;
- if (!n.Type.IsDatatype) {
- p = null;
- }
- return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, p));
+ var q = n.Type.IsDatatype ? p : pForNotElevated;
+ return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));
} else if (expr is OldExpr) {
var e = (OldExpr)expr;
return VarOccursInArgumentToRecursiveFunction(e.E, n, p);
@@ -6506,16 +6792,17 @@ namespace Microsoft.Dafny {
return VarOccursInArgumentToRecursiveFunction(e.E, n, p);
} else if (expr is FreshExpr) {
var e = (FreshExpr)expr;
- return VarOccursInArgumentToRecursiveFunction(e.E, n, null);
+ return VarOccursInArgumentToRecursiveFunction(e.E, n, pForNotElevated);
} else if (expr is AllocatedExpr) {
var e = (AllocatedExpr)expr;
- return VarOccursInArgumentToRecursiveFunction(e.E, n, null);
+ return VarOccursInArgumentToRecursiveFunction(e.E, n, pForNotElevated);
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
// arguments to both Not and SeqLength are "elevated"
return VarOccursInArgumentToRecursiveFunction(e.E, n, p);
} else if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
+ IVariable q;
switch (e.ResolvedOp) {
case BinaryExpr.ResolvedOpcode.Add:
case BinaryExpr.ResolvedOpcode.Sub:
@@ -6527,22 +6814,23 @@ namespace Microsoft.Dafny {
case BinaryExpr.ResolvedOpcode.SetDifference:
case BinaryExpr.ResolvedOpcode.Concat:
// these operators have "elevated" arguments
+ q = p;
break;
default:
// whereas all other binary operators do not
- p = null;
+ q = pForNotElevated;
break;
}
- return VarOccursInArgumentToRecursiveFunction(e.E0, n, p) ||
- VarOccursInArgumentToRecursiveFunction(e.E1, n, p);
+ return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||
+ VarOccursInArgumentToRecursiveFunction(e.E1, n, q);
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
- return (e.Range != null && VarOccursInArgumentToRecursiveFunction(e.Range, n, null)) ||
- VarOccursInArgumentToRecursiveFunction(e.Term, n, null);
+ return (e.Range != null && VarOccursInArgumentToRecursiveFunction(e.Range, n, pForNotElevated)) ||
+ VarOccursInArgumentToRecursiveFunction(e.Term, n, pForNotElevated);
} else if (expr is ITEExpr) {
var e = (ITEExpr)expr;
- return VarOccursInArgumentToRecursiveFunction(e.Test, n, null) || // test is not "elevated"
- VarOccursInArgumentToRecursiveFunction(e.Thn, n, p) || // but the two branches are
+ return VarOccursInArgumentToRecursiveFunction(e.Test, n, pForNotElevated) || // test is not "elevated"
+ VarOccursInArgumentToRecursiveFunction(e.Thn, n, p) || // but the two branches are
VarOccursInArgumentToRecursiveFunction(e.Els, n, p);
} else if (expr is ConcreteSyntaxExpression) {
var e = (ConcreteSyntaxExpression)expr;
@@ -6593,7 +6881,26 @@ namespace Microsoft.Dafny {
}
}
- static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap) {
+ static bool ContainsFreeVariable(Expression expr, bool lookForReceiver, IVariable v) {
+ Contract.Requires(expr != null);
+ Contract.Requires(lookForReceiver || v != null);
+
+ if (expr is ThisExpr) {
+ return lookForReceiver;
+ } else if (expr is IdentifierExpr) {
+ IdentifierExpr e = (IdentifierExpr)expr;
+ return e.Var == v;
+ } else {
+ foreach (var ee in expr.SubExpressions) {
+ if (ContainsFreeVariable(ee, lookForReceiver, v)) {
+ return true;
+ }
+ }
+ return false;
+ }
+ }
+
+ static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {
Contract.Requires(expr != null);
Contract.Requires(cce.NonNullDictionaryAndValues(substMap));
Contract.Ensures(Contract.Result<Expression>() != null);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 04d60716..b2914776 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -970,7 +970,11 @@ ParallelResolveErrors.dfy(72,20): Error: trying to break out of more loop levels
ParallelResolveErrors.dfy(73,20): Error: break label is undefined or not in scope: OutsideLoop
ParallelResolveErrors.dfy(82,24): Error: trying to break out of more loop levels than there are enclosing loops
ParallelResolveErrors.dfy(83,24): Error: break label is undefined or not in scope: OutsideLoop
-13 resolution/type errors detected in ParallelResolveErrors.dfy
+ParallelResolveErrors.dfy(94,43): Error: fresh expressions are not allowed in this context
+ParallelResolveErrors.dfy(101,50): Error: old expressions are not allowed in this context
+ParallelResolveErrors.dfy(124,12): Error: old expressions are not allowed in this context
+ParallelResolveErrors.dfy(144,45): Error: fresh expressions are not allowed in this context
+17 resolution/type errors detected in ParallelResolveErrors.dfy
-------------------- Parallel.dfy --------------------
Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.
@@ -1051,7 +1055,7 @@ Execution trace:
(0,0): anon20_Then
(0,0): anon5
-Dafny program verifier finished with 20 verified, 8 errors
+Dafny program verifier finished with 24 verified, 8 errors
-------------------- TypeParameters.dfy --------------------
TypeParameters.dfy(44,22): Error: assertion violation
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 817120ce..539974fd 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -187,3 +187,14 @@ method DuplicateUpdate() {
}
}
}
+
+ghost method DontDoMuch(x: int)
+{
+}
+
+method OmittedRange() {
+ parallel (x) { }
+ parallel (x) {
+ DontDoMuch(x);
+ }
+}
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index 4e0be32e..9afa311a 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -85,3 +85,67 @@ method M1() {
}
}
}
+
+// -------------------------------------------------------------------------------------
+// Some soundness considerations
+// -------------------------------------------------------------------------------------
+
+ghost static method X_M0(y: int)
+ ensures exists o: object :: o != null && fresh(o); // error: not allowed 'fresh' here
+{
+ var p := new object;
+}
+
+class X_C { ghost var data: int; }
+ghost static method X_M1(y: int)
+ ensures exists c: X_C :: c != null && c.data != old(c.data); // error: not allowed 'old' here
+{
+ var c := new X_C;
+ c.data := c.data + 1;
+}
+
+method X_Main() {
+ if (*) {
+ parallel (x) { X_M0(x); }
+ } else {
+ parallel (x) { X_M1(x); }
+ }
+ assert false;
+}
+
+
+// The following seems to be a legitimate use of a two-state predicate in the postcondition of the parallel statement
+method X_Legit(c: X_C)
+ requires c != null;
+ modifies c;
+{
+ c.data := c.data + 1;
+ parallel (x | c.data <= x)
+ ensures old(c.data) < x; // error: not allowed 'old' here
+ {
+ }
+}
+
+// X_M2 is like X_M0, but with an out-parameter
+ghost static method X_M2(y: int) returns (r: int)
+ ensures exists o: object :: o != null && fresh(o); // 'fresh' is allowed here (because there's something coming "out" of this ghost method, namely 'r'
+{
+ var p := new object;
+}
+
+// The following method exhibits a case where M2 and a two-state parallel ensures would lead to an unsoundness
+// with the current translation.
+method X_AnotherMain(c: X_C)
+ requires c != null;
+ modifies c;
+{
+ c.data := c.data + 1;
+ parallel (x: int)
+ ensures exists o: object :: o != null && fresh(o); // error: not allowed 'fresh' here
+ {
+ var s := X_M2(x);
+ }
+ assert false;
+}
+
+// -------------------------------------------------------------------------------------
diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 0a99ca95..d53ae14b 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -81,11 +81,11 @@ Dafny program verifier finished with 6 verified, 0 errors
-------------------- Induction.dfy --------------------
-Dafny program verifier finished with 29 verified, 0 errors
+Dafny program verifier finished with 33 verified, 0 errors
-------------------- Rippling.dfy --------------------
-Dafny program verifier finished with 137 verified, 0 errors
+Dafny program verifier finished with 141 verified, 0 errors
-------------------- MoreInduction.dfy --------------------
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 15cc1ffe..3585dde6 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -56,6 +56,23 @@ class IntegerInduction {
{
}
+ // The following two ghost methods are the same as the previous two, but
+ // here no body is given--and the proof still goes through (thanks to
+ // Dafny's ghost-method induction tactic).
+
+ ghost method Lemma_Auto(n: int)
+ requires 0 <= n;
+ ensures 2 * Gauss(n) == n*(n+1);
+ {
+ }
+
+ ghost method Theorem1_Auto(n: int)
+ requires 0 <= n;
+ ensures SumOfCubes(n) == Gauss(n) * Gauss(n);
+ ensures 2 * Gauss(n) == n*(n+1);
+ {
+ }
+
// Here is another proof. It makes use of Dafny's induction heuristics to
// prove the lemma.
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 6f6a7ba7..4a1c4bbe 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -298,248 +298,248 @@ function AlwaysTrueFunction(): FunctionValue
// -----------------------------------------------------------------------------------
ghost method P1()
- ensures (forall n, xs :: concat(take(n, xs), drop(n, xs)) == xs);
+ ensures forall n, xs :: concat(take(n, xs), drop(n, xs)) == xs;
{
}
ghost method P2()
- ensures (forall n, xs, ys :: add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys))));
+ ensures forall n, xs, ys :: add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys)));
{
}
ghost method P3()
- ensures (forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True);
+ ensures forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True;
{
}
ghost method P4()
- ensures (forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs)));
+ ensures forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs));
{
}
ghost method P5()
- ensures (forall n, xs, x ::
+ ensures forall n, xs, x ::
add(Suc(Zero), count(n, xs)) == count(n, Cons(x, xs))
- ==> n == x);
+ ==> n == x;
{
}
ghost method P6()
- ensures (forall m, n :: minus(n, add(n, m)) == Zero);
+ ensures forall m, n :: minus(n, add(n, m)) == Zero;
{
}
ghost method P7()
- ensures (forall m, n :: minus(add(n, m), n) == m);
+ ensures forall m, n :: minus(add(n, m), n) == m;
{
}
ghost method P8()
- ensures (forall k, m, n :: minus(add(k, m), add(k, n)) == minus(m, n));
+ ensures forall k, m, n :: minus(add(k, m), add(k, n)) == minus(m, n);
{
}
ghost method P9()
- ensures (forall i, j, k :: minus(minus(i, j), k) == minus(i, add(j, k)));
+ ensures forall i, j, k :: minus(minus(i, j), k) == minus(i, add(j, k));
{
}
ghost method P10()
- ensures (forall m :: minus(m, m) == Zero);
+ ensures forall m :: minus(m, m) == Zero;
{
}
ghost method P11()
- ensures (forall xs :: drop(Zero, xs) == xs);
+ ensures forall xs :: drop(Zero, xs) == xs;
{
}
ghost method P12()
- ensures (forall n, xs, f :: drop(n, map(f, xs)) == map(f, drop(n, xs)));
+ ensures forall n, xs, f :: drop(n, map(f, xs)) == map(f, drop(n, xs));
{
}
ghost method P13()
- ensures (forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs));
+ ensures forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs);
{
}
ghost method P14()
- ensures (forall xs, ys, p :: filter(p, concat(xs, ys)) == concat(filter(p, xs), filter(p, ys)));
+ ensures forall xs, ys, p :: filter(p, concat(xs, ys)) == concat(filter(p, xs), filter(p, ys));
{
}
ghost method P15()
- ensures (forall x, xs :: len(ins(x, xs)) == Suc(len(xs)));
+ ensures forall x, xs :: len(ins(x, xs)) == Suc(len(xs));
{
}
ghost method P16()
- ensures (forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x);
+ ensures forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x;
{
}
ghost method P17()
- ensures (forall n :: leq(n, Zero) == True <==> n == Zero);
+ ensures forall n :: leq(n, Zero) == True <==> n == Zero;
{
}
ghost method P18()
- ensures (forall i, m :: less(i, Suc(add(i, m))) == True);
+ ensures forall i, m :: less(i, Suc(add(i, m))) == True;
{
}
ghost method P19()
- ensures (forall n, xs :: len(drop(n, xs)) == minus(len(xs), n));
+ ensures forall n, xs :: len(drop(n, xs)) == minus(len(xs), n);
{
}
ghost method P20()
- ensures (forall xs :: len(sort(xs)) == len(xs));
+ ensures forall xs :: len(sort(xs)) == len(xs);
{
// proving this theorem requires an additional lemma:
- assert (forall k, ks :: len(ins(k, ks)) == len(Cons(k, ks)));
+ assert forall k, ks :: len(ins(k, ks)) == len(Cons(k, ks));
// ...and one manually introduced case study:
- assert (forall ys ::
+ assert forall ys ::
sort(ys) == Nil ||
- (exists z, zs :: sort(ys) == Cons(z, zs)));
+ exists z, zs :: sort(ys) == Cons(z, zs);
}
ghost method P21()
- ensures (forall n, m :: leq(n, add(n, m)) == True);
+ ensures forall n, m :: leq(n, add(n, m)) == True;
{
}
ghost method P22()
- ensures (forall a, b, c :: max(max(a, b), c) == max(a, max(b, c)));
+ ensures forall a, b, c :: max(max(a, b), c) == max(a, max(b, c));
{
}
ghost method P23()
- ensures (forall a, b :: max(a, b) == max(b, a));
+ ensures forall a, b :: max(a, b) == max(b, a);
{
}
ghost method P24()
- ensures (forall a, b :: max(a, b) == a <==> leq(b, a) == True);
+ ensures forall a, b :: max(a, b) == a <==> leq(b, a) == True;
{
}
ghost method P25()
- ensures (forall a, b :: max(a, b) == b <==> leq(a, b) == True);
+ ensures forall a, b :: max(a, b) == b <==> leq(a, b) == True;
{
}
ghost method P26()
- ensures (forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True);
+ ensures forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True;
{
}
ghost method P27()
- ensures (forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True);
+ ensures forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True;
{
}
ghost method P28()
- ensures (forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True);
+ ensures forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True;
{
}
ghost method P29()
- ensures (forall x, xs :: mem(x, ins1(x, xs)) == True);
+ ensures forall x, xs :: mem(x, ins1(x, xs)) == True;
{
}
ghost method P30()
- ensures (forall x, xs :: mem(x, ins(x, xs)) == True);
+ ensures forall x, xs :: mem(x, ins(x, xs)) == True;
{
}
ghost method P31()
- ensures (forall a, b, c :: min(min(a, b), c) == min(a, min(b, c)));
+ ensures forall a, b, c :: min(min(a, b), c) == min(a, min(b, c));
{
}
ghost method P32()
- ensures (forall a, b :: min(a, b) == min(b, a));
+ ensures forall a, b :: min(a, b) == min(b, a);
{
}
ghost method P33()
- ensures (forall a, b :: min(a, b) == a <==> leq(a, b) == True);
+ ensures forall a, b :: min(a, b) == a <==> leq(a, b) == True;
{
}
ghost method P34()
- ensures (forall a, b :: min(a, b) == b <==> leq(b, a) == True);
+ ensures forall a, b :: min(a, b) == b <==> leq(b, a) == True;
{
}
ghost method P35()
- ensures (forall xs :: dropWhileAlways(AlwaysFalseFunction(), xs) == xs);
+ ensures forall xs :: dropWhileAlways(AlwaysFalseFunction(), xs) == xs;
{
}
ghost method P36()
- ensures (forall xs :: takeWhileAlways(AlwaysTrueFunction(), xs) == xs);
+ ensures forall xs :: takeWhileAlways(AlwaysTrueFunction(), xs) == xs;
{
}
ghost method P37()
- ensures (forall x, xs :: not(mem(x, delete(x, xs))) == True);
+ ensures forall x, xs :: not(mem(x, delete(x, xs))) == True;
{
}
ghost method P38()
- ensures (forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs)));
+ ensures forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs));
{
}
ghost method P39()
- ensures (forall n, x, xs ::
- add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs)));
+ ensures forall n, x, xs ::
+ add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs));
{
}
ghost method P40()
- ensures (forall xs :: take(Zero, xs) == Nil);
+ ensures forall xs :: take(Zero, xs) == Nil;
{
}
ghost method P41()
- ensures (forall n, xs, f :: take(n, map(f, xs)) == map(f, take(n, xs)));
+ ensures forall n, xs, f :: take(n, map(f, xs)) == map(f, take(n, xs));
{
}
ghost method P42()
- ensures (forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs)));
+ ensures forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs));
{
}
ghost method P43(p: FunctionValue)
- ensures (forall xs :: concat(takeWhileAlways(p, xs), dropWhileAlways(p, xs)) == xs);
+ ensures forall xs :: concat(takeWhileAlways(p, xs), dropWhileAlways(p, xs)) == xs;
{
}
ghost method P44()
- ensures (forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys));
+ ensures forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys);
{
}
ghost method P45()
- ensures (forall x, xs, y, ys ::
+ ensures forall x, xs, y, ys ::
zip(Cons(x, xs), Cons(y, ys)) ==
- PCons(Pair.Pair(x, y), zip(xs, ys)));
+ PCons(Pair.Pair(x, y), zip(xs, ys));
{
}
ghost method P46()
- ensures (forall ys :: zip(Nil, ys) == PNil);
+ ensures forall ys :: zip(Nil, ys) == PNil;
{
}
ghost method P47()
- ensures (forall a :: height(mirror(a)) == height(a));
+ ensures forall a :: height(mirror(a)) == height(a);
{
// proving this theorem requires a previously proved lemma:
P23();
@@ -548,40 +548,53 @@ ghost method P47()
// ...
ghost method P54()
- ensures (forall m, n :: minus(add(m, n), n) == m);
+ ensures forall m, n :: minus(add(m, n), n) == m;
{
// the proof of this theorem follows from two lemmas:
- assert (forall m, n :: minus(add(n, m), n) == m);
- assert (forall m, n :: add(m, n) == add(n, m));
+ assert forall m, n :: minus(add(n, m), n) == m;
+ assert forall m, n :: add(m, n) == add(n, m);
}
ghost method P65()
- ensures (forall i, m :: less(i, Suc(add(m, i))) == True);
+ ensures forall i, m :: less(i, Suc(add(m, i))) == True;
{
if (*) {
// the proof of this theorem follows from two lemmas:
- assert (forall i, m :: less(i, Suc(add(i, m))) == True);
- assert (forall m, n :: add(m, n) == add(n, m));
+ assert forall i, m :: less(i, Suc(add(i, m))) == True;
+ assert forall m, n :: add(m, n) == add(n, m);
} else {
// a different way to prove it uses the following lemma:
- assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));
+ assert forall x,y :: add(x, Suc(y)) == Suc(add(x,y));
}
}
ghost method P67()
- ensures (forall m, n :: leq(n, add(m, n)) == True);
+ ensures forall m, n :: leq(n, add(m, n)) == True;
{
if (*) {
// the proof of this theorem follows from two lemmas:
- assert (forall m, n :: leq(n, add(n, m)) == True);
- assert (forall m, n :: add(m, n) == add(n, m));
+ assert forall m, n :: leq(n, add(n, m)) == True;
+ assert forall m, n :: add(m, n) == add(n, m);
} else {
// a different way to prove it uses the following lemma:
- assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));
+ assert forall x,y :: add(x, Suc(y)) == Suc(add(x,y));
}
}
// ---------
+// Here is a alternate way of writing down the proof obligations:
+
+ghost method P1_alt(n: Nat, xs: List)
+ ensures concat(take(n, xs), drop(n, xs)) == xs;
+{
+}
+
+ghost method P2_alt(n: Nat, xs: List, ys: List)
+ ensures add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys)));
+{
+}
+
+// ---------
ghost method Lemma_RevConcat(xs: List, ys: List)
ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-28 19:01:32 +0000