diff options
| author |  Rustan Leino <unknown> | 2013-04-01 14:28:37 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-04-01 14:28:37 -0700 |
| commit | 7ee036cae0cc6a2d48786f18908f26de37136236 (patch) | |
| tree | d8e3965854d7499f754551695f694cee8a7acbe5 | |
| parent | 5152d9cd2fd4cd7258d745ec01324b4b654e1172 (diff) | |
Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, where more type information is known
Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement.
Fixed numerous places where some recursive checks did not reach.
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 65 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 411 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 8 | ||||
| -rw-r--r-- | Test/VSComp2010/Problem4-Queens.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 10 | ||||
| -rw-r--r-- | Test/dafny0/Basics.dfy | 1 | ||||
| -rw-r--r-- | Test/dafny0/Maps.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 16 | ||||
| -rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 8 |
9 files changed, 310 insertions, 221 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 7a6871c7..3ac7b11c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2506,7 +2506,7 @@ namespace Microsoft.Dafny { /// <summary>
/// Common superclass of UpdateStmt and AssignSuchThatStmt.
/// </summary>
- public abstract class ConcreteUpdateStatement : ConcreteSyntaxStatement
+ public abstract class ConcreteUpdateStatement : Statement
{
public readonly List<Expression> Lhss;
public ConcreteUpdateStatement(IToken tok, List<Expression> lhss)
@@ -2556,6 +2556,12 @@ namespace Microsoft.Dafny { {
public readonly List<AssignmentRhs> Rhss;
public readonly bool CanMutateKnownState;
+
+ public List<Statement> ResolvedStatements = new List<Statement>(); // contents filled in during resolution
+ public override IEnumerable<Statement> SubStatements {
+ get { return ResolvedStatements; }
+ }
+
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(Lhss));
@@ -3060,6 +3066,13 @@ namespace Microsoft.Dafny { var block = s as BlockStmt;
if (block != null && block.Body.Count == 1) {
s = block.Body[0];
+ } else if (s is UpdateStmt) {
+ var update = (UpdateStmt)s;
+ if (update.ResolvedStatements.Count == 1) {
+ s = update.ResolvedStatements[0];
+ } else {
+ return s;
+ }
} else {
var conc = s as ConcreteSyntaxStatement;
if (conc != null && conc.ResolvedStatements.Count == 1) {
@@ -3294,7 +3307,13 @@ namespace Microsoft.Dafny { {
get {
foreach (var l in Lines) {
- yield return l;
+ yield return l;
+ }
+ foreach (var e in Steps) {
+ yield return e;
+ }
+ if (Result != null) {
+ yield return Result;
}
}
}
@@ -3744,6 +3763,14 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(elements));
Elements = elements;
}
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ foreach (var ep in Elements) {
+ yield return ep.A;
+ yield return ep.B;
+ }
+ }
+ }
}
public class SeqDisplayExpr : DisplayExpression {
public SeqDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements)
@@ -4027,6 +4054,8 @@ namespace Microsoft.Dafny { }
public readonly Opcode Op;
public enum ResolvedOpcode {
+ YetUndetermined, // the value before resolution has determined the value; .ResolvedOp should never be read in this state
+
// logical operators
Iff,
Imp,
@@ -4090,7 +4119,20 @@ namespace Microsoft.Dafny { RankLt,
RankGt
}
- public ResolvedOpcode ResolvedOp; // filled in by resolution
+ private ResolvedOpcode _theResolvedOp = ResolvedOpcode.YetUndetermined;
+ public ResolvedOpcode ResolvedOp {
+ set {
+ Contract.Assume(_theResolvedOp == ResolvedOpcode.YetUndetermined || _theResolvedOp == value); // there's never a reason for resolution to change its mind, is there?
+ _theResolvedOp = value;
+ }
+ get {
+ Contract.Assume(_theResolvedOp != ResolvedOpcode.YetUndetermined); // shouldn't read it until it has been properly initialized
+ return _theResolvedOp;
+ }
+ }
+ public ResolvedOpcode ResolvedOp_PossiblyStillUndetermined { // offer a way to return _theResolveOp -- for experts only!
+ get { return _theResolvedOp; }
+ }
public static Opcode ResolvedOp2SyntacticOp(ResolvedOpcode rop) {
switch (rop) {
@@ -4360,7 +4402,11 @@ namespace Microsoft.Dafny { public readonly Attributes Attributes;
- public abstract class BoundedPool { }
+ public abstract class BoundedPool {
+ public virtual bool IsFinite {
+ get { return true; } // most bounds are finite
+ }
+ }
public class BoolBoundedPool : BoundedPool
{
}
@@ -4372,6 +4418,11 @@ namespace Microsoft.Dafny { LowerBound = lowerBound;
UpperBound = upperBound;
}
+ public override bool IsFinite {
+ get {
+ return LowerBound != null && UpperBound != null;
+ }
+ }
}
public class SetBoundedPool : BoundedPool
{
@@ -4581,10 +4632,8 @@ namespace Microsoft.Dafny { public override IEnumerable<Expression> SubExpressions {
get {
- // NadiaToDo: is this correct?
- foreach (var e in Guard.SubExpressions) {
- yield return e;
- }
+ // Note: A CalcExpr is unusual in that it contains a statement. For now, callers
+ // of SubExpressions need to be aware of this and hand it specially.
yield return Body;
}
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index bab0aca7..8e1fbff4 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1178,6 +1178,22 @@ namespace Microsoft.Dafny }
if (ErrorCount == prevErrorCount) {
+ // Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions
+ foreach (TopLevelDecl d in declarations) {
+ if (d is IteratorDecl) {
+ var iter = (IteratorDecl)d;
+ iter.Members.Iter(CheckTypeInference_Member);
+ if (iter.Body != null) {
+ CheckTypeInference(iter.Body);
+ }
+ } else if (d is ClassDecl) {
+ var cl = (ClassDecl)d;
+ cl.Members.Iter(CheckTypeInference_Member);
+ }
+ }
+ }
+
+ if (ErrorCount == prevErrorCount) {
// fill in the postconditions and bodies of prefix methods
foreach (var com in ModuleDefinition.AllCoMethods(declarations)) {
var prefixMethod = com.PrefixMethod;
@@ -1211,58 +1227,7 @@ namespace Microsoft.Dafny ResolveMethod(prefixMethod);
allTypeParameters.PopMarker();
currentClass = null;
- }
-
- foreach (TopLevelDecl d in declarations) {
- if (d is ClassDecl) {
- foreach (var member in ((ClassDecl)d).Members) {
- if (member is Method) {
- var m = (Method)member;
- m.Req.Iter(mfe => CheckTypeInference(mfe.E));
- m.Ens.Iter(mfe => CheckTypeInference(mfe.E));
- m.Mod.Expressions.Iter(fe => CheckTypeInference(fe.E));
- m.Decreases.Expressions.Iter(CheckTypeInference);
- if (m.Body != null) {
- CheckTypeInference(m.Body);
- bool tail = true;
- bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);
- if (hasTailRecursionPreference && !tail) {
- // the user specifically requested no tail recursion, so do nothing else
- } else if (hasTailRecursionPreference && tail && m.IsGhost) {
- Error(m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods");
- } else {
- var module = m.EnclosingClass.Module;
- var sccSize = module.CallGraph.GetSCCSize(m);
- if (hasTailRecursionPreference && 2 <= sccSize) {
- Error(m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods");
- } else if (hasTailRecursionPreference || sccSize == 1) {
- CallStmt tailCall = null;
- var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
- if (status != TailRecursionStatus.NotTailRecursive) {
- m.IsTailRecursive = true;
- }
- }
- }
- }
- if (!m.IsTailRecursive && m.Body != null && Contract.Exists(m.Decreases.Expressions, e => e is WildcardExpr)) {
- Error(m.Decreases.Expressions[0].tok, "'decreases *' is allowed only on tail-recursive methods");
- }
- } else if (member is Function) {
- var f = (Function)member;
- f.Req.Iter(CheckTypeInference);
- f.Ens.Iter(CheckTypeInference);
- f.Reads.Iter(fe => CheckTypeInference(fe.E));
- f.Decreases.Expressions.Iter(CheckTypeInference);
- if (f.Body != null) {
- CheckTypeInference(f.Body);
- bool tail = true;
- if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) {
- Error(f.tok, "sorry, tail-call functions are not supported");
- }
- }
- }
- }
- }
+ CheckTypeInference_Member(prefixMethod);
}
}
@@ -1492,6 +1457,54 @@ namespace Microsoft.Dafny }
}
+ private void CheckTypeInference_Member(MemberDecl member) {
+ if (member is Method) {
+ var m = (Method)member;
+ m.Req.Iter(mfe => CheckTypeInference(mfe.E));
+ m.Ens.Iter(mfe => CheckTypeInference(mfe.E));
+ m.Mod.Expressions.Iter(fe => CheckTypeInference(fe.E));
+ m.Decreases.Expressions.Iter(CheckTypeInference);
+ if (m.Body != null) {
+ CheckTypeInference(m.Body);
+ bool tail = true;
+ bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);
+ if (hasTailRecursionPreference && !tail) {
+ // the user specifically requested no tail recursion, so do nothing else
+ } else if (hasTailRecursionPreference && tail && m.IsGhost) {
+ Error(m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods");
+ } else {
+ var module = m.EnclosingClass.Module;
+ var sccSize = module.CallGraph.GetSCCSize(m);
+ if (hasTailRecursionPreference && 2 <= sccSize) {
+ Error(m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods");
+ } else if (hasTailRecursionPreference || sccSize == 1) {
+ CallStmt tailCall = null;
+ var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
+ if (status != TailRecursionStatus.NotTailRecursive) {
+ m.IsTailRecursive = true;
+ }
+ }
+ }
+ }
+ if (!m.IsTailRecursive && m.Body != null && Contract.Exists(m.Decreases.Expressions, e => e is WildcardExpr)) {
+ Error(m.Decreases.Expressions[0].tok, "'decreases *' is allowed only on tail-recursive methods");
+ }
+ } else if (member is Function) {
+ var f = (Function)member;
+ f.Req.Iter(CheckTypeInference);
+ f.Ens.Iter(CheckTypeInference);
+ f.Reads.Iter(fe => CheckTypeInference(fe.E));
+ f.Decreases.Expressions.Iter(CheckTypeInference);
+ if (f.Body != null) {
+ CheckTypeInference(f.Body);
+ bool tail = true;
+ if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) {
+ Error(f.tok, "sorry, tail-call functions are not supported");
+ }
+ }
+ }
+ }
+
enum TailRecursionStatus
{
NotTailRecursive, // contains code that makes the enclosing method body not tail recursive (in way that is supported)
@@ -1649,6 +1662,9 @@ namespace Microsoft.Dafny }
return status;
} else if (stmt is AssignSuchThatStmt) {
+ } else if (stmt is UpdateStmt) {
+ var s = (UpdateStmt)stmt;
+ return CheckTailRecursive(s.ResolvedStatements, enclosingMethod, ref tailCall, reportErrors);
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
return CheckTailRecursive(s.ResolvedStatements, enclosingMethod, ref tailCall, reportErrors);
@@ -1850,6 +1866,12 @@ namespace Microsoft.Dafny foreach (MatchCaseStmt mc in s.Cases) {
mc.Body.Iter(CheckEqualityTypes_Stmt);
}
+ } else if (stmt is AssignSuchThatStmt) {
+ var s = (AssignSuchThatStmt)stmt;
+ s.SubExpressions.Iter(CheckEqualityTypes);
+ } else if (stmt is UpdateStmt) {
+ var s = (UpdateStmt)stmt;
+ s.ResolvedStatements.Iter(CheckEqualityTypes_Stmt);
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
s.ResolvedStatements.Iter(CheckEqualityTypes_Stmt);
@@ -1931,6 +1953,10 @@ namespace Microsoft.Dafny }
i++;
}
+ } else if (expr is CalcExpr) {
+ // a calc expression also contains statements
+ var e = (CalcExpr)expr;
+ CheckEqualityTypes_Stmt(e.Guard);
}
foreach (var ee in expr.SubExpressions) {
@@ -1992,101 +2018,51 @@ namespace Microsoft.Dafny }
}
- void CheckTypeIsDetermined(IToken tok, Type t, string what) {
+ bool CheckTypeIsDetermined(IToken tok, Type t, string what) {
Contract.Requires(tok != null);
Contract.Requires(t != null);
Contract.Requires(what != null);
t = t.Normalize();
if (t is TypeProxy && !(t is InferredTypeProxy || t is ParamTypeProxy || t is ObjectTypeProxy)) {
Error(tok, "the type of this {0} is underspecified, but it cannot be an arbitrary type.", what);
+ return false;
}
+ return true;
}
- void CheckTypeInference(Expression e) {
- if (e == null) return;
- e.SubExpressions.Iter(CheckTypeInference);
- var ce = e as ComprehensionExpr;
- if (ce != null) {
- foreach (var bv in ce.BoundVars) {
- if (bv.Type.Normalize() is TypeProxy) {
- Error(bv.tok, "type of bound variable '{0}' could not determined; please specify the type explicitly", bv.Name);
+ void CheckTypeInference(Expression expr) {
+ if (expr == null) return;
+ expr.SubExpressions.Iter(CheckTypeInference);
+ if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ if (e != null) {
+ foreach (var bv in e.BoundVars) {
+ if (bv.Type.Normalize() is TypeProxy) {
+ Error(bv.tok, "type of bound variable '{0}' could not determined; please specify the type explicitly", bv.Name);
+ }
}
}
+ } else if (expr is CalcExpr) {
+ // a calc expression also contains statements
+ var e = (CalcExpr)expr;
+ CheckTypeInference(e.Guard);
+ }
+ if (CheckTypeIsDetermined(expr.tok, expr.Type, "expression")) {
+ var bin = expr as BinaryExpr;
+ if (bin != null) {
+ bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type);
+ }
}
- CheckTypeIsDetermined(e.tok, e.Type, "expression");
}
void CheckTypeInference(Statement stmt) {
Contract.Requires(stmt != null);
- if (stmt is PrintStmt) {
- var s = (PrintStmt)stmt;
- s.Args.Iter(arg => CheckTypeInference(arg.E));
- } else if (stmt is BreakStmt) {
- } else if (stmt is ProduceStmt) {
- var s = (ProduceStmt)stmt;
- if (s.rhss != null) {
- s.rhss.Iter(rhs => rhs.SubExpressions.Iter(e => CheckTypeInference(e)));
- }
- } else if (stmt is AssignStmt) {
- AssignStmt s = (AssignStmt)stmt;
- CheckTypeInference(s.Lhs);
- s.Rhs.SubExpressions.Iter(e => { CheckTypeInference(e); });
- } else if (stmt is VarDecl) {
+ stmt.SubExpressions.Iter(CheckTypeInference);
+ stmt.SubStatements.Iter(CheckTypeInference);
+ if (stmt is VarDecl) {
var s = (VarDecl)stmt;
- s.SubStatements.Iter(CheckTypeInference);
CheckTypeIsDetermined(s.Tok, s.Type, "local variable");
- } else if (stmt is CallStmt) {
- var s = (CallStmt)stmt;
- CheckTypeInference(s.Receiver);
- s.Args.Iter(e => CheckTypeInference(e));
- s.Lhs.Iter(e => CheckTypeInference(e));
- } else if (stmt is BlockStmt) {
- var s = (BlockStmt)stmt;
- s.Body.Iter(CheckTypeInference);
- } else if (stmt is IfStmt) {
- var s = (IfStmt)stmt;
- if (s.Guard != null) {
- CheckTypeInference(s.Guard);
- }
- s.SubStatements.Iter(CheckTypeInference);
- } else if (stmt is AlternativeStmt) {
- var s = (AlternativeStmt)stmt;
- foreach (var alt in s.Alternatives) {
- CheckTypeInference(alt.Guard);
- alt.Body.Iter(CheckTypeInference);
- }
- } else if (stmt is WhileStmt) {
- var s = (WhileStmt)stmt;
- if (s.Guard != null) {
- CheckTypeInference(s.Guard);
- }
- CheckTypeInference(s.Body);
- } else if (stmt is AlternativeLoopStmt) {
- var s = (AlternativeLoopStmt)stmt;
- foreach (var alt in s.Alternatives) {
- CheckTypeInference(alt.Guard);
- alt.Body.Iter(CheckTypeInference);
- }
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
- CheckTypeInference(s.Range);
- CheckTypeInference(s.Body);
s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));
- } else if (stmt is CalcStmt) {
- var s = (CalcStmt)stmt;
- s.SubExpressions.Iter(e => CheckTypeInference(e));
- s.SubStatements.Iter(CheckTypeInference);
- } else if (stmt is MatchStmt) {
- var s = (MatchStmt)stmt;
- CheckTypeInference(s.Source);
- foreach (MatchCaseStmt mc in s.Cases) {
- mc.Body.Iter(CheckTypeInference);
- }
- } else if (stmt is ConcreteSyntaxStatement) {
- var s = (ConcreteSyntaxStatement)stmt;
- s.ResolvedStatements.Iter(CheckTypeInference);
- } else if (stmt is PredicateStmt) {
- CheckTypeInference(((PredicateStmt)stmt).Expr);
- } else {
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
}
}
@@ -3587,7 +3563,7 @@ namespace Microsoft.Dafny s.hiddenUpdate = null;
}
} else if (stmt is ConcreteUpdateStatement) {
- ResolveUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);
+ ResolveConcreteUpdateStmt((ConcreteUpdateStatement)stmt, specContextOnly, codeContext);
} else if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
foreach (var vd in s.Lhss) {
@@ -3842,6 +3818,7 @@ namespace Microsoft.Dafny bool bodyMustBeSpecOnly = specContextOnly || (prevErrorCount == ErrorCount && UsesSpecFeatures(s.Range));
if (!bodyMustBeSpecOnly && prevErrorCount == ErrorCount) {
var missingBounds = new List<BoundVar>();
+ CheckTypeInference(s.Range); // we need to resolve operators before the call to DiscoverBounds
s.Bounds = DiscoverBounds(s.Tok, s.BoundVars, s.Range, true, false, missingBounds);
if (missingBounds.Count != 0) {
bodyMustBeSpecOnly = true;
@@ -4037,37 +4014,57 @@ namespace Microsoft.Dafny Contract.Assert(false); throw new cce.UnreachableException();
}
}
- private void ResolveUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, ICodeContext codeContext) {
+ private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, bool specContextOnly, ICodeContext codeContext) {
Contract.Requires(codeContext != null);
- int prevErrorCount = ErrorCount;
// First, resolve all LHS's and expression-looking RHS's.
+ int errorCountBeforeCheckingLhs = ErrorCount;
var update = s as UpdateStmt;
+ var lhsNameSet = new Dictionary<string, object>(); // used to check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)
foreach (var lhs in s.Lhss) {
var ec = ErrorCount;
ResolveExpression(lhs, true, codeContext);
- if (update == null && ec == ErrorCount && specContextOnly && !AssignStmt.LhsIsToGhost(lhs)) {
- Error(lhs, "cannot assign to non-ghost variable in a ghost context");
- }
- if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
- Error(lhs, "cannot assign to a range of array elements (try the 'forall' statement)");
+ if (ec == ErrorCount) {
+ if (update == null && specContextOnly && !AssignStmt.LhsIsToGhost(lhs)) {
+ Error(lhs, "cannot assign to non-ghost variable in a ghost context");
+ }
+ if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
+ Error(lhs, "cannot assign to a range of array elements (try the 'forall' statement)");
+ }
+ var ie = lhs.Resolved as IdentifierExpr;
+ if (ie != null) {
+ if (lhsNameSet.ContainsKey(ie.Name)) {
+ Error(update, "duplicate variable in left-hand side of call statement: {0}", ie.Name);
+ } else {
+ lhsNameSet.Add(ie.Name, null);
+ }
+ }
}
}
+
// Resolve RHSs
if (update == null) {
var suchThat = (AssignSuchThatStmt)s; // this is the other possible subclass
ResolveAssignSuchThatStmt(suchThat, specContextOnly, codeContext);
- return;
- }
-
+ } else {
+ ResolveUpdateStmt(update, specContextOnly, codeContext, errorCountBeforeCheckingLhs);
+ }
+ }
+ /// <summary>
+ /// Resolve the RHSs and entire UpdateStmt (LHSs should already have been checked by the caller).
+ /// errorCountBeforeCheckingLhs is passed in so that this method can determined if any resolution errors were found during
+ /// LHS or RHS checking, because only if no errors were found is update.ResolvedStmt changed.
+ /// </summary>
+ private void ResolveUpdateStmt(UpdateStmt update, bool specContextOnly, ICodeContext codeContext, int errorCountBeforeCheckingLhs) {
+ Contract.Requires(update != null);
IToken firstEffectfulRhs = null;
CallRhs callRhs = null;
foreach (var rhs in update.Rhss) {
bool isEffectful;
if (rhs is TypeRhs) {
var tr = (TypeRhs)rhs;
- ResolveTypeRhs(tr, s, specContextOnly, codeContext);
+ ResolveTypeRhs(tr, update, specContextOnly, codeContext);
isEffectful = tr.InitCall != null;
} else if (rhs is HavocRhs) {
isEffectful = false;
@@ -4094,34 +4091,24 @@ namespace Microsoft.Dafny firstEffectfulRhs = rhs.Tok;
}
}
- // syntactically disallow duplicate LHSs for call statements
- if (callRhs != null) {
- // check for duplicate identifiers on the left (full duplication checking for references and the like is done during verification)
- var lhsNameSet = new Dictionary<string, object>();
- foreach (var lhs in s.Lhss) {
- var ie = lhs.Resolved as IdentifierExpr;
- if (ie != null) {
- if (lhsNameSet.ContainsKey(ie.Name)) {
- Error(s, "duplicate variable in left-hand side of call statement: {0}", ie.Name);
- } else {
- lhsNameSet.Add(ie.Name, null);
- }
- }
- }
+ var resolvedStatements = update.ResolvedStatements;
+ if (ErrorCount != errorCountBeforeCheckingLhs) {
+ // Errors occurs, so don't populate the real update.ResolvedStatements. Instead, create a placebo.
+ resolvedStatements = new List<Statement>();
}
// figure out what kind of UpdateStmt this is
if (firstEffectfulRhs == null) {
- if (s.Lhss.Count == 0) {
+ if (update.Lhss.Count == 0) {
Contract.Assert(update.Rhss.Count == 1); // guaranteed by the parser
- Error(s, "expected method call, found expression");
- } else if (s.Lhss.Count != update.Rhss.Count) {
- Error(s, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count);
- } else if (ErrorCount == prevErrorCount) {
+ Error(update, "expected method call, found expression");
+ } else if (update.Lhss.Count != update.Rhss.Count) {
+ Error(update, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", update.Lhss.Count, update.Rhss.Count);
+ } else {
// add the statements here in a sequence, but don't use that sequence later for translation (instead, should translated properly as multi-assignment)
- for (int i = 0; i < s.Lhss.Count; i++) {
- var a = new AssignStmt(s.Tok, s.Lhss[i].Resolved, update.Rhss[i]);
- s.ResolvedStatements.Add(a);
+ for (int i = 0; i < update.Lhss.Count; i++) {
+ var a = new AssignStmt(update.Tok, update.Lhss[i].Resolved, update.Rhss[i]);
+ resolvedStatements.Add(a);
}
}
@@ -4139,9 +4126,10 @@ namespace Microsoft.Dafny Contract.Assert(tr.InitCall != null); // there were effects, so this must have been a call.
if (tr.CanAffectPreviouslyKnownExpressions) {
Error(tr.Tok, "can only have initialization methods which modify at most 'this'.");
+ } else {
+ var a = new AssignStmt(update.Tok, update.Lhss[0].Resolved, tr);
+ resolvedStatements.Add(a);
}
- var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, tr);
- s.ResolvedStatements.Add(a);
}
}
@@ -4151,30 +4139,28 @@ namespace Microsoft.Dafny Error(firstEffectfulRhs, "an update statement is allowed an effectful RHS only if there is just one RHS");
} else if (callRhs == null) {
// must be a single TypeRhs
- if (s.Lhss.Count != 1) {
- Contract.Assert(2 <= s.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
- Error(s.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", s.Lhss.Count, update.Rhss.Count);
- } else if (ErrorCount == prevErrorCount) {
- var a = new AssignStmt(s.Tok, s.Lhss[0].Resolved, update.Rhss[0]);
- s.ResolvedStatements.Add(a);
+ if (update.Lhss.Count != 1) {
+ Contract.Assert(2 <= update.Lhss.Count); // the parser allows 0 Lhss only if the whole statement looks like an expression (not a TypeRhs)
+ Error(update.Lhss[1].tok, "the number of left-hand sides ({0}) and right-hand sides ({1}) must match for a multi-assignment", update.Lhss.Count, update.Rhss.Count);
+ } else {
+ var a = new AssignStmt(update.Tok, update.Lhss[0].Resolved, update.Rhss[0]);
+ resolvedStatements.Add(a);
}
} else {
// a call statement
- if (ErrorCount == prevErrorCount) {
- var resolvedLhss = new List<Expression>();
- foreach (var ll in s.Lhss) {
- resolvedLhss.Add(ll.Resolved);
- }
- var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
- s.ResolvedStatements.Add(a);
+ var resolvedLhss = new List<Expression>();
+ foreach (var ll in update.Lhss) {
+ resolvedLhss.Add(ll.Resolved);
}
+ var a = new CallStmt(callRhs.Tok, resolvedLhss, callRhs.Receiver, callRhs.MethodName, callRhs.Args);
+ resolvedStatements.Add(a);
}
}
- foreach (var a in s.ResolvedStatements) {
+ foreach (var a in update.ResolvedStatements) {
ResolveStatement(a, specContextOnly, codeContext);
}
- s.IsGhost = s.ResolvedStatements.TrueForAll(ss => ss.IsGhost);
+ update.IsGhost = update.ResolvedStatements.TrueForAll(ss => ss.IsGhost);
}
private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, bool specContextOnly, ICodeContext codeContext) {
@@ -4200,6 +4186,7 @@ namespace Microsoft.Dafny CheckIsNonGhost(s.Expr);
var missingBounds = new List<IVariable>();
+ CheckTypeInference(s.Expr); // we need to resolve operators before the call to DiscoverBoundsAux
var allBounds = DiscoverBoundsAux(s.Tok, varLhss, s.Expr, true, true, missingBounds);
if (missingBounds.Count != 0) {
s.MissingBounds = missingBounds; // so that an error message can be produced during compilation
@@ -4457,6 +4444,11 @@ namespace Microsoft.Dafny foreach (var lhs in s.Lhss) {
CheckForallStatementBodyLhs(s.Tok, lhs.Resolved, kind);
}
+ } else if (stmt is UpdateStmt) {
+ var s = (UpdateStmt)stmt;
+ foreach (var ss in s.ResolvedStatements) {
+ CheckForallStatementBodyRestrictions(ss, kind);
+ }
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
foreach (var ss in s.ResolvedStatements) {
@@ -4607,6 +4599,11 @@ namespace Microsoft.Dafny if (s.Method.Mod.Expressions.Count != 0) {
Error(stmt, "calls to methods with side-effects are not allowed inside a hint");
}
+ } else if (stmt is UpdateStmt) {
+ var s = (UpdateStmt)stmt;
+ foreach (var ss in s.ResolvedStatements) {
+ CheckHintRestrictions(ss);
+ }
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
foreach (var ss in s.ResolvedStatements) {
@@ -5287,12 +5284,16 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Le:
case BinaryExpr.Opcode.Add: {
if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) {
- if (!UnifyTypes(e.E1.Type, new DatatypeProxy(false))) {
+ if (UnifyTypes(e.E1.Type, new DatatypeProxy(false))) {
+ e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt;
+ } else {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
} else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsIndDatatype) {
- if (!UnifyTypes(e.E0.Type, new DatatypeProxy(false))) {
+ if (UnifyTypes(e.E0.Type, new DatatypeProxy(false))) {
+ e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankLt;
+ } else {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
}
expr.Type = Type.Bool;
@@ -5320,10 +5321,19 @@ namespace Microsoft.Dafny case BinaryExpr.Opcode.Gt:
case BinaryExpr.Opcode.Ge: {
if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) {
- if (!UnifyTypes(e.E1.Type, new DatatypeProxy(false))) {
+ if (UnifyTypes(e.E1.Type, new DatatypeProxy(false))) {
+ e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt;
+ } else {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
+ } else if (e.Op == BinaryExpr.Opcode.Gt && e.E1.Type.IsIndDatatype) {
+ if (UnifyTypes(e.E0.Type, new DatatypeProxy(false))) {
+ e.ResolvedOp = BinaryExpr.ResolvedOpcode.RankGt;
+ } else {
+ Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
+ }
+ expr.Type = Type.Bool;
} else {
bool err = false;
if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false))) {
@@ -5365,7 +5375,8 @@ namespace Microsoft.Dafny default:
Contract.Assert(false); throw new cce.UnreachableException(); // unexpected operator
}
- e.ResolvedOp = ResolveOp(e.Op, e.E1.Type);
+ // We should also fill in e.ResolvedOp, but we may not have enough information for that yet. So, instead, delay
+ // setting e.ResolvedOp until inside CheckTypeInference.
} else if (expr is TernaryExpr) {
var e = (TernaryExpr)expr;
@@ -5471,6 +5482,7 @@ namespace Microsoft.Dafny if (prevErrorCount == ErrorCount) {
var missingBounds = new List<BoundVar>();
+ CheckTypeInference(e.LogicalBody()); // we need to resolve operators before the call to DiscoverBounds
e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.LogicalBody(), e is ExistsExpr, false, missingBounds);
if (missingBounds.Count != 0) {
// Report errors here about quantifications that depend on the allocation state.
@@ -5515,6 +5527,7 @@ namespace Microsoft.Dafny if (prevErrorCount == ErrorCount) {
var missingBounds = new List<BoundVar>();
+ CheckTypeInference(e.Range); // we need to resolve operators before the call to DiscoverBounds
e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);
if (missingBounds.Count != 0) {
e.MissingBounds = missingBounds;
@@ -5551,6 +5564,7 @@ namespace Microsoft.Dafny if (prevErrorCount == ErrorCount) {
var missingBounds = new List<BoundVar>();
+ CheckTypeInference(e.Range); // we need to resolve operators before the call to DiscoverBounds
e.Bounds = DiscoverBounds(e.tok, e.BoundVars, e.Range, true, false, missingBounds);
if (missingBounds.Count != 0) {
e.MissingBounds = missingBounds;
@@ -5883,7 +5897,7 @@ namespace Microsoft.Dafny } else if (expr is BinaryExpr) {
var e = (BinaryExpr)expr;
- switch (e.ResolvedOp) {
+ switch (e.ResolvedOp_PossiblyStillUndetermined) {
case BinaryExpr.ResolvedOpcode.RankGt:
case BinaryExpr.ResolvedOpcode.RankLt:
Error(expr, "rank comparisons are allowed only in specification and ghost contexts");
@@ -6628,13 +6642,19 @@ namespace Microsoft.Dafny if (b != null) {
bool breakDownFurther = false;
bool p0 = polarity;
- if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.And) {
- breakDownFurther = polarity;
- } else if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.Or) {
- breakDownFurther = !polarity;
- } else if (b.ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
- breakDownFurther = !polarity;
- p0 = !p0;
+ switch (b.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.And:
+ breakDownFurther = polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.Or:
+ breakDownFurther = !polarity;
+ break;
+ case BinaryExpr.ResolvedOpcode.Imp:
+ breakDownFurther = !polarity;
+ p0 = !p0;
+ break;
+ default:
+ break;
}
if (breakDownFurther) {
foreach (var c in NormalizedConjuncts(b.E0, p0)) {
@@ -7058,10 +7078,13 @@ namespace Microsoft.Dafny return UsesSpecFeatures(e.E);
} else if (expr is BinaryExpr) {
BinaryExpr e = (BinaryExpr)expr;
- if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.RankLt || e.ResolvedOp == BinaryExpr.ResolvedOpcode.RankGt) {
- return true;
+ switch (e.ResolvedOp_PossiblyStillUndetermined) {
+ case BinaryExpr.ResolvedOpcode.RankGt:
+ case BinaryExpr.ResolvedOpcode.RankLt:
+ return true;
+ default:
+ return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);
}
- return UsesSpecFeatures(e.E0) || UsesSpecFeatures(e.E1);
} else if (expr is TernaryExpr) {
var e = (TernaryExpr)expr;
switch (e.Op) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 225eb487..3d07a729 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -6662,7 +6662,7 @@ namespace Microsoft.Dafny { for (int j = 0; j < i; j++) {
var prev = lhss[j] as IdentifierExpr;
if (prev != null && names[i] == names[j]) {
- builder.Add(Assert(tok, Bpl.Expr.Imp(Bpl.Expr.True, Bpl.Expr.Eq(rhs[i],rhs[j])), string.Format("when left-hand sides {0} and {1} refer to the same location, they must have the same value", j, i)));
+ builder.Add(Assert(tok, Bpl.Expr.Imp(Bpl.Expr.True, Bpl.Expr.Eq(rhs[i], rhs[j])), string.Format("when left-hand sides {0} and {1} refer to the same location, they must be assigned the same value", j, i)));
}
}
} else if (lhs is FieldSelectExpr) {
@@ -6671,7 +6671,7 @@ namespace Microsoft.Dafny { for (int j = 0; j < i; j++) {
var prev = lhss[j] as FieldSelectExpr;
if (prev != null && prev.Field == fse.Field) {
- builder.Add(Assert(tok, Bpl.Expr.Imp(Bpl.Expr.Eq(objs[j], objs[i]), Bpl.Expr.Eq(rhs[i], rhs[j])), string.Format("when left-hand sides {0} and {1} refer to the same location, they must have the same value", j, i)));
+ builder.Add(Assert(tok, Bpl.Expr.Imp(Bpl.Expr.Eq(objs[j], objs[i]), Bpl.Expr.Eq(rhs[i], rhs[j])), string.Format("when left-hand sides {0} and {1} refer to the same location, they must be assigned the same value", j, i)));
}
}
} else if (lhs is SeqSelectExpr) {
@@ -6682,7 +6682,7 @@ namespace Microsoft.Dafny { if (prev != null) {
builder.Add(Assert(tok,
Bpl.Expr.Imp(Bpl.Expr.And(Bpl.Expr.Eq(objs[j], objs[i]), Bpl.Expr.Eq(fields[j], fields[i])), Bpl.Expr.Eq(rhs[i], rhs[j])),
- string.Format("when left-hand sides {0} and {1} may refer to the same location, they must have the same value", j, i)));
+ string.Format("when left-hand sides {0} and {1} may refer to the same location, they must be assigned the same value", j, i)));
}
}
} else {
@@ -6693,7 +6693,7 @@ namespace Microsoft.Dafny { if (prev != null) {
builder.Add(Assert(tok,
Bpl.Expr.Imp(Bpl.Expr.And(Bpl.Expr.Eq(objs[j], objs[i]), Bpl.Expr.Eq(fields[j], fields[i])), Bpl.Expr.Eq(rhs[i], rhs[j])),
- string.Format("when left-hand sides {0} and {1} refer to the same location, they must have the same value", j, i)));
+ string.Format("when left-hand sides {0} and {1} refer to the same location, they must be assigned the same value", j, i)));
}
}
diff --git a/Test/VSComp2010/Problem4-Queens.dfy b/Test/VSComp2010/Problem4-Queens.dfy index 2f21b7a1..2d4111db 100644 --- a/Test/VSComp2010/Problem4-Queens.dfy +++ b/Test/VSComp2010/Problem4-Queens.dfy @@ -34,7 +34,7 @@ method Search(N: int) returns (success: bool, board: seq<int>) |board| == N &&
(forall p :: 0 <= p && p < N ==> IsConsistent(board, p));
ensures !success ==>
- (forall B ::
+ (forall B: seq<int> ::
|B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N)
==>
(exists p :: 0 <= p && p < N && !IsConsistent(B, p)));
@@ -66,7 +66,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: |newBoard| == N &&
(forall p :: 0 <= p && p < N ==> IsConsistent(newBoard, p));
ensures !success ==>
- (forall B ::
+ (forall B: seq<int> ::
|B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&
boardSoFar <= B
==>
@@ -84,7 +84,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: var n := 0;
while (n < N)
invariant n <= N;
- invariant (forall B ::
+ invariant (forall B: seq<int> ::
// For any board 'B' with 'N' queens, each placed in an existing row
|B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&
// ... where 'B' is an extension of 'boardSoFar'
@@ -122,7 +122,7 @@ method SearchAux(N: int, boardSoFar: seq<int>) returns (success: bool, newBoard: } else {
// Since 'n' is not a consistent placement for a queen in column 'pos', there is also
// no extension of 'candidateBoard' that would make the entire board consistent.
- assert (forall B ::
+ assert (forall B: seq<int> ::
|B| == N && (forall i :: 0 <= i && i < N ==> 0 <= B[i] && B[i] < N) &&
candidateBoard <= B
==>
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0ca8c4f8..d2ddc057 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -357,6 +357,8 @@ ResolutionErrors.dfy(606,10): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(615,17): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(617,20): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(619,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
+ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
ResolutionErrors.dfy(427,2): Error: More than one default constructor
ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
@@ -429,7 +431,7 @@ ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only i ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(544,18): Error: unresolved identifier: w
-89 resolution/type errors detected in ResolutionErrors.dfy
+91 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -703,7 +705,7 @@ Basics.dfy(110,16): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon10_Then
-Basics.dfy(129,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value
+Basics.dfy(129,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
(0,0): anon10_Then
@@ -712,7 +714,7 @@ Execution trace: (0,0): anon6
(0,0): anon12_Then
(0,0): anon9
-Basics.dfy(143,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
+Basics.dfy(143,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
Basics.dfy(155,19): Error: assertion violation
@@ -743,7 +745,7 @@ Execution trace: (0,0): anon13_Then
(0,0): anon8
(0,0): anon14_Then
-Basics.dfy(236,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value
+Basics.dfy(235,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy index ccd55fa3..b451cdf1 100644 --- a/Test/dafny0/Basics.dfy +++ b/Test/dafny0/Basics.dfy @@ -207,7 +207,6 @@ method m() {
var i: int, j: int;
i, j := 3, 6;
- i, i := 3, 3;
}
method swap(a: array<int>, i: nat, j: nat)
diff --git a/Test/dafny0/Maps.dfy b/Test/dafny0/Maps.dfy index 1c245952..b23a3750 100644 --- a/Test/dafny0/Maps.dfy +++ b/Test/dafny0/Maps.dfy @@ -103,13 +103,13 @@ method m7() }
method m8()
{
- var a := map[];
+ var a: map<int,int> := map[];
assert forall i :: i !in a; // check emptiness
var i,n := 0, 100;
while(i < n)
invariant 0 <= i <= n;
invariant forall i | i in a :: a[i] == i * i;
- invariant forall k :: 0 <= k < i <==> k in a;
+ invariant forall k :: 0 <= k < i <==> k in a;
{
a := a[i := i * i];
i := i + 1;
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 696a583f..60314836 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -626,3 +626,19 @@ module GhostAllocationTests { {
}
}
+
+// ------------------------- underspecified types ------------------------------
+
+module UnderspecifiedTypes {
+ method M(S: set<int>) {
+ var n, p, T0 :| 12 <= n && n in T0 && 10 <= p && p in T0 && T0 <= S && p % 2 != n % 2;
+ var T1 :| 12 in T1 && T1 <= S;
+ var T2 :| T2 <= S && 12 in T2;
+ var T3 :| 120 in T3; // error: underspecified type
+ var T3'0: set<int> :| 120 in T3'0;
+ var T3'1: multiset<int> :| 120 in T3'1;
+ var T3'2: map<int,bool> :| 120 in T3'2;
+ var T3'3: seq<int> :| 120 in T3'3;
+ var T4 :| T4 <= S;
+ }
+}
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy index 93bf1812..1cc906f3 100644 --- a/Test/dafny2/StoreAndRetrieve.dfy +++ b/Test/dafny2/StoreAndRetrieve.dfy @@ -1,6 +1,6 @@ abstract module A {
import L = Library;
- class {:autocontracts} StoreAndRetrieve<Thing> {
+ class {:autocontracts} StoreAndRetrieve<Thing(==)> {
ghost var Contents: set<Thing>;
predicate Valid
{
@@ -26,7 +26,7 @@ abstract module A { }
module B refines A {
- class StoreAndRetrieve<Thing> {
+ class StoreAndRetrieve<Thing(==)> {
var arr: seq<Thing>;
predicate Valid
{
@@ -52,14 +52,14 @@ module B refines A { }
var k := arr[i];
...;
- var a :| assume Contents == set x | x in a;
+ var a: seq<Thing> :| assume Contents == set x | x in a;
arr := a;
}
}
}
module C refines B {
- class StoreAndRetrieve<Thing> {
+ class StoreAndRetrieve<Thing(==)> {
method Retrieve...
{
...;
|