summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Compiler.cs40
-rw-r--r--Source/Dafny/DafnyAst.cs13
-rw-r--r--Source/Dafny/Resolver.cs49
-rw-r--r--Source/Dafny/Translator.cs139
-rw-r--r--Test/dafny0/Compilation.dfy35
-rw-r--r--Test/dafny0/Compilation.dfy.expect13
-rw-r--r--Test/dafny0/ExistentialGuards.dfy86
-rw-r--r--Test/dafny0/ExistentialGuards.dfy.expect111
-rw-r--r--Test/dafny0/ExistentialGuardsResolution.dfy154
-rw-r--r--Test/dafny0/ExistentialGuardsResolution.dfy.expect167
-rw-r--r--Test/dafny0/ResolutionErrors.dfy20
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect7
12 files changed, 769 insertions, 65 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 13381cc7..aa4ca3ec 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1455,10 +1455,17 @@ namespace Microsoft.Dafny {
}
} else {
Indent(indent); wr.Write("if (");
- TrExpr(s.Guard);
+ TrExpr(s.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)s.Guard, "eg_d", new Translator(null)) : s.Guard);
wr.WriteLine(")");
- TrStmt(s.Thn, indent);
+ // We'd like to do "TrStmt(s.Thn, indent)", except we want the scope of any existential variables to come inside the block
+ Indent(indent); wr.WriteLine("{");
+ if (s.IsExistentialGuard) {
+ IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)s.Guard);
+ }
+ TrStmtList(s.Thn.Body, indent);
+ Indent(indent); wr.WriteLine("}");
+
if (s.Els != null) {
Indent(indent); wr.WriteLine("else");
TrStmt(s.Els, indent);
@@ -1467,13 +1474,14 @@ namespace Microsoft.Dafny {
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
- foreach (var alternative in s.Alternatives) {
- }
Indent(indent);
foreach (var alternative in s.Alternatives) {
wr.Write("if (");
- TrExpr(alternative.Guard);
+ TrExpr(alternative.IsExistentialGuard ? Translator.AlphaRename((ExistsExpr)alternative.Guard, "eg_d", new Translator(null)) : alternative.Guard);
wr.WriteLine(") {");
+ if (alternative.IsExistentialGuard) {
+ IntroduceAndAssignBoundVars(indent + IndentAmount, (ExistsExpr)alternative.Guard);
+ }
TrStmtList(alternative.Body, indent);
Indent(indent);
wr.Write("} else ");
@@ -1766,6 +1774,18 @@ namespace Microsoft.Dafny {
}
}
+ private void IntroduceAndAssignBoundVars(int indent, ExistsExpr exists) {
+ Contract.Requires(0 <= indent);
+ Contract.Requires(exists != null);
+ Contract.Assume(exists.Bounds != null); // follows from successful resolution
+ Contract.Assert(exists.Range == null); // follows from invariant of class IfStmt
+ foreach (var bv in exists.BoundVars) {
+ TrLocalVar(bv, false, indent);
+ }
+ var ivars = exists.BoundVars.ConvertAll(bv => (IVariable)bv);
+ TrAssignSuchThat(indent, ivars, exists.Term, exists.Bounds, exists.tok.line);
+ }
+
private void TrAssignSuchThat(int indent, List<IVariable> lhss, Expression constraint, List<ComprehensionExpr.BoundedPool> bounds, int debuginfoLine) {
Contract.Requires(0 <= indent);
Contract.Requires(lhss != null);
@@ -2155,18 +2175,18 @@ namespace Microsoft.Dafny {
}
}
- void TrLocalVar(LocalVariable s, bool alwaysInitialize, int indent) {
- Contract.Requires(s != null);
- if (s.IsGhost) {
+ void TrLocalVar(IVariable v, bool alwaysInitialize, int indent) {
+ Contract.Requires(v != null);
+ if (v.IsGhost) {
// only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)
return;
}
Indent(indent);
- wr.Write("{0} @{1}", TypeName(s.Type), s.CompileName);
+ wr.Write("{0} @{1}", TypeName(v.Type), v.CompileName);
if (alwaysInitialize) {
// produce a default value
- wr.WriteLine(" = {0};", DefaultValue(s.Type));
+ wr.WriteLine(" = {0};", DefaultValue(v.Type));
} else {
wr.WriteLine(";");
}
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 64af1425..667f8407 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3903,7 +3903,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(Expr != null);
}
- public ExprRhs(Expression expr, Attributes attrs = null)
+ public ExprRhs(Expression expr, Attributes attrs = null) // TODO: these 'attrs' apparently aren't handled correctly in the Cloner, and perhaps not in various visitors either (for example, CheckIsCompilable should not go into attributes)
: base(expr.tok, attrs)
{
Contract.Requires(expr != null);
@@ -7175,9 +7175,16 @@ namespace Microsoft.Dafny {
public override IEnumerable<Expression> SubExpressions {
get {
if (SplitQuantifier == null) {
- return base.SubExpressions;
+ foreach (var e in base.SubExpressions) {
+ yield return e;
+ }
} else {
- return SplitQuantifier;
+ foreach (var e in Attributes.SubExpressions(Attributes)) {
+ yield return e;
+ }
+ foreach (var e in SplitQuantifier) {
+ yield return e;
+ }
}
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index bc94e491..1798243c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2264,12 +2264,14 @@ namespace Microsoft.Dafny
what = "quantifier";
whereToLookForBounds = ((QuantifierExpr)e).LogicalBody();
polarity = e is ExistsExpr;
- } else if (e is SetComprehension && ((SetComprehension)e).Finite) {
+ } else if (e is SetComprehension) {
what = "set comprehension";
whereToLookForBounds = e.Range;
- } else if (e is MapComprehension && ((MapComprehension)e).Finite) {
+ } else if (e is MapComprehension) {
what = "map comprehension";
whereToLookForBounds = e.Range;
+ } else {
+ Contract.Assume(e is LambdaExpr); // otherwise, unexpected ComprehensionExpr
}
if (whereToLookForBounds != null) {
List<BoundVar> missingBounds;
@@ -2278,9 +2280,9 @@ namespace Microsoft.Dafny
e.MissingBounds = missingBounds;
if ((e is SetComprehension && !((SetComprehension)e).Finite) || (e is MapComprehension && !((MapComprehension)e).Finite)) {
- // a possibly infinite set/map has no restrictions on its range
+ // a possibly infinite set/map has no restrictions on its range (unless it's used in a compilable context, which is checked later)
} else if (e is QuantifierExpr) {
- // don't report any errors at this time (instead, wait to see if the quantifier is used in a non-ghost context)
+ // a quantifier has no restrictions on its range (unless it's used in a compilable context, which is checked later)
} else if (e is SetComprehension && e.Type.HasFinitePossibleValues) {
// This means the set is finite, regardless of if the Range is bounded. So, we don't give any error here.
// However, if this expression is used in a non-ghost context (which is not yet known at this stage of
@@ -2341,7 +2343,6 @@ namespace Microsoft.Dafny
var bin = expr as BinaryExpr;
if (bin != null) {
bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type);
-
}
}
}
@@ -5647,7 +5648,17 @@ namespace Microsoft.Dafny
Contract.Assert(s.Guard.Type != null); // follows from postcondition of ResolveExpression
ConstrainTypes(s.Guard.Type, Type.Bool, s.Guard, "condition is expected to be of type {0}, but is {1}", Type.Bool, s.Guard.Type);
}
- ResolveStatement(s.Thn, codeContext);
+
+ scope.PushMarker();
+ if (s.IsExistentialGuard) {
+ var exists = (ExistsExpr)s.Guard;
+ foreach (var v in exists.BoundVars) {
+ ScopePushAndReport(scope, v, "bound-variable");
+ }
+ }
+ ResolveBlockStatement(s.Thn, codeContext);
+ scope.PopMarker();
+
if (s.Els != null) {
ResolveStatement(s.Els, codeContext);
}
@@ -6525,7 +6536,7 @@ namespace Microsoft.Dafny
Contract.Requires(alternatives != null);
Contract.Requires(codeContext != null);
- // first, resolve the guards, which tells us whether or not the entire statement is a ghost statement
+ // first, resolve the guards
foreach (var alternative in alternatives) {
int prevErrorCount = reporter.Count(ErrorLevel.Error);
ResolveExpression(alternative.Guard, new ResolveOpts(codeContext, true));
@@ -6539,6 +6550,12 @@ namespace Microsoft.Dafny
}
foreach (var alternative in alternatives) {
scope.PushMarker();
+ if (alternative.IsExistentialGuard) {
+ var exists = (ExistsExpr)alternative.Guard;
+ foreach (var v in exists.BoundVars) {
+ ScopePushAndReport(scope, v, "bound-variable");
+ }
+ }
foreach (Statement ss in alternative.Body) {
ResolveStatement(ss, codeContext);
}
@@ -9508,9 +9525,9 @@ namespace Microsoft.Dafny
if (uncompilableBoundVars.Count != 0) {
string what;
if (e is SetComprehension) {
- what = "set comprehensions";
+ what = ((SetComprehension)e).Finite ? "set comprehensions" : "iset comprehensions";
} else if (e is MapComprehension) {
- what = "map comprehensions";
+ what = ((MapComprehension)e).Finite ? "map comprehensions" : "imap comprehensions";
} else {
Contract.Assume(e is QuantifierExpr); // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above)
Contract.Assert(((QuantifierExpr)e).SplitQuantifier == null); // No split quantifiers during resolution
@@ -9521,15 +9538,11 @@ namespace Microsoft.Dafny
}
return;
}
+ // don't recurse down any attributes
+ if (e.Range != null) { CheckIsCompilable(e.Range); }
+ CheckIsCompilable(e.Term);
+ return;
- } else if (expr is MapComprehension) {
- var e = (MapComprehension)expr;
- if (e.MissingBounds != null && !e.Finite) {
- foreach (var bv in e.MissingBounds) {
- reporter.Error(MessageSource.Resolver, expr, "imaps in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
- }
- return;
- }
} else if (expr is NamedExpr) {
if (!moduleInfo.IsAbstract)
CheckIsCompilable(((NamedExpr)expr).Body);
@@ -10436,7 +10449,7 @@ namespace Microsoft.Dafny
} else if (expr is QuantifierExpr) {
var e = (QuantifierExpr)expr;
Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution
- return e.UncompilableBoundVars().Count != 0;
+ return e.UncompilableBoundVars().Count != 0 || UsesSpecFeatures(e.LogicalBody());
} else if (expr is SetComprehension) {
var e = (SetComprehension)expr;
return !e.Finite || e.UncompilableBoundVars().Count != 0 || (e.Range != null && UsesSpecFeatures(e.Range)) || (e.Term != null && UsesSpecFeatures(e.Term));
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index c84f0cec..18b50686 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4740,7 +4740,7 @@ namespace Microsoft.Dafny {
var typeMap = Util.Dict(e.TypeArgs, Map(typeArgumentCopies, tp => (Type)new UserDefinedType(tp)));
var newLocals = Map(typeArgumentCopies, tp => new Bpl.LocalVariable(tp.tok, new TypedIdent(tp.tok, nameTypeParam(tp), predef.Ty)));
locals.AddRange(newLocals);
- // Create local variables corresponding to the in-parameters:
+ // Create local variables corresponding to the bound variables:
var substMap = SetupBoundVarsAsLocals(e.BoundVars, builder, locals, etran, typeMap);
// Get the body of the quantifier and suitably substitute for the type variables and bound variables
var body = Substitute(e.LogicalBody(true), null, substMap, typeMap);
@@ -7244,24 +7244,30 @@ namespace Microsoft.Dafny {
} else if (stmt is IfStmt) {
AddComment(builder, stmt, "if statement");
IfStmt s = (IfStmt)stmt;
- Bpl.Expr guard;
+ Expression guard;
if (s.Guard == null) {
guard = null;
} else {
- TrStmt_CheckWellformed(s.Guard, builder, locals, etran, true);
- guard = etran.TrExpr(s.Guard);
+ guard = s.IsExistentialGuard ? AlphaRename((ExistsExpr)s.Guard, "eg$", this) : s.Guard;
+ TrStmt_CheckWellformed(guard, builder, locals, etran, true);
}
Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();
CurrentIdGenerator.Push();
+ if (s.IsExistentialGuard) {
+ var exists = (ExistsExpr)s.Guard; // the original (that is, not alpha-renamed) guard
+ IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran);
+ }
Bpl.StmtList thn = TrStmt2StmtList(b, s.Thn, locals, etran);
CurrentIdGenerator.Pop();
Bpl.StmtList els;
Bpl.IfCmd elsIf = null;
+ b = new Bpl.StmtListBuilder();
+ if (s.IsExistentialGuard) {
+ b.Add(new Bpl.AssumeCmd(guard.tok, Bpl.Expr.Not(etran.TrExpr(guard))));
+ }
if (s.Els == null) {
- b = new Bpl.StmtListBuilder();
els = b.Collect(s.Tok);
} else {
- b = new Bpl.StmtListBuilder();
els = TrStmt2StmtList(b, s.Els, locals, etran);
if (els.BigBlocks.Count == 1) {
Bpl.BigBlock bb = els.BigBlocks[0];
@@ -7271,7 +7277,7 @@ namespace Microsoft.Dafny {
}
}
}
- builder.Add(new Bpl.IfCmd(stmt.Tok, guard, thn, elsIf, els));
+ builder.Add(new Bpl.IfCmd(stmt.Tok, guard == null || s.IsExistentialGuard ? null : etran.TrExpr(guard), thn, elsIf, els));
} else if (stmt is AlternativeStmt) {
AddComment(builder, stmt, "alternative statement");
@@ -7551,6 +7557,26 @@ namespace Microsoft.Dafny {
}
}
+ private void IntroduceAndAssignExistentialVars(ExistsExpr exists, Bpl.StmtListBuilder builder, Bpl.StmtListBuilder builderOutsideIfConstruct, List<Variable> locals, ExpressionTranslator etran) {
+ Contract.Requires(exists != null);
+ Contract.Requires(exists.Range == null);
+ Contract.Requires(builder != null);
+ Contract.Requires(builderOutsideIfConstruct != null);
+ Contract.Requires(locals != null);
+ Contract.Requires(etran != null);
+ // declare and havoc the bound variables of 'exists' as local variables
+ var iesForHavoc = new List<Bpl.IdentifierExpr>();
+ foreach (var bv in exists.BoundVars) {
+ Bpl.Type varType = TrType(bv.Type);
+ Bpl.Expr wh = GetWhereClause(bv.Tok, new Bpl.IdentifierExpr(bv.Tok, bv.AssignUniqueName(currentDeclaration.IdGenerator), varType), bv.Type, etran);
+ Bpl.Variable local = new Bpl.LocalVariable(bv.Tok, new Bpl.TypedIdent(bv.Tok, bv.AssignUniqueName(currentDeclaration.IdGenerator), varType, wh));
+ locals.Add(local);
+ iesForHavoc.Add(new Bpl.IdentifierExpr(local.tok, local));
+ }
+ builderOutsideIfConstruct.Add(new Bpl.HavocCmd(exists.tok, iesForHavoc));
+ builder.Add(new Bpl.AssumeCmd(exists.tok, etran.TrExpr(exists.Term)));
+ }
+
void TrStmtList(List<Statement> stmts, Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
Contract.Requires(stmts != null);
Contract.Requires(builder != null);
@@ -7565,6 +7591,46 @@ namespace Microsoft.Dafny {
}
/// <summary>
+ /// Returns an expression like 'exists' but where the bound variables have been renamed to have
+ /// 'prefix' as a prefix to their previous names.
+ /// Assumes the expression has been resolved.
+ /// </summary>
+ public static Expression AlphaRename(ExistsExpr exists, string prefix, Translator translator) {
+ Contract.Requires(exists != null);
+ Contract.Requires(prefix != null);
+ Contract.Requires(translator != null);
+
+ if (exists.SplitQuantifier != null) {
+ // TODO: what to do? Substitute(exists.SplitQuantifierExpression);
+ }
+
+ var substMap = new Dictionary<IVariable, Expression>();
+ var var4var = new Dictionary<BoundVar, BoundVar>();
+ var bvars = new List<BoundVar>();
+ foreach (var bv in exists.BoundVars) {
+ var newBv = new BoundVar(bv.tok, prefix + bv.Name, bv.Type);
+ bvars.Add(newBv);
+ var4var.Add(bv, newBv);
+ var ie = new IdentifierExpr(newBv.tok, newBv.Name);
+ ie.Var = newBv; // resolve here
+ ie.Type = newBv.Type; // resolve here
+ substMap.Add(bv, ie);
+ }
+ var s = new Substituter(null, substMap, new Dictionary<TypeParameter, Type>(), translator);
+ var range = exists.Range == null ? null : s.Substitute(exists.Range);
+ var term = s.Substitute(exists.Term);
+ var attrs = s.SubstAttributes(exists.Attributes);
+ var ex = new ExistsExpr(exists.tok, exists.TypeArgs, bvars, range, term, attrs);
+ if (exists.Bounds != null) {
+ ex.Bounds = exists.Bounds.ConvertAll(bound => s.SubstituteBoundedPool(bound));
+ }
+ if (exists.MissingBounds != null) {
+ ex.MissingBounds = exists.MissingBounds.ConvertAll(bv => var4var[bv]);
+ }
+ return ex;
+ }
+
+ /// <summary>
/// Generate:
/// havoc Heap \ {this} \ _reads \ _new;
/// assume this.Valid();
@@ -8569,7 +8635,7 @@ namespace Microsoft.Dafny {
void TrAlternatives(List<GuardedAlternative> alternatives, Bpl.Cmd elseCase0, Bpl.StructuredCmd elseCase1,
Bpl.StmtListBuilder builder, List<Variable> locals, ExpressionTranslator etran) {
Contract.Requires(alternatives != null);
- Contract.Requires((elseCase0 != null) == (elseCase1 == null)); // ugly way of doing a type union
+ Contract.Requires((elseCase0 == null) != (elseCase1 == null)); // ugly way of doing a type union
Contract.Requires(builder != null);
Contract.Requires(locals != null);
Contract.Requires(etran != null);
@@ -8583,10 +8649,13 @@ namespace Microsoft.Dafny {
return;
}
+ // alpha-rename any existential guards
+ var guards = alternatives.ConvertAll(alt => alt.IsExistentialGuard ? AlphaRename((ExistsExpr)alt.Guard, "eg$", this) : alt.Guard);
+
// build the negation of the disjunction of all guards (that is, the conjunction of their negations)
Bpl.Expr noGuard = Bpl.Expr.True;
- foreach (var alternative in alternatives) {
- noGuard = BplAnd(noGuard, Bpl.Expr.Not(etran.TrExpr(alternative.Guard)));
+ foreach (var g in guards) {
+ noGuard = BplAnd(noGuard, Bpl.Expr.Not(etran.TrExpr(g)));
}
var b = new Bpl.StmtListBuilder();
@@ -8605,8 +8674,13 @@ namespace Microsoft.Dafny {
CurrentIdGenerator.Push();
var alternative = alternatives[i];
b = new Bpl.StmtListBuilder();
- TrStmt_CheckWellformed(alternative.Guard, b, locals, etran, true);
- b.Add(new AssumeCmd(alternative.Guard.tok, etran.TrExpr(alternative.Guard)));
+ TrStmt_CheckWellformed(guards[i], b, locals, etran, true);
+ if (alternative.IsExistentialGuard) {
+ var exists = (ExistsExpr)alternative.Guard; // the original (that is, not alpha-renamed) guard
+ IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran);
+ } else {
+ b.Add(new AssumeCmd(alternative.Guard.tok, etran.TrExpr(alternative.Guard)));
+ }
foreach (var s in alternative.Body) {
TrStmt(s, b, locals, etran);
}
@@ -13705,6 +13779,9 @@ namespace Microsoft.Dafny {
Contract.Assert(false); // unexpected ComprehensionExpr
}
}
+ if (e.Bounds != null) {
+ ((ComprehensionExpr)newExpr).Bounds = e.Bounds.ConvertAll(bound => SubstituteBoundedPool(bound));
+ }
// undo any changes to substMap (could be optimized to do this only if newBoundVars != e.BoundVars)
foreach (var bv in e.BoundVars) {
substMap.Remove(bv);
@@ -13761,6 +13838,44 @@ namespace Microsoft.Dafny {
}
}
+ public ComprehensionExpr.BoundedPool SubstituteBoundedPool(ComprehensionExpr.BoundedPool bound) {
+ if (bound == null) {
+ return null;
+ } else if (bound is ComprehensionExpr.ExactBoundedPool) {
+ var b = (ComprehensionExpr.ExactBoundedPool)bound;
+ return new ComprehensionExpr.ExactBoundedPool(Substitute(b.E));
+ } else if (bound is ComprehensionExpr.BoolBoundedPool) {
+ return bound; // nothing to substitute
+ } else if (bound is ComprehensionExpr.CharBoundedPool) {
+ return bound; // nothing to substitute
+ } else if (bound is ComprehensionExpr.RefBoundedPool) {
+ return bound; // nothing to substitute
+ } else if (bound is ComprehensionExpr.IntBoundedPool) {
+ var b = (ComprehensionExpr.IntBoundedPool)bound;
+ return new ComprehensionExpr.IntBoundedPool(b.LowerBound == null ? null : Substitute(b.LowerBound), b.UpperBound == null ? null : Substitute(b.UpperBound));
+ } else if (bound is ComprehensionExpr.SetBoundedPool) {
+ var b = (ComprehensionExpr.SetBoundedPool)bound;
+ return new ComprehensionExpr.SetBoundedPool(Substitute(b.Set));
+ } else if (bound is ComprehensionExpr.SubSetBoundedPool) {
+ var b = (ComprehensionExpr.SubSetBoundedPool)bound;
+ return new ComprehensionExpr.SubSetBoundedPool(Substitute(b.UpperBound));
+ } else if (bound is ComprehensionExpr.SuperSetBoundedPool) {
+ var b = (ComprehensionExpr.SuperSetBoundedPool)bound;
+ return new ComprehensionExpr.SuperSetBoundedPool(Substitute(b.LowerBound));
+ } else if (bound is ComprehensionExpr.MapBoundedPool) {
+ var b = (ComprehensionExpr.MapBoundedPool)bound;
+ return new ComprehensionExpr.MapBoundedPool(Substitute(b.Map));
+ } else if (bound is ComprehensionExpr.SeqBoundedPool) {
+ var b = (ComprehensionExpr.SeqBoundedPool)bound;
+ return new ComprehensionExpr.SeqBoundedPool(Substitute(b.Seq));
+ } else if (bound is ComprehensionExpr.DatatypeBoundedPool) {
+ return bound; // nothing to substitute
+ } else {
+ Contract.Assume(false); // unexpected ComprehensionExpr.BoundedPool
+ throw new cce.UnreachableException(); // to please compiler
+ }
+ }
+
/// <summary>
/// Return a list of bound variables, of the same length as 'vars' but with possible substitutions.
/// For any change necessary, update 'substMap' to reflect the new substitution; the caller is responsible for
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index a2b96996..7f9169da 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny "%s" > "%t"
+// RUN: %dafny /compile:3 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// The tests in this file are designed to run through the compiler. They contain
@@ -43,6 +43,8 @@ module CoRecursion {
// 40
// 41
// 42
+ // 9
+ // 9
method Main() {
var m := 17;
var cell := new Cell;
@@ -58,6 +60,37 @@ module CoRecursion {
print l.car, "\n";
l := l.cdr;
}
+ var nio := OneLess(0, 10);
+ print nio, "\n";
+ nio := OneLess'(0, 10);
+ print nio, "\n";
+ }
+
+ method OneLess(lo: int, hi: int) returns (m: int)
+ requires lo < hi
+ // This method ensures m == hi - 1, but we don't care to prove it
+ decreases hi - lo
+ {
+ if y :| lo < y < hi {
+ m := OneLess(y, hi);
+ } else {
+ m := lo;
+ }
+ }
+
+ method OneLess'(lo: int, hi: int) returns (m: int)
+ requires lo < hi
+ // This method ensures m == hi - 1, but we don't care to prove it
+ decreases hi - lo
+ {
+ if {
+ case y :| lo < y < hi =>
+ m := OneLess'(y, hi);
+ case lo+1 < hi =>
+ m := OneLess'(lo+1, hi);
+ case lo + 1 == hi =>
+ m := lo;
+ }
}
}
diff --git a/Test/dafny0/Compilation.dfy.expect b/Test/dafny0/Compilation.dfy.expect
index 0a1938ae..2b76b107 100644
--- a/Test/dafny0/Compilation.dfy.expect
+++ b/Test/dafny0/Compilation.dfy.expect
@@ -1,3 +1,12 @@
-Dafny program verifier finished with 46 verified, 0 errors
-Compiled assembly into Compilation.exe
+Dafny program verifier finished with 50 verified, 0 errors
+Program compiled successfully
+Running...
+
+400
+320
+40
+41
+42
+9
+9
diff --git a/Test/dafny0/ExistentialGuards.dfy b/Test/dafny0/ExistentialGuards.dfy
index 001acb55..5afb3979 100644
--- a/Test/dafny0/ExistentialGuards.dfy
+++ b/Test/dafny0/ExistentialGuards.dfy
@@ -2,12 +2,19 @@
// RUN: %diff "%s.expect" "%t"
predicate P(n: int)
+{
+ n % 2 == 0
+}
predicate R(r: real)
+{
+ 0.0 <= r
+}
method M0()
{
if x :| P(x) {
+ var y := x + 3;
}
}
@@ -19,13 +26,19 @@ method M1()
method M2()
{
- if x, y :| P(x) && R(y) {
+ var x := true;
+ if x, y :| P(x) && R(y) { // this declares a new 'x'
+ var z := x + 12;
}
+ x := x && false;
}
method M3()
{
+ var x := true;
if x: int, y :| P(x) && R(y) {
+ var z := x + y.Trunc;
+ var w := real(x) + y;
}
}
@@ -53,37 +66,94 @@ method M6()
}
}
-method M7()
+ghost method M7() returns (z: real, w: real)
+ ensures -2.0 <= z
+ ensures z == w // error: does not hold
{
+ var k;
if x :| P(x) {
+ k, z := 4, 18.0;
} else if * {
+ z := z + -z;
} else if y :| R(y) {
+ z := y;
} else if y :| P(y) {
+ k := y;
+ } else {
+ z :| R(z);
+ }
+ if P(k) {
+ z := 18.0;
+ }
+}
+
+ghost method M8(m: int, n: int)
+ requires forall y :: m <= y < n ==> P(y)
+{
+ var t := -1;
+ var u;
+ if y :| m <= y < n && P(y) {
+ u := y;
+ if * {
+ t := n - y;
+ } else if * {
+ t := y - m;
+ } else if P(y) {
+ t := 8;
+ } else {
+ t := -100; // will never happen
+ }
+ }
+ if t < 0 && m < n {
+ assert P(m) && !P(m);
+ assert false;
}
+ assert t < 0 ==> n <= m;
}
method P0(m: int, n: int)
requires m < n
{
+ ghost var even, alsoEven := 4, 8;
if {
case x :| P(x) =>
+ even := x;
case x: int :| P(x) =>
+ even := x;
case x, y :| P(x) && R(y) =>
+ even, alsoEven := x, y.Trunc; // this assigns to 'alsoEven' a possibly odd number
case x: int, y :| P(x) && R(y) =>
+ even := x;
case m < n => // just to be different
case x, y: real :| P(x) && R(y) =>
+ even := x;
case x: int, y: real :| P(x) && R(y) =>
+ even := x;
}
+ assert P(even);
+ assert P(alsoEven); // error: may not hold
}
method P1(m: int, n: int)
- requires m < n
{
+ if { // error: missing case
+ case x :| m <= x < n && P(x) =>
+ }
+}
+
+method P2(m: int, n: int)
+ requires forall y :: m <= y < n ==> P(y)
+{
+ if { // error: missing case
+ case x :| m <= x < n && P(x) =>
+ }
+}
+
+method P3(m: int, n: int)
+ requires m < n && forall y :: m <= y < n ==> P(y)
+{
+ assert P(m); // lemma that proves that the following 'if' covers all possibilities
if {
- case x {:myattribute x, "hello"} :| P(x) =>
- case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>
- case x: int {:myattribute x, "chello"} :| P(x) =>
- case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>
- case m < n =>
+ case x :| m <= x < n && P(x) =>
}
}
diff --git a/Test/dafny0/ExistentialGuards.dfy.expect b/Test/dafny0/ExistentialGuards.dfy.expect
index cf229553..21461067 100644
--- a/Test/dafny0/ExistentialGuards.dfy.expect
+++ b/Test/dafny0/ExistentialGuards.dfy.expect
@@ -3,12 +3,19 @@
// ExistentialGuards.dfy
predicate P(n: int)
+{
+ n % 2 == 0
+}
predicate R(r: real)
+{
+ 0.0 <= r
+}
method M0()
{
if x :| P(x) {
+ var y := x + 3;
}
}
@@ -20,13 +27,19 @@ method M1()
method M2()
{
+ var x := true;
if x, y :| P(x) && R(y) {
+ var z := x + 12;
}
+ x := x && false;
}
method M3()
{
+ var x := true;
if x: int, y :| P(x) && R(y) {
+ var z := x + y.Trunc;
+ var w := real(x) + y;
}
}
@@ -54,41 +67,119 @@ method M6()
}
}
-method M7()
+ghost method M7() returns (z: real, w: real)
+ ensures -2.0 <= z
+ ensures z == w
{
+ var k;
if x :| P(x) {
+ k, z := 4, 18.0;
} else if * {
+ z := z + -z;
} else if y :| R(y) {
+ z := y;
} else if y :| P(y) {
+ k := y;
+ } else {
+ z :| R(z);
+ }
+ if P(k) {
+ z := 18.0;
}
}
+ghost method M8(m: int, n: int)
+ requires forall y :: m <= y < n ==> P(y)
+{
+ var t := -1;
+ var u;
+ if y :| m <= y < n && P(y) {
+ u := y;
+ if * {
+ t := n - y;
+ } else if * {
+ t := y - m;
+ } else if P(y) {
+ t := 8;
+ } else {
+ t := -100;
+ }
+ }
+ if t < 0 && m < n {
+ assert P(m) && !P(m);
+ assert false;
+ }
+ assert t < 0 ==> n <= m;
+}
+
method P0(m: int, n: int)
requires m < n
{
+ ghost var even, alsoEven := 4, 8;
if {
case x :| P(x) =>
+ even := x;
case x: int :| P(x) =>
+ even := x;
case x, y :| P(x) && R(y) =>
+ even, alsoEven := x, y.Trunc;
case x: int, y :| P(x) && R(y) =>
+ even := x;
case m < n =>
case x, y: real :| P(x) && R(y) =>
+ even := x;
case x: int, y: real :| P(x) && R(y) =>
+ even := x;
}
+ assert P(even);
+ assert P(alsoEven);
}
method P1(m: int, n: int)
- requires m < n
{
if {
- case x {:myattribute x, "hello"} :| P(x) =>
- case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>
- case x: int {:myattribute x, "chello"} :| P(x) =>
- case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>
- case m < n =>
+ case x :| m <= x < n && P(x) =>
+ }
+}
+
+method P2(m: int, n: int)
+ requires forall y :: m <= y < n ==> P(y)
+{
+ if {
+ case x :| m <= x < n && P(x) =>
+ }
+}
+
+method P3(m: int, n: int)
+ requires m < n && forall y :: m <= y < n ==> P(y)
+{
+ assert P(m);
+ if {
+ case x :| m <= x < n && P(x) =>
}
}
+ExistentialGuards.dfy(85,10): Error BP5003: A postcondition might not hold on this return path.
+ExistentialGuards.dfy(71,12): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon12_Then
+ (0,0): anon9
+ (0,0): anon16_Then
+ExistentialGuards.dfy(134,9): Error: assertion violation
+ExistentialGuards.dfy(6,8): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon20_Then
+ (0,0): anon21_Then
+ (0,0): anon5
+ (0,0): anon17
+ExistentialGuards.dfy(139,2): Error: alternative cases fail to cover all possibilties
+Execution trace:
+ (0,0): anon0
+ (0,0): anon7_Else
+ExistentialGuards.dfy(147,2): Error: alternative cases fail to cover all possibilties
+Execution trace:
+ (0,0): anon0
+ (0,0): anon7_Else
-Dafny program verifier finished with 22 verified, 0 errors
-Compilation error: Function _module._default.P has no body
-Compilation error: Function _module._default.R has no body
+Dafny program verifier finished with 24 verified, 4 errors
diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy b/Test/dafny0/ExistentialGuardsResolution.dfy
new file mode 100644
index 00000000..8fce1de5
--- /dev/null
+++ b/Test/dafny0/ExistentialGuardsResolution.dfy
@@ -0,0 +1,154 @@
+// RUN: %dafny /dprint:- "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+predicate P(n: int)
+
+predicate R(r: real)
+
+method M0()
+{
+ if x :| P(x) {
+ var y := x + 3;
+ var x := true; // error: 'x' is already declared in this scope
+ }
+}
+
+method M1()
+{
+ if x: int :| P(x) {
+ x := x + 1; // error: 'x' is an immutable variable
+ }
+}
+
+method M2()
+{
+ var x := true;
+ if x, y :| P(x) && R(y) { // this declares a new 'x'
+ var z := x + 12;
+ }
+ x := x && false;
+}
+
+method M3()
+{
+ var x := true;
+ if x: int, y :| P(x) && R(y) {
+ var z := x + int(y);
+ var w := real(x) + y;
+ }
+ var x := 0.0; // error: 'x' is already declared in this scope
+}
+
+method M4()
+{
+ if x, y: real :| P(x) && R(y) {
+ }
+}
+
+method M5()
+{
+ if x: int, y: real :| P(x) && R(y) {
+ }
+}
+
+method M6()
+{
+ if x {:myattribute x, "hello"} :| P(x) {
+ }
+ if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+ }
+ if x: int {:myattribute x, "chello"} :| P(x) {
+ }
+ if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+ }
+}
+
+method M7()
+{
+ if x :| P(x) {
+ } else if * {
+ } else if y :| R(y) {
+ } else if y :| P(y) {
+ }
+}
+
+method P0(m: int, n: int)
+ requires m < n
+{
+ var x := true;
+ if {
+ case x :| P(x) =>
+ var t := 3 * x;
+ case x: int :| P(x) =>
+ case x, y :| P(x) && R(y) =>
+ y := y + 1.0; // error: 'y' is an immutable variable
+ case x: int, y :| P(x) && R(y) =>
+ case m < n =>
+ x := x || m + 5 == n;
+ case x, y: real :| P(x) && R(y) =>
+ case x: int, y: real :| P(x) && R(y) =>
+ }
+ assert x;
+}
+
+method P1(m: int, n: int)
+ requires m < n
+{
+ if {
+ case x {:myattribute x, "hello"} :| P(x) =>
+ case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>
+ case x: int {:myattribute x, "chello"} :| P(x) =>
+ case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>
+ case m < n =>
+ }
+}
+
+module TypesNotFullyDetermined {
+ method T0()
+ {
+ if x :| true { // error: type not entirely resolved
+ }
+ }
+ method T1()
+ {
+ if x :| true {
+ var y := x + 3;
+ }
+ }
+}
+
+module Ghost {
+ predicate P(x: int) // note, P is ghost
+ predicate method R(x: int)
+ method M7() returns (z: int, b: bool)
+ {
+ if * {
+ z := z + -z;
+ } else if y :| 1000 <= y < 2000 && R(y) {
+ z := y;
+ } else if y :| 0 <= y < 100 && P(y) {
+ z := y; // error: not allowed, because the P in the guard makes this a ghost context
+ } else if y :| 0 <= y < 100 && R(y) {
+ z := y; // error: this is also in a ghost context, because it depends on the P above
+ }
+
+ if * {
+ z := z + -z;
+ } else if exists y :: 1000 <= y < 2000 && R(y) {
+ z := 0;
+ } else if exists y :: 0 <= y < 100 && P(y) {
+ z := 0; // error: not allowed, because the P in the guard makes this a ghost context
+ } else if exists y :: 0 <= y < 100 && R(y) {
+ z := 0; // error: this is also in a ghost context, because it depends on the P above
+ }
+
+ if P(z) {
+ z := 20; // error: blatant ghost context
+ }
+
+ b := exists y :: 0 <= y < 100 && P(y); // error: assignment to non-ghost of something that depends on ghost
+ ghost var c;
+ c := exists y :: 0 <= y < 100 && P(y);
+ b := exists y {:myattribute P(y)} :: 0 <= y < 100;
+ }
+}
diff --git a/Test/dafny0/ExistentialGuardsResolution.dfy.expect b/Test/dafny0/ExistentialGuardsResolution.dfy.expect
new file mode 100644
index 00000000..681bb13d
--- /dev/null
+++ b/Test/dafny0/ExistentialGuardsResolution.dfy.expect
@@ -0,0 +1,167 @@
+// Dafny program verifier version 1.9.5.20511, Copyright (c) 2003-2015, Microsoft.
+// Command Line Options: -nologo -countVerificationErrors:0 -useBaseNameForFileName /dprint:- C:\dafny\Test\dafny0\ExistentialGuardsResolution.dfy
+// ExistentialGuardsResolution.dfy
+
+
+module TypesNotFullyDetermined {
+ method T0()
+ {
+ if x :| true {
+ }
+ }
+
+ method T1()
+ {
+ if x :| true {
+ var y := x + 3;
+ }
+ }
+}
+
+module Ghost {
+ predicate P(x: int)
+
+ predicate method R(x: int)
+
+ method M7() returns (z: int, b: bool)
+ {
+ if * {
+ z := z + -z;
+ } else if y :| 1000 <= y < 2000 && R(y) {
+ z := y;
+ } else if y :| 0 <= y < 100 && P(y) {
+ z := y;
+ } else if y :| 0 <= y < 100 && R(y) {
+ z := y;
+ }
+ if * {
+ z := z + -z;
+ } else if exists y :: 1000 <= y < 2000 && R(y) {
+ z := 0;
+ } else if exists y :: 0 <= y < 100 && P(y) {
+ z := 0;
+ } else if exists y :: 0 <= y < 100 && R(y) {
+ z := 0;
+ }
+ if P(z) {
+ z := 20;
+ }
+ b := exists y :: 0 <= y < 100 && P(y);
+ ghost var c;
+ c := exists y :: 0 <= y < 100 && P(y);
+ b := exists y {:myattribute P(y)} :: 0 <= y < 100;
+ }
+}
+predicate P(n: int)
+
+predicate R(r: real)
+
+method M0()
+{
+ if x :| P(x) {
+ var y := x + 3;
+ var x := true;
+ }
+}
+
+method M1()
+{
+ if x: int :| P(x) {
+ x := x + 1;
+ }
+}
+
+method M2()
+{
+ var x := true;
+ if x, y :| P(x) && R(y) {
+ var z := x + 12;
+ }
+ x := x && false;
+}
+
+method M3()
+{
+ var x := true;
+ if x: int, y :| P(x) && R(y) {
+ var z := x + int(y);
+ var w := real(x) + y;
+ }
+ var x := 0.0;
+}
+
+method M4()
+{
+ if x, y: real :| P(x) && R(y) {
+ }
+}
+
+method M5()
+{
+ if x: int, y: real :| P(x) && R(y) {
+ }
+}
+
+method M6()
+{
+ if x {:myattribute x, "hello"} :| P(x) {
+ }
+ if x, y {:myattribute y, "sveika"} :| P(x) && R(y) {
+ }
+ if x: int {:myattribute x, "chello"} :| P(x) {
+ }
+ if x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) {
+ }
+}
+
+method M7()
+{
+ if x :| P(x) {
+ } else if * {
+ } else if y :| R(y) {
+ } else if y :| P(y) {
+ }
+}
+
+method P0(m: int, n: int)
+ requires m < n
+{
+ var x := true;
+ if {
+ case x :| P(x) =>
+ var t := 3 * x;
+ case x: int :| P(x) =>
+ case x, y :| P(x) && R(y) =>
+ y := y + 1.0;
+ case x: int, y :| P(x) && R(y) =>
+ case m < n =>
+ x := x || m + 5 == n;
+ case x, y: real :| P(x) && R(y) =>
+ case x: int, y: real :| P(x) && R(y) =>
+ }
+ assert x;
+}
+
+method P1(m: int, n: int)
+ requires m < n
+{
+ if {
+ case x {:myattribute x, "hello"} :| P(x) =>
+ case x, y {:myattribute y, "sveika"} :| P(x) && R(y) =>
+ case x: int {:myattribute x, "chello"} :| P(x) =>
+ case x {:myattribute x, "hola"} {:yourattribute x + x, "hej"} :| P(x) =>
+ case m < n =>
+ }
+}
+ExistentialGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly
+ExistentialGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ExistentialGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ExistentialGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ExistentialGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ExistentialGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ExistentialGuardsResolution.dfy(149,37): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ExistentialGuardsResolution.dfy(12,8): Error: Duplicate local-variable name: x
+ExistentialGuardsResolution.dfy(19,4): Error: LHS of assignment must denote a mutable variable
+ExistentialGuardsResolution.dfy(39,6): Error: Duplicate local-variable name: x
+ExistentialGuardsResolution.dfy(84,6): Error: LHS of assignment must denote a mutable variable
+11 resolution/type errors detected in ExistentialGuardsResolution.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index e935c83d..58ba6701 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1692,3 +1692,23 @@ module LoopResolutionTests {
}
}
}
+
+module UnderspecifiedTypesInAttributes {
+ function method P<T>(x: T): int
+ method M() {
+ var {:myattr var u :| true; 6} v: int; // error: type of u is underspecified
+ var j {:myattr var u :| true; 6} :| 0 <= j < 100; // error: type of u is underspecified
+
+ var a := new int[100];
+ forall lp {:myattr var u :| true; 6} | 0 <= lp < 100 { // error: type of u is underspecified
+ a[lp] := 0;
+ }
+
+ modify {:myattr P(10)} {:myattr var u :| true; 6} a; // error: type of u is underspecified
+
+ calc {:myattr P(10)} {:myattr var u :| true; 6} // error: type of u is underspecified
+ {
+ 5;
+ }
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index be19eeac..b055184f 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -161,6 +161,11 @@ ResolutionErrors.dfy(1673,4): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(1677,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(1687,4): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(1691,29): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(1699,17): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1700,19): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1703,23): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1707,36): Error: the type of the bound variable 'u' could not be determined
+ResolutionErrors.dfy(1709,34): Error: the type of the bound variable 'u' could not be determined
ResolutionErrors.dfy(469,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
@@ -224,4 +229,4 @@ ResolutionErrors.dfy(1123,8): Error: new cannot be applied to a trait
ResolutionErrors.dfy(1144,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1151,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1166,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-226 resolution/type errors detected in ResolutionErrors.dfy
+231 resolution/type errors detected in ResolutionErrors.dfy
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 21:21:58 +0000