summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Dafny/Compiler.cs59
-rw-r--r--Dafny/Dafny.atg32
-rw-r--r--Dafny/DafnyAst.cs34
-rw-r--r--Dafny/Parser.cs500
-rw-r--r--Dafny/Printer.cs21
-rw-r--r--Dafny/Resolver.cs59
-rw-r--r--Dafny/Scanner.cs201
-rw-r--r--Dafny/Translator.cs126
-rw-r--r--Test/dafny0/Answer64
-rw-r--r--Test/dafny0/Definedness.dfy25
-rw-r--r--Test/dafny0/SmallTests.dfy14
-rw-r--r--Test/dafny0/TypeAntecedents.dfy4
-rw-r--r--Util/Emacs/dafny-mode.el2
-rw-r--r--Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs4
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs1
-rw-r--r--Util/latex/dafny.sty2
-rw-r--r--Util/vim/syntax/dafny.vim2
17 files changed, 374 insertions, 776 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 52a4578c..9938d30a 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -690,12 +690,6 @@ namespace Microsoft.Dafny {
CheckHasNoAssumes(s);
}
}
- } else if (stmt is ForeachStmt) {
- ForeachStmt s = (ForeachStmt)stmt;
- foreach (PredicateStmt t in s.BodyPrefix) {
- CheckHasNoAssumes(t);
- }
- CheckHasNoAssumes(s.GivenBody);
} else if (stmt is ParallelStmt) {
var s = (ParallelStmt)stmt;
CheckHasNoAssumes(s.Body);
@@ -1031,59 +1025,6 @@ namespace Microsoft.Dafny {
Indent(indent);
wr.WriteLine("}");
- } else if (stmt is ForeachStmt) {
- ForeachStmt s = (ForeachStmt)stmt;
- // List<Pair<TType,RhsType>> pendingUpdates = new List<Pair<TType,RhsType>>();
- // foreach (TType x in S) {
- // if (Range(x)) {
- // assert/assume ...;
- // pendingUpdates.Add(new Pair(x,RHS));
- // }
- // }
- // foreach (Pair<TType,RhsType> p in pendingUpdates) {
- // p.Car.m = p.Cdr;
- // }
- string pu = "_pendingUpdates" + tmpVarCount;
- string pr = "_pair" + tmpVarCount;
- tmpVarCount++;
- string TType = TypeName(s.BoundVar.Type);
- string RhsType = TypeName(cce.NonNull(s.BodyAssign.Lhs.Type));
-
- Indent(indent);
- wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);
-
- Indent(indent);
- wr.Write("foreach ({0} @{1} in (", TType, s.BoundVar.Name);
- TrExpr(s.Collection);
- wr.WriteLine(").Elements) {");
-
- Indent(indent + IndentAmount);
- wr.Write("if (");
- TrExpr(s.Range);
- wr.WriteLine(") {");
-
- foreach (PredicateStmt p in s.BodyPrefix) {
- TrStmt(p, indent + 2*IndentAmount);
- }
- Indent(indent + 2*IndentAmount);
- wr.Write("{0}.Add(new Pair<{1},{2}>(@{3}, ", pu, TType, RhsType, s.BoundVar.Name);
- ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;
- if (rhsExpr != null) {
- TrExpr(rhsExpr.Expr);
- } else {
- wr.Write(DefaultValue(s.BodyAssign.Lhs.Type));
- }
- wr.WriteLine("))");
-
- Indent(indent + IndentAmount); wr.WriteLine("}");
- Indent(indent); wr.WriteLine("}");
-
- Indent(indent); wr.WriteLine("foreach (Pair<{0},{1}> {2} in {3}) {{", TType, RhsType, pr, pu);
- Indent(indent + IndentAmount);
- FieldSelectExpr fse = (FieldSelectExpr)s.BodyAssign.Lhs;
- wr.WriteLine("{0}.Car.{1} = {0}.Cdr;", pr, fse.FieldName);
- Indent(indent); wr.WriteLine("}");
-
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
// Type source = e;
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 0092b4d9..9de1421b 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -631,7 +631,6 @@ OneStmt<out Statement/*!*/ s>
| IfStmt<out s>
| WhileStmt<out s>
| MatchStmt<out s>
- | ForeachStmt<out s>
| ParallelStmt<out s>
| "label" (. x = t; .)
Ident<out id> ":"
@@ -886,36 +885,7 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
(. c = new MatchCaseStmt(x, id.val, arguments, body); .)
.
/*------------------------------------------------------------------------*/
-ForeachStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- IToken/*!*/ x, boundVar;
- Type/*!*/ ty;
- Expression/*!*/ collection;
- Expression/*!*/ range;
- List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
- Statement bodyAssign = null;
- .)
- "foreach" (. x = t;
- range = new LiteralExpr(x, true);
- ty = new InferredTypeProxy();
- .)
- "(" Ident<out boundVar>
- [ ":" Type<out ty> ]
- "in" Expression<out collection>
- [ "|" Expression<out range> ]
- ")"
- "{"
- { AssertStmt<out s> (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
- | AssumeStmt<out s> (. if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); } .)
- }
- UpdateStmt<out s> (. bodyAssign = s; .)
- "}" (. if (bodyAssign != null) {
- s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
- } else {
- s = dummyStmt; // some error occurred in parsing the bodyAssign
- }
- .)
- .
+
AssertStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"assert" (. x = t; .)
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index d9d5c486..88862483 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1753,40 +1753,6 @@ namespace Microsoft.Dafny {
}
}
- public class ForeachStmt : Statement
- {
- public readonly BoundVar/*!*/ BoundVar;
- public readonly Expression/*!*/ Collection;
- public readonly Expression/*!*/ Range;
- public readonly List<PredicateStmt/*!*/>/*!*/ BodyPrefix;
- public readonly Statement GivenBody; // used only until resolution; afterwards, use BodyAssign
- public AssignStmt/*!*/ BodyAssign; // filled in during resolution
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(BoundVar != null);
- Contract.Invariant(Collection != null);
- Contract.Invariant(Range != null);
- Contract.Invariant(cce.NonNullElements(BodyPrefix));
- Contract.Invariant(GivenBody != null);
- }
-
- public ForeachStmt(IToken tok, BoundVar boundVar, Expression collection, Expression range,
- List<PredicateStmt/*!*/>/*!*/ bodyPrefix, Statement givenBody)
- : base(tok) {
- Contract.Requires(tok != null);
- Contract.Requires(boundVar != null);
- Contract.Requires(collection != null);
- Contract.Requires(range != null);
- Contract.Requires(cce.NonNullElements(bodyPrefix));
- Contract.Requires(givenBody != null);
- this.BoundVar = boundVar;
- this.Collection = collection;
- this.Range = range;
- this.BodyPrefix = bodyPrefix;
- this.GivenBody = givenBody;
- }
- }
-
public class ParallelStmt : Statement
{
public readonly List<BoundVar/*!*/> BoundVars;
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 483217e5..57f4c46e 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -18,12 +18,12 @@ public class Parser {
public const int _digits = 2;
public const int _arrayToken = 3;
public const int _string = 4;
- public const int maxT = 105;
+ public const int maxT = 104;
const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -134,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
@@ -150,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -182,7 +182,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -375,7 +375,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
mm.Add(m);
} else if (la.kind == 20) {
CouplingInvDecl(mmod, mm);
- } else SynErr(106);
+ } else SynErr(105);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -490,7 +490,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
} else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(107);
+ } else SynErr(106);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
if (isConstructor) {
if (mmod.IsGhost) {
@@ -728,7 +728,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(108); break;
+ default: SynErr(107); break;
}
}
@@ -779,12 +779,12 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out e);
Expect(17);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(109);
+ } else SynErr(108);
} else if (la.kind == 32) {
Get();
DecreasesList(decreases, false);
Expect(17);
- } else SynErr(110);
+ } else SynErr(109);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -874,7 +874,7 @@ List<Expression/*!*/>/*!*/ decreases) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(111);
+ } else SynErr(110);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -906,7 +906,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
DecreasesList(decreases, false);
Expect(17);
- } else SynErr(112);
+ } else SynErr(111);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -925,7 +925,7 @@ List<Expression/*!*/>/*!*/ decreases) {
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(6)) {
FrameExpression(out fe);
- } else SynErr(113);
+ } else SynErr(112);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -936,7 +936,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new WildcardExpr(t);
} else if (StartOf(6)) {
Expression(out e);
- } else SynErr(114);
+ } else SynErr(113);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -957,19 +957,19 @@ List<Expression/*!*/>/*!*/ decreases) {
BlockStmt(out s, out bodyStart, out bodyEnd);
break;
}
- case 64: {
+ case 62: {
AssertStmt(out s);
break;
}
- case 65: {
+ case 63: {
AssumeStmt(out s);
break;
}
- case 66: {
+ case 64: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
+ case 1: case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
UpdateStmt(out s);
break;
}
@@ -989,11 +989,7 @@ List<Expression/*!*/>/*!*/ decreases) {
MatchStmt(out s);
break;
}
- case 62: {
- ForeachStmt(out s);
- break;
- }
- case 67: {
+ case 65: {
ParallelStmt(out s);
break;
}
@@ -1017,7 +1013,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
breakCount++;
}
- } else SynErr(115);
+ } else SynErr(114);
Expect(17);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
@@ -1026,13 +1022,13 @@ List<Expression/*!*/>/*!*/ decreases) {
ReturnStmt(out s);
break;
}
- default: SynErr(116); break;
+ default: SynErr(115); break;
}
}
void AssertStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(64);
+ Expect(62);
x = t;
Expression(out e);
Expect(17);
@@ -1041,7 +1037,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(65);
+ Expect(63);
x = t;
Expression(out e);
Expect(17);
@@ -1052,7 +1048,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(66);
+ Expect(64);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1097,7 +1093,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 22) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(117);
+ } else SynErr(116);
s = new UpdateStmt(x, lhss, rhss);
}
@@ -1170,13 +1166,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(118);
+ } else SynErr(117);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(119);
+ } else SynErr(118);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1202,7 +1198,7 @@ List<Expression/*!*/>/*!*/ decreases) {
LoopSpec(out invariants, out decreases, out mod);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives);
- } else SynErr(120);
+ } else SynErr(119);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1221,54 +1217,6 @@ List<Expression/*!*/>/*!*/ decreases) {
s = new MatchStmt(x, e, cases);
}
- void ForeachStmt(out Statement/*!*/ s) {
- Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- IToken/*!*/ x, boundVar;
- Type/*!*/ ty;
- Expression/*!*/ collection;
- Expression/*!*/ range;
- List<PredicateStmt/*!*/> bodyPrefix = new List<PredicateStmt/*!*/>();
- Statement bodyAssign = null;
-
- Expect(62);
- x = t;
- range = new LiteralExpr(x, true);
- ty = new InferredTypeProxy();
-
- Expect(33);
- Ident(out boundVar);
- if (la.kind == 22) {
- Get();
- Type(out ty);
- }
- Expect(63);
- Expression(out collection);
- if (la.kind == 16) {
- Get();
- Expression(out range);
- }
- Expect(34);
- Expect(7);
- while (la.kind == 64 || la.kind == 65) {
- if (la.kind == 64) {
- AssertStmt(out s);
- if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- } else {
- AssumeStmt(out s);
- if (s is PredicateStmt) { bodyPrefix.Add((PredicateStmt)s); }
- }
- }
- UpdateStmt(out s);
- bodyAssign = s;
- Expect(8);
- if (bodyAssign != null) {
- s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);
- } else {
- s = dummyStmt; // some error occurred in parsing the bodyAssign
- }
-
- }
-
void ParallelStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
IToken/*!*/ x;
@@ -1281,7 +1229,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Statement/*!*/ block;
IToken bodyStart, bodyEnd;
- Expect(67);
+ Expect(65);
x = t;
Expect(33);
QuantifierDomain(out bvars, out attrs, out range);
@@ -1371,7 +1319,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(6)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(121);
+ } else SynErr(120);
}
void Lhs(out Expression e) {
@@ -1388,7 +1336,7 @@ List<Expression/*!*/>/*!*/ decreases) {
while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
- } else SynErr(122);
+ } else SynErr(121);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1411,7 +1359,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(6)) {
Expression(out ee);
e = ee;
- } else SynErr(123);
+ } else SynErr(122);
Expect(34);
}
@@ -1510,7 +1458,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (StartOf(6)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(124);
+ } else SynErr(123);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -1538,7 +1486,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 68 || la.kind == 69) {
+ while (la.kind == 66 || la.kind == 67) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1549,7 +1497,7 @@ List<Expression/*!*/>/*!*/ decreases) {
void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 70 || la.kind == 71) {
+ if (la.kind == 68 || la.kind == 69) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1558,23 +1506,23 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void EquivOp() {
- if (la.kind == 68) {
+ if (la.kind == 66) {
Get();
- } else if (la.kind == 69) {
+ } else if (la.kind == 67) {
Get();
- } else SynErr(125);
+ } else SynErr(124);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(13)) {
- if (la.kind == 72 || la.kind == 73) {
+ if (la.kind == 70 || la.kind == 71) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 72 || la.kind == 73) {
+ while (la.kind == 70 || la.kind == 71) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1585,7 +1533,7 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 74 || la.kind == 75) {
+ while (la.kind == 72 || la.kind == 73) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1596,11 +1544,11 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void ImpliesOp() {
- if (la.kind == 70) {
+ if (la.kind == 68) {
Get();
- } else if (la.kind == 71) {
+ } else if (la.kind == 69) {
Get();
- } else SynErr(126);
+ } else SynErr(125);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1694,25 +1642,25 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void AndOp() {
- if (la.kind == 72) {
+ if (la.kind == 70) {
Get();
- } else if (la.kind == 73) {
+ } else if (la.kind == 71) {
Get();
- } else SynErr(127);
+ } else SynErr(126);
}
void OrOp() {
- if (la.kind == 74) {
+ if (la.kind == 72) {
Get();
- } else if (la.kind == 75) {
+ } else if (la.kind == 73) {
Get();
- } else SynErr(128);
+ } else SynErr(127);
}
void Term(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
Factor(out e0);
- while (la.kind == 85 || la.kind == 86) {
+ while (la.kind == 84 || la.kind == 85) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1725,7 +1673,7 @@ List<Expression/*!*/>/*!*/ decreases) {
IToken y;
switch (la.kind) {
- case 76: {
+ case 74: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
@@ -1740,35 +1688,35 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 77: {
+ case 75: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 78: {
+ case 76: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 79: {
+ case 77: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 80: {
+ case 78: {
Get();
x = t; op = BinaryExpr.Opcode.Disjoint;
break;
}
- case 63: {
+ case 79: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
}
- case 81: {
+ case 80: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 63) {
+ if (la.kind == 79) {
Get();
y = t;
}
@@ -1783,29 +1731,29 @@ List<Expression/*!*/>/*!*/ decreases) {
break;
}
- case 82: {
+ case 81: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 83: {
+ case 82: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 84: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(129); break;
+ default: SynErr(128); break;
}
}
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 44 || la.kind == 87 || la.kind == 88) {
+ while (la.kind == 44 || la.kind == 86 || la.kind == 87) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -1814,33 +1762,33 @@ List<Expression/*!*/>/*!*/ decreases) {
void AddOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 85) {
+ if (la.kind == 84) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 86) {
+ } else if (la.kind == 85) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(130);
+ } else SynErr(129);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 86: {
+ case 85: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 81: case 89: {
+ case 80: case 88: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 38: case 55: case 61: case 99: case 100: case 101: case 102: {
+ case 38: case 55: case 61: case 98: case 99: case 100: case 101: {
EndlessExpression(out e);
break;
}
@@ -1859,14 +1807,14 @@ List<Expression/*!*/>/*!*/ decreases) {
MultiSetExpr(out e);
break;
}
- case 2: case 16: case 33: case 90: case 91: case 92: case 93: case 94: case 95: case 96: {
+ case 2: case 16: case 33: case 89: case 90: case 91: case 92: case 93: case 94: case 95: {
ConstAtomExpression(out e);
while (la.kind == 51 || la.kind == 53) {
Suffix(ref e);
}
break;
}
- default: SynErr(131); break;
+ default: SynErr(130); break;
}
}
@@ -1875,21 +1823,21 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 44) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 87) {
+ } else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 88) {
+ } else if (la.kind == 87) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(132);
+ } else SynErr(131);
}
void NegOp() {
- if (la.kind == 81) {
+ if (la.kind == 80) {
Get();
- } else if (la.kind == 89) {
+ } else if (la.kind == 88) {
Get();
- } else SynErr(133);
+ } else SynErr(132);
}
void EndlessExpression(out Expression e) {
@@ -1901,7 +1849,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
x = t;
Expression(out e);
- Expect(97);
+ Expect(96);
Expression(out e0);
Expect(56);
Expression(out e1);
@@ -1912,7 +1860,7 @@ List<Expression/*!*/>/*!*/ decreases) {
QuantifierGuts(out e);
} else if (la.kind == 38) {
ComprehensionExpr(out e);
- } else SynErr(134);
+ } else SynErr(133);
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -1963,7 +1911,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (StartOf(6)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 98) {
+ if (la.kind == 97) {
Get();
anyDots = true;
if (StartOf(6)) {
@@ -1985,15 +1933,15 @@ List<Expression/*!*/>/*!*/ decreases) {
multipleIndices.Add(ee);
}
- } else SynErr(135);
- } else if (la.kind == 98) {
+ } else SynErr(134);
+ } else if (la.kind == 97) {
Get();
anyDots = true;
if (StartOf(6)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(136);
+ } else SynErr(135);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2017,7 +1965,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(52);
- } else SynErr(137);
+ } else SynErr(136);
}
void DisplayExpr(out Expression e) {
@@ -2041,7 +1989,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
e = new SeqDisplayExpr(x, elements);
Expect(52);
- } else SynErr(138);
+ } else SynErr(137);
}
void MultiSetExpr(out Expression e) {
@@ -2067,7 +2015,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(34);
} else if (StartOf(16)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(139);
+ } else SynErr(138);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2076,17 +2024,17 @@ List<Expression/*!*/>/*!*/ decreases) {
e = dummyExpr;
switch (la.kind) {
- case 90: {
+ case 89: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 91: {
+ case 90: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 92: {
+ case 91: {
Get();
e = new LiteralExpr(t);
break;
@@ -2096,12 +2044,12 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new LiteralExpr(t, n);
break;
}
- case 93: {
+ case 92: {
Get();
e = new ThisExpr(t);
break;
}
- case 94: {
+ case 93: {
Get();
x = t;
Expect(33);
@@ -2110,7 +2058,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new FreshExpr(x, e);
break;
}
- case 95: {
+ case 94: {
Get();
x = t;
Expect(33);
@@ -2119,7 +2067,7 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new AllocatedExpr(x, e);
break;
}
- case 96: {
+ case 95: {
Get();
x = t;
Expect(33);
@@ -2144,7 +2092,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(34);
break;
}
- default: SynErr(140); break;
+ default: SynErr(139); break;
}
}
@@ -2181,13 +2129,13 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression range;
Expression/*!*/ body;
- if (la.kind == 99 || la.kind == 100) {
+ if (la.kind == 98 || la.kind == 99) {
Forall();
x = t; univ = true;
- } else if (la.kind == 101 || la.kind == 102) {
+ } else if (la.kind == 100 || la.kind == 101) {
Exists();
x = t;
- } else SynErr(141);
+ } else SynErr(140);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -2218,7 +2166,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(16);
Expression(out range);
- if (la.kind == 103 || la.kind == 104) {
+ if (la.kind == 102 || la.kind == 103) {
QSep();
Expression(out body);
}
@@ -2253,27 +2201,27 @@ List<Expression/*!*/>/*!*/ decreases) {
}
void Forall() {
- if (la.kind == 99) {
+ if (la.kind == 98) {
Get();
- } else if (la.kind == 100) {
+ } else if (la.kind == 99) {
Get();
- } else SynErr(142);
+ } else SynErr(141);
}
void Exists() {
- if (la.kind == 101) {
+ if (la.kind == 100) {
Get();
- } else if (la.kind == 102) {
+ } else if (la.kind == 101) {
Get();
- } else SynErr(143);
+ } else SynErr(142);
}
void QSep() {
- if (la.kind == 103) {
+ if (la.kind == 102) {
Get();
- } else if (la.kind == 104) {
+ } else if (la.kind == 103) {
Get();
- } else SynErr(144);
+ } else SynErr(143);
}
void AttributeBody(ref Attributes attrs) {
@@ -2300,32 +2248,32 @@ List<Expression/*!*/>/*!*/ decreases) {
public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
- Expect(0);
+ Expect(0);
}
-
+
static readonly bool[,]/*!*/ set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x},
- {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x},
- {x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,T, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,T,T,x, x,x,x,T, T,x,x},
- {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, T,x,x,T, T,T,T,x, x,x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,T, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},
+ {x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,T,x,T, x,x,x,T, T,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, T,x,x,x, T,T,T,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},
+ {x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
};
} // end Parser
@@ -2334,18 +2282,20 @@ List<Expression/*!*/>/*!*/ decreases) {
public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
- public virtual void SynErr(string filename, int line, int col, string msg) {
- Contract.Requires(msg != null);
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+
+ public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
- }
- string GetSyntaxErrorString(int n) {
+ }
+
+ string GetSyntaxErrorString(int n) {
string s;
switch (n) {
case 0: s = "EOF expected"; break;
@@ -2410,93 +2360,92 @@ public class Errors {
case 59: s = "\"while\" expected"; break;
case 60: s = "\"invariant\" expected"; break;
case 61: s = "\"match\" expected"; break;
- case 62: s = "\"foreach\" expected"; break;
- case 63: s = "\"in\" expected"; break;
- case 64: s = "\"assert\" expected"; break;
- case 65: s = "\"assume\" expected"; break;
- case 66: s = "\"print\" expected"; break;
- case 67: s = "\"parallel\" expected"; break;
- case 68: s = "\"<==>\" expected"; break;
- case 69: s = "\"\\u21d4\" expected"; break;
- case 70: s = "\"==>\" expected"; break;
- case 71: s = "\"\\u21d2\" expected"; break;
- case 72: s = "\"&&\" expected"; break;
- case 73: s = "\"\\u2227\" expected"; break;
- case 74: s = "\"||\" expected"; break;
- case 75: s = "\"\\u2228\" expected"; break;
- case 76: s = "\"==\" expected"; break;
- case 77: s = "\"<=\" expected"; break;
- case 78: s = "\">=\" expected"; break;
- case 79: s = "\"!=\" expected"; break;
- case 80: s = "\"!!\" expected"; break;
- case 81: s = "\"!\" expected"; break;
- case 82: s = "\"\\u2260\" expected"; break;
- case 83: s = "\"\\u2264\" expected"; break;
- case 84: s = "\"\\u2265\" expected"; break;
- case 85: s = "\"+\" expected"; break;
- case 86: s = "\"-\" expected"; break;
- case 87: s = "\"/\" expected"; break;
- case 88: s = "\"%\" expected"; break;
- case 89: s = "\"\\u00ac\" expected"; break;
- case 90: s = "\"false\" expected"; break;
- case 91: s = "\"true\" expected"; break;
- case 92: s = "\"null\" expected"; break;
- case 93: s = "\"this\" expected"; break;
- case 94: s = "\"fresh\" expected"; break;
- case 95: s = "\"allocated\" expected"; break;
- case 96: s = "\"old\" expected"; break;
- case 97: s = "\"then\" expected"; break;
- case 98: s = "\"..\" expected"; break;
- case 99: s = "\"forall\" expected"; break;
- case 100: s = "\"\\u2200\" expected"; break;
- case 101: s = "\"exists\" expected"; break;
- case 102: s = "\"\\u2203\" expected"; break;
- case 103: s = "\"::\" expected"; break;
- case 104: s = "\"\\u2022\" expected"; break;
- case 105: s = "??? expected"; break;
- case 106: s = "invalid ClassMemberDecl"; break;
- case 107: s = "invalid MethodDecl"; break;
- case 108: s = "invalid TypeAndToken"; break;
+ case 62: s = "\"assert\" expected"; break;
+ case 63: s = "\"assume\" expected"; break;
+ case 64: s = "\"print\" expected"; break;
+ case 65: s = "\"parallel\" expected"; break;
+ case 66: s = "\"<==>\" expected"; break;
+ case 67: s = "\"\\u21d4\" expected"; break;
+ case 68: s = "\"==>\" expected"; break;
+ case 69: s = "\"\\u21d2\" expected"; break;
+ case 70: s = "\"&&\" expected"; break;
+ case 71: s = "\"\\u2227\" expected"; break;
+ case 72: s = "\"||\" expected"; break;
+ case 73: s = "\"\\u2228\" expected"; break;
+ case 74: s = "\"==\" expected"; break;
+ case 75: s = "\"<=\" expected"; break;
+ case 76: s = "\">=\" expected"; break;
+ case 77: s = "\"!=\" expected"; break;
+ case 78: s = "\"!!\" expected"; break;
+ case 79: s = "\"in\" expected"; break;
+ case 80: s = "\"!\" expected"; break;
+ case 81: s = "\"\\u2260\" expected"; break;
+ case 82: s = "\"\\u2264\" expected"; break;
+ case 83: s = "\"\\u2265\" expected"; break;
+ case 84: s = "\"+\" expected"; break;
+ case 85: s = "\"-\" expected"; break;
+ case 86: s = "\"/\" expected"; break;
+ case 87: s = "\"%\" expected"; break;
+ case 88: s = "\"\\u00ac\" expected"; break;
+ case 89: s = "\"false\" expected"; break;
+ case 90: s = "\"true\" expected"; break;
+ case 91: s = "\"null\" expected"; break;
+ case 92: s = "\"this\" expected"; break;
+ case 93: s = "\"fresh\" expected"; break;
+ case 94: s = "\"allocated\" expected"; break;
+ case 95: s = "\"old\" expected"; break;
+ case 96: s = "\"then\" expected"; break;
+ case 97: s = "\"..\" expected"; break;
+ case 98: s = "\"forall\" expected"; break;
+ case 99: s = "\"\\u2200\" expected"; break;
+ case 100: s = "\"exists\" expected"; break;
+ case 101: s = "\"\\u2203\" expected"; break;
+ case 102: s = "\"::\" expected"; break;
+ case 103: s = "\"\\u2022\" expected"; break;
+ case 104: s = "??? expected"; break;
+ case 105: s = "invalid ClassMemberDecl"; break;
+ case 106: s = "invalid MethodDecl"; break;
+ case 107: s = "invalid TypeAndToken"; break;
+ case 108: s = "invalid MethodSpec"; break;
case 109: s = "invalid MethodSpec"; break;
- case 110: s = "invalid MethodSpec"; break;
- case 111: s = "invalid ReferenceType"; break;
- case 112: s = "invalid FunctionSpec"; break;
- case 113: s = "invalid PossiblyWildFrameExpression"; break;
- case 114: s = "invalid PossiblyWildExpression"; break;
+ case 110: s = "invalid ReferenceType"; break;
+ case 111: s = "invalid FunctionSpec"; break;
+ case 112: s = "invalid PossiblyWildFrameExpression"; break;
+ case 113: s = "invalid PossiblyWildExpression"; break;
+ case 114: s = "invalid OneStmt"; break;
case 115: s = "invalid OneStmt"; break;
- case 116: s = "invalid OneStmt"; break;
- case 117: s = "invalid UpdateStmt"; break;
+ case 116: s = "invalid UpdateStmt"; break;
+ case 117: s = "invalid IfStmt"; break;
case 118: s = "invalid IfStmt"; break;
- case 119: s = "invalid IfStmt"; break;
- case 120: s = "invalid WhileStmt"; break;
- case 121: s = "invalid Rhs"; break;
- case 122: s = "invalid Lhs"; break;
- case 123: s = "invalid Guard"; break;
- case 124: s = "invalid AttributeArg"; break;
- case 125: s = "invalid EquivOp"; break;
- case 126: s = "invalid ImpliesOp"; break;
- case 127: s = "invalid AndOp"; break;
- case 128: s = "invalid OrOp"; break;
- case 129: s = "invalid RelOp"; break;
- case 130: s = "invalid AddOp"; break;
- case 131: s = "invalid UnaryExpression"; break;
- case 132: s = "invalid MulOp"; break;
- case 133: s = "invalid NegOp"; break;
- case 134: s = "invalid EndlessExpression"; break;
+ case 119: s = "invalid WhileStmt"; break;
+ case 120: s = "invalid Rhs"; break;
+ case 121: s = "invalid Lhs"; break;
+ case 122: s = "invalid Guard"; break;
+ case 123: s = "invalid AttributeArg"; break;
+ case 124: s = "invalid EquivOp"; break;
+ case 125: s = "invalid ImpliesOp"; break;
+ case 126: s = "invalid AndOp"; break;
+ case 127: s = "invalid OrOp"; break;
+ case 128: s = "invalid RelOp"; break;
+ case 129: s = "invalid AddOp"; break;
+ case 130: s = "invalid UnaryExpression"; break;
+ case 131: s = "invalid MulOp"; break;
+ case 132: s = "invalid NegOp"; break;
+ case 133: s = "invalid EndlessExpression"; break;
+ case 134: s = "invalid Suffix"; break;
case 135: s = "invalid Suffix"; break;
case 136: s = "invalid Suffix"; break;
- case 137: s = "invalid Suffix"; break;
- case 138: s = "invalid DisplayExpr"; break;
- case 139: s = "invalid MultiSetExpr"; break;
- case 140: s = "invalid ConstAtomExpression"; break;
- case 141: s = "invalid QuantifierGuts"; break;
- case 142: s = "invalid Forall"; break;
- case 143: s = "invalid Exists"; break;
- case 144: s = "invalid QSep"; break;
+ case 137: s = "invalid DisplayExpr"; break;
+ case 138: s = "invalid MultiSetExpr"; break;
+ case 139: s = "invalid ConstAtomExpression"; break;
+ case 140: s = "invalid QuantifierGuts"; break;
+ case 141: s = "invalid Forall"; break;
+ case 142: s = "invalid Exists"; break;
+ case 143: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2504,8 +2453,9 @@ public class Errors {
Contract.Requires(msg != null);
SemErr(tok.filename, tok.line, tok.col, msg);
}
+
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
}
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index f9f1eca0..7f7ba963 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -541,27 +541,6 @@ namespace Microsoft.Dafny {
Indent(indent);
wr.Write("}");
- } else if (stmt is ForeachStmt) {
- ForeachStmt s = (ForeachStmt)stmt;
- wr.Write("foreach ({0} in ", s.BoundVar.Name);
- PrintExpression(s.Collection);
- if (!LiteralExpr.IsTrue(s.Range)) {
- wr.Write(" | ");
- PrintExpression(s.Range);
- }
- wr.WriteLine(") {");
- int ind = indent + IndentAmount;
- foreach (PredicateStmt t in s.BodyPrefix) {
- Indent(ind);
- PrintStatement(t, ind);
- wr.WriteLine();
- }
- Indent(ind);
- PrintStatement(s.GivenBody, ind);
- wr.WriteLine();
- Indent(indent);
- wr.Write("}");
-
} else if (stmt is ParallelStmt) {
var s = (ParallelStmt)stmt;
wr.Write("parallel (");
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index e053f212..a3668619 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1474,62 +1474,6 @@ namespace Microsoft.Dafny {
// any type is fine
}
- } else if (stmt is ForeachStmt) {
- ForeachStmt s = (ForeachStmt)stmt;
-
- ResolveExpression(s.Collection, true);
- Contract.Assert(s.Collection.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(s.Collection.Type, new CollectionTypeProxy(s.BoundVar.Type))) {
- Error(s.Collection, "The type is expected to be a collection of {0} (instead got {1})", s.BoundVar.Type, s.Collection.Type);
- }
-
- scope.PushMarker();
- bool b = scope.Push(s.BoundVar.Name, s.BoundVar);
- Contract.Assert(b); // since we just pushed a marker, we expect the Push to succeed
- ResolveType(s.BoundVar.tok, s.BoundVar.Type);
- int prevErrorCount = ErrorCount;
-
- ResolveExpression(s.Range, true);
- Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(s.Range.Type, Type.Bool)) {
- Error(s.Range, "range condition is expected to be of type {0}, but is {1}", Type.Bool, s.Range.Type);
- }
- bool successfullyResolvedCollectionAndRange = ErrorCount == prevErrorCount;
-
- foreach (PredicateStmt ss in s.BodyPrefix) {
- ResolveStatement(ss, specContextOnly, method);
- }
-
- bool specOnly = specContextOnly ||
- (successfullyResolvedCollectionAndRange && (UsesSpecFeatures(s.Collection) || UsesSpecFeatures(s.Range)));
- s.IsGhost = specOnly;
- ResolveStatement(s.GivenBody, specOnly, method);
- // check for correct usage of BoundVar in LHS and RHS of this assignment
- if (s.GivenBody is AssignStmt) {
- s.BodyAssign = (AssignStmt)s.GivenBody;
- } else if (s.GivenBody is ConcreteSyntaxStatement) {
- var css = (ConcreteSyntaxStatement)s.GivenBody;
- if (css.ResolvedStatements.Count == 1 && css.ResolvedStatements[0] is AssignStmt) {
- s.BodyAssign = (AssignStmt)css.ResolvedStatements[0];
- }
- }
- if (s.BodyAssign == null) {
- Error(s, "update statement inside foreach must be a single assignment statement");
- } else {
- FieldSelectExpr lhs = s.BodyAssign.Lhs as FieldSelectExpr;
- IdentifierExpr obj = lhs == null ? null : lhs.Obj as IdentifierExpr;
- if (obj == null || obj.Var != s.BoundVar) {
- Error(s, "assignment inside foreach must assign to a field of the bound variable of the foreach statement");
- } else {
- var rhs = s.BodyAssign.Rhs as ExprRhs;
- if (rhs != null && rhs.Expr is UnaryExpr && ((UnaryExpr)rhs.Expr).Op == UnaryExpr.Opcode.SetChoose) {
- Error(s, "foreach statement does not support 'choose' statements");
- }
- }
- }
-
- scope.PopMarker();
-
} else if (stmt is ParallelStmt) {
var s = (ParallelStmt)stmt;
@@ -2151,9 +2095,6 @@ namespace Microsoft.Dafny {
}
}
- } else if (stmt is ForeachStmt) {
- Error(stmt, "foreach statement not allowed in body of parallel statement");
-
} else if (stmt is ParallelStmt) {
var s = (ParallelStmt)stmt;
switch (s.Kind) {
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index ae887c47..634abf45 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
// a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,15 +31,17 @@ public class Buffer {
Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
-[ContractInvariantMethod]
-void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);}
- [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
+ [ContractInvariantMethod]
+ void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);
+ }
+
+// [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -51,12 +53,12 @@ void ObjectInvariant(){
buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -73,14 +75,14 @@ void ObjectInvariant(){
}
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -100,7 +102,7 @@ void ObjectInvariant(){
Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -139,7 +141,7 @@ void ObjectInvariant(){
}
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -209,23 +211,24 @@ public class UTF8Buffer: Buffer {
public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 105;
- const int noSym = 105;
-
-
-[ContractInvariantMethod]
-void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
-}
+ const int maxT = 104;
+ const int noSym = 104;
+
+
+ [ContractInvariantMethod]
+ void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+ }
+
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -236,13 +239,13 @@ void objectInvariant(){
Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -290,9 +293,9 @@ void objectInvariant(){
start[Buffer.EOF] = -1;
}
-
- [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
+
+// [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -302,15 +305,14 @@ void objectInvariant(){
Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
-
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
- [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
+
+// [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -319,10 +321,9 @@ void objectInvariant(){
buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
-
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -343,11 +344,11 @@ void objectInvariant(){
Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -358,7 +359,7 @@ void objectInvariant(){
}
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -366,9 +367,9 @@ void objectInvariant(){
// // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -418,7 +419,7 @@ void objectInvariant(){
return;
}
-
+
}
}
@@ -525,22 +526,21 @@ void objectInvariant(){
case "while": t.kind = 59; break;
case "invariant": t.kind = 60; break;
case "match": t.kind = 61; break;
- case "foreach": t.kind = 62; break;
- case "in": t.kind = 63; break;
- case "assert": t.kind = 64; break;
- case "assume": t.kind = 65; break;
- case "print": t.kind = 66; break;
- case "parallel": t.kind = 67; break;
- case "false": t.kind = 90; break;
- case "true": t.kind = 91; break;
- case "null": t.kind = 92; break;
- case "this": t.kind = 93; break;
- case "fresh": t.kind = 94; break;
- case "allocated": t.kind = 95; break;
- case "old": t.kind = 96; break;
- case "then": t.kind = 97; break;
- case "forall": t.kind = 99; break;
- case "exists": t.kind = 101; break;
+ case "assert": t.kind = 62; break;
+ case "assume": t.kind = 63; break;
+ case "print": t.kind = 64; break;
+ case "parallel": t.kind = 65; break;
+ case "in": t.kind = 79; break;
+ case "false": t.kind = 89; break;
+ case "true": t.kind = 90; break;
+ case "null": t.kind = 91; break;
+ case "this": t.kind = 92; break;
+ case "fresh": t.kind = 93; break;
+ case "allocated": t.kind = 94; break;
+ case "old": t.kind = 95; break;
+ case "then": t.kind = 96; break;
+ case "forall": t.kind = 98; break;
+ case "exists": t.kind = 100; break;
default: break;
}
}
@@ -557,10 +557,13 @@ void objectInvariant(){
t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
+ if (start.ContainsKey(ch)) {
+ Contract.Assert(start[ch] != null);
+ state = (int) start[ch];
+ }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -666,56 +669,56 @@ void objectInvariant(){
if (ch == '>') {AddCh(); goto case 30;}
else {goto case 0;}
case 30:
- {t.kind = 68; break;}
+ {t.kind = 66; break;}
case 31:
- {t.kind = 69; break;}
+ {t.kind = 67; break;}
case 32:
- {t.kind = 70; break;}
+ {t.kind = 68; break;}
case 33:
- {t.kind = 71; break;}
+ {t.kind = 69; break;}
case 34:
if (ch == '&') {AddCh(); goto case 35;}
else {goto case 0;}
case 35:
- {t.kind = 72; break;}
+ {t.kind = 70; break;}
case 36:
- {t.kind = 73; break;}
+ {t.kind = 71; break;}
case 37:
- {t.kind = 74; break;}
+ {t.kind = 72; break;}
case 38:
- {t.kind = 75; break;}
+ {t.kind = 73; break;}
case 39:
- {t.kind = 78; break;}
+ {t.kind = 76; break;}
case 40:
- {t.kind = 79; break;}
+ {t.kind = 77; break;}
case 41:
- {t.kind = 80; break;}
+ {t.kind = 78; break;}
case 42:
- {t.kind = 82; break;}
+ {t.kind = 81; break;}
case 43:
- {t.kind = 83; break;}
+ {t.kind = 82; break;}
case 44:
- {t.kind = 84; break;}
+ {t.kind = 83; break;}
case 45:
- {t.kind = 85; break;}
+ {t.kind = 84; break;}
case 46:
- {t.kind = 86; break;}
+ {t.kind = 85; break;}
case 47:
- {t.kind = 87; break;}
+ {t.kind = 86; break;}
case 48:
- {t.kind = 88; break;}
+ {t.kind = 87; break;}
case 49:
- {t.kind = 89; break;}
+ {t.kind = 88; break;}
case 50:
- {t.kind = 98; break;}
+ {t.kind = 97; break;}
case 51:
- {t.kind = 100; break;}
+ {t.kind = 99; break;}
case 52:
- {t.kind = 102; break;}
+ {t.kind = 101; break;}
case 53:
- {t.kind = 103; break;}
+ {t.kind = 102; break;}
case 54:
- {t.kind = 104; break;}
+ {t.kind = 103; break;}
case 55:
recEnd = pos; recKind = 15;
if (ch == '>') {AddCh(); goto case 28;}
@@ -743,31 +746,31 @@ void objectInvariant(){
if (ch == '.') {AddCh(); goto case 50;}
else {t.kind = 53; break;}
case 61:
- recEnd = pos; recKind = 81;
+ recEnd = pos; recKind = 80;
if (ch == '=') {AddCh(); goto case 40;}
else if (ch == '!') {AddCh(); goto case 41;}
- else {t.kind = 81; break;}
+ else {t.kind = 80; break;}
case 62:
- recEnd = pos; recKind = 76;
+ recEnd = pos; recKind = 74;
if (ch == '>') {AddCh(); goto case 32;}
- else {t.kind = 76; break;}
+ else {t.kind = 74; break;}
case 63:
- recEnd = pos; recKind = 77;
+ recEnd = pos; recKind = 75;
if (ch == '=') {AddCh(); goto case 29;}
- else {t.kind = 77; break;}
+ else {t.kind = 75; break;}
}
t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -788,7 +791,7 @@ void objectInvariant(){
}
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 9e28a6ec..61f3dad3 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3190,132 +3190,6 @@ namespace Microsoft.Dafny {
delegate(Bpl.StmtListBuilder bld, ExpressionTranslator e) { TrAlternatives(s.Alternatives, null, new Bpl.BreakCmd(s.Tok, null), bld, locals, e); },
builder, locals, etran);
- } else if (stmt is ForeachStmt) {
- AddComment(builder, stmt, "foreach statement");
- ForeachStmt s = (ForeachStmt)stmt;
- // assert/assume (forall o: ref :: o != null && o in S && Range(o) ==> Expr);
- // assert (forall o: ref :: o != null && o in S && Range(o) ==> IsTotal(RHS));
- // assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]); // this checks the enclosing modifies clause
- // var oldHeap := $Heap;
- // havoc $Heap;
- // assume $HeapSucc(oldHeap, $Heap);
- // assume (forall<alpha> o: ref, f: Field alpha :: $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && o in S && Range(o)));
- // assume (forall o: ref :: o != null && o in S && Range(o) ==> $Heap[o,F] = RHS[$Heap := oldHeap]);
- // Note, $Heap[o,alloc] is intentionally omitted from the antecedent of the quantifier in the previous line. That
- // allocatedness property should hold automatically, because the set/seq quantified is a program expression, which
- // will have been constructed from allocated objects.
- // For sets, "o in S" means just that. For sequences, "o in S" is:
- // (exists i :: { Seq#Index(S,i) } 0 <= i && i < Seq#Length(S) && Seq#Index(S,i) == o)
-
- Bpl.BoundVariable oVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.BoundVar.UniqueName, TrType(s.BoundVar.Type)));
- Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(stmt.Tok, oVar);
-
- // colection
- TrStmt_CheckWellformed(s.Collection, builder, locals, etran, true);
- Bpl.Expr oInS;
- if (s.Collection.Type is SetType) {
- oInS = etran.TrInSet(stmt.Tok, o, s.Collection, ((SetType)s.Collection.Type).Arg);
- } else if (s.Collection.Type is MultiSetType) {
- // should not be reached.
- Contract.Assert(false);
- throw new cce.UnreachableException();
- } else {
- Bpl.BoundVariable iVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$i", Bpl.Type.Int));
- Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(stmt.Tok, iVar);
- Bpl.Expr S = etran.TrExpr(s.Collection);
- Bpl.Expr range = InSeqRange(stmt.Tok, i, S, true, null, false);
- Bpl.Expr Si = FunctionCall(stmt.Tok, BuiltinFunction.SeqIndex, predef.BoxType, S, i);
- Bpl.Trigger tr = new Bpl.Trigger(stmt.Tok, true, new Bpl.ExprSeq(Si));
- // TODO: in the next line, the == should be replaced by something that understands extensionality, for sets and sequences
- var boxO = etran.BoxIfNecessary(stmt.Tok, o, ((SeqType)s.Collection.Type).Arg);
- oInS = new Bpl.ExistsExpr(stmt.Tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.And(range, Bpl.Expr.Eq(Si, boxO)));
- }
- oInS = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), oInS);
-
- // range
- Bpl.Expr qr = new Bpl.ForallExpr(s.Range.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(s.Range, etran)));
- builder.Add(AssertNS(s.Range.tok, qr, "range expression must be well defined"));
- oInS = Bpl.Expr.And(oInS, etran.TrExpr(s.Range));
-
- // sequence of asserts and assumes and uses
- foreach (PredicateStmt ps in s.BodyPrefix) {
- if (ps is AssertStmt || CommandLineOptions.Clo.DisallowSoundnessCheating) {
- Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, IsTotal(ps.Expr, etran)));
- builder.Add(AssertNS(ps.Expr.tok, q, "assert condition must be well defined")); // totality check
- bool splitHappened;
- var ss = TrSplitExpr(ps.Expr, etran, out splitHappened);
- if (!splitHappened) {
- Bpl.Expr e = etran.TrExpr(ps.Expr);
- q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
- builder.Add(Assert(ps.Expr.tok, q, "assertion violation"));
- } else {
- foreach (var split in ss) {
- if (!split.IsFree) {
- q = new Bpl.ForallExpr(split.E.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, split.E));
- builder.Add(AssertNS(split.E.tok, q, "assertion violation"));
- }
- }
- Bpl.Expr e = etran.TrExpr(ps.Expr);
- q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, e));
- builder.Add(new Bpl.AssumeCmd(ps.Expr.tok, q));
- }
- } else if (ps is AssumeStmt) {
- Bpl.Expr eIsTotal = IsTotal(ps.Expr, etran);
- Bpl.Expr q = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, eIsTotal));
- builder.Add(AssertNS(ps.Expr.tok, q, "assume condition must be well defined")); // totality check
- } else {
- Contract.Assert(false);
- }
- Bpl.Expr enchilada = etran.TrExpr(ps.Expr); // the whole enchilada
- Bpl.Expr qEnchilada = new Bpl.ForallExpr(ps.Expr.tok, new Bpl.VariableSeq(oVar), Bpl.Expr.Imp(oInS, enchilada));
- builder.Add(new Bpl.AssumeCmd(ps.Expr.tok, qEnchilada));
- }
-
- // Check RHS of assignment to be well defined
- ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;
- if (rhsExpr != null) {
- // assert (forall o: ref :: o != null && o in S && Range(o) ==> IsTotal(RHS));
- Bpl.Expr bbb = Bpl.Expr.Imp(oInS, IsTotal(rhsExpr.Expr, etran));
- Bpl.Expr qqq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), bbb);
- builder.Add(AssertNS(rhsExpr.Expr.tok, qqq, "RHS of assignment must be well defined")); // totality check
- }
-
- // Here comes: assert (forall o: ref :: o != null && o in S && Range(o) ==> $_Frame[o,F]);
- Bpl.Expr body = Bpl.Expr.Imp(oInS, Bpl.Expr.Select(etran.TheFrame(stmt.Tok), o, GetField((FieldSelectExpr)s.BodyAssign.Lhs)));
- Bpl.Expr qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
- builder.Add(Assert(s.BodyAssign.Tok, qq, "foreach assignment may update an object not in the enclosing method's modifies clause"));
-
- // Set up prevHeap
- Bpl.IdentifierExpr prevHeap = GetPrevHeapVar_IdExpr(stmt.Tok, locals);
- builder.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, prevHeap, etran.HeapExpr));
- builder.Add(new Bpl.HavocCmd(stmt.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));
- builder.Add(new Bpl.AssumeCmd(stmt.Tok, FunctionCall(stmt.Tok, BuiltinFunction.HeapSucc, null, prevHeap, etran.HeapExpr)));
-
- // Here comes: assume (forall<alpha> o: ref, f: Field alpha :: $Heap[o,f] = oldHeap[o,f] || (f = F && o != null && o in S && Range(o)));
- Bpl.TypeVariable alpha = new Bpl.TypeVariable(stmt.Tok, "alpha");
- Bpl.BoundVariable fVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$f", predef.FieldName(stmt.Tok, alpha)));
- Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(stmt.Tok, fVar);
- Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(stmt.Tok, etran.HeapExpr, o, f);
- Bpl.Expr oldHeapOF = ExpressionTranslator.ReadHeap(stmt.Tok, prevHeap, o, f);
- body = Bpl.Expr.Or(
- Bpl.Expr.Eq(heapOF, oldHeapOF),
- Bpl.Expr.And(
- Bpl.Expr.Eq(f, GetField((FieldSelectExpr)s.BodyAssign.Lhs)),
- oInS));
- qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), body);
- builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
-
- // Here comes: assume (forall o: ref :: o != null && o in S && Range(o) ==> $Heap[o,F] = RHS[$Heap := oldHeap]);
- if (rhsExpr != null) {
- Bpl.Expr heapOField = ExpressionTranslator.ReadHeap(stmt.Tok, etran.HeapExpr, o, GetField((FieldSelectExpr)(s.BodyAssign).Lhs));
- ExpressionTranslator oldEtran = new ExpressionTranslator(this, predef, prevHeap);
- body = Bpl.Expr.Imp(oInS, Bpl.Expr.Eq(heapOField, oldEtran.TrExpr(rhsExpr.Expr)));
- qq = new Bpl.ForallExpr(stmt.Tok, new Bpl.VariableSeq(oVar), body);
- builder.Add(new Bpl.AssumeCmd(stmt.Tok, qq));
- }
-
- builder.Add(CaptureState(stmt.Tok));
-
} else if (stmt is ParallelStmt) {
AddComment(builder, stmt, "parallel statement");
var s = (ParallelStmt)stmt;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 697bdd9e..04d60716 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -173,11 +173,18 @@ SmallTests.dfy(131,9): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-SmallTests.dfy(171,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
+SmallTests.dfy(171,9): Error: assignment may update an object field not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
- (0,0): anon4_Else
- (0,0): anon3
+ (0,0): anon22_Else
+ (0,0): anon5
+ (0,0): anon24_Else
+ (0,0): anon11
+ (0,0): anon26_Else
+ (0,0): anon16
+ (0,0): anon28_Then
+ (0,0): anon29_Then
+ (0,0): anon19
SmallTests.dfy(199,14): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -374,46 +381,37 @@ Execution trace:
(0,0): anon23_Then
(0,0): anon24_Then
(0,0): anon11
-Definedness.dfy(199,24): Error: possible violation of function precondition
+Definedness.dfy(193,19): Error: possible division by zero
Execution trace:
(0,0): anon0
-Definedness.dfy(201,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause
-Execution trace:
- (0,0): anon0
-Definedness.dfy(203,33): Error: range expression must be well defined
-Execution trace:
- (0,0): anon0
-Definedness.dfy(218,19): Error: possible division by zero
-Execution trace:
- (0,0): anon0
- Definedness.dfy(216,5): anon7_LoopHead
+ Definedness.dfy(191,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(218,23): Error BP5004: This loop invariant might not hold on entry.
+Definedness.dfy(193,23): Error BP5004: This loop invariant might not hold on entry.
Execution trace:
(0,0): anon0
-Definedness.dfy(218,28): Error: possible division by zero
+Definedness.dfy(193,28): Error: possible division by zero
Execution trace:
(0,0): anon0
- Definedness.dfy(216,5): anon7_LoopHead
+ Definedness.dfy(191,5): anon7_LoopHead
(0,0): anon7_LoopBody
(0,0): anon8_Then
-Definedness.dfy(239,46): Error: possible violation of function postcondition
+Definedness.dfy(214,46): Error: possible violation of function postcondition
Execution trace:
(0,0): anon0
(0,0): anon5_Else
-Definedness.dfy(246,22): Error: target object may be null
+Definedness.dfy(221,22): Error: target object may be null
Execution trace:
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Definedness.dfy(262,24): Error: possible violation of function postcondition
+Definedness.dfy(237,24): Error: possible violation of function postcondition
Execution trace:
(0,0): anon7_Then
(0,0): anon2
(0,0): anon8_Else
-Dafny program verifier finished with 23 verified, 39 errors
+Dafny program verifier finished with 22 verified, 36 errors
-------------------- FunctionSpecifications.dfy --------------------
FunctionSpecifications.dfy(28,13): Error: possible violation of function postcondition
@@ -1128,21 +1126,25 @@ TypeAntecedents.dfy(55,1): Error BP5003: A postcondition might not hold on this
TypeAntecedents.dfy(54,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
- (0,0): anon15_Then
+ (0,0): anon25_Then
(0,0): anon6
- (0,0): anon18_Then
+ (0,0): anon28_Then
(0,0): anon8
- (0,0): anon19_Then
- (0,0): anon10
- (0,0): anon20_Then
- (0,0): anon21_Then
- (0,0): anon14
+ (0,0): anon29_Else
+ (0,0): anon13
+ (0,0): anon31_Else
+ (0,0): anon18
+ (0,0): anon33_Then
+ (0,0): anon20
+ (0,0): anon34_Then
+ (0,0): anon35_Then
+ (0,0): anon24
TypeAntecedents.dfy(63,16): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon15_Else
- (0,0): anon16_Then
- (0,0): anon17_Else
+ (0,0): anon25_Else
+ (0,0): anon26_Then
+ (0,0): anon27_Else
Dafny program verifier finished with 12 verified, 3 errors
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 44b54f3d..f99d1503 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -185,31 +185,6 @@ class StatementTwoShoes {
function G(w: int): int { 5 }
function method H(x: int): int { -x }
- method V(s: set<StatementTwoShoes>, a: int, b: int)
- modifies s;
- {
-
- foreach (m in s | m.x < 200) // s may contain null, but the foreach excludes null
- {
- assume 0 <= m.x;
- assert m.x < 1000;
-
- m.x := m.x + 1;
- }
- foreach (m in s + {F(a)}) // error: collection expression may not be well defined (fn precondition)
- {
- m.x := 5; // error: possible modifies clause violation
- }
- foreach (m in s | F(H(m.x)) == this) // error: range expression may not be well defined
- {
- m.x := H(m.x);
- }
- foreach (m in s)
- {
- m.x := 100 / m.x; // error: RhS may not be well defined
- }
- }
-
method W(x: int)
{
var i := 0;
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 439930b5..d4a0ad9a 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -144,7 +144,7 @@ class Modifies {
method F(s: set<Modifies>)
modifies s;
{
- foreach (m in s | 2 <= m.x) {
+ parallel (m | m in s && m != null && 2 <= m.x) {
m.x := m.x + 1;
}
if (this in s) {
@@ -157,17 +157,17 @@ class Modifies {
{
var m := 3; // this is a different m
- foreach (m in s | m == this) {
+ parallel (m | m in s && m == this) {
m.x := m.x + 1;
}
if (s <= {this}) {
- foreach (m in s) {
+ parallel (m | m in s) {
m.x := m.x + 1;
}
F(s);
}
- foreach (m in s) {
- assert m.x < m.x + 10; // nothing wrong with asserting something
+ parallel (m | m in s) ensures true; { assert m == null || m.x < m.x + 10; }
+ parallel (m | m != null && m in s) {
m.x := m.x + 1; // error: may violate modifies clause
}
}
@@ -322,10 +322,10 @@ class SomeType
{
var x: int;
method DoIt(stack: seq<SomeType>)
+ requires null !in stack;
modifies stack;
{
- // the following line once gave rise to a crash in the translation
- foreach (n in stack) {
+ parallel (n | n in stack) {
n.x := 10;
}
}
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 5982a9e6..b6ef0d68 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -68,8 +68,8 @@ method M(list: List, S: set<MyClass>) returns (ret: int)
ghost var l := NF();
assert l != null ==> l.H() == 5;
- foreach (s in S) {
- assert s == null || s.H() == 5;
+ parallel (s | s in S) ensures true; { assert s == null || s.H() == 5; }
+ parallel (s | s != null && s in S) {
s.x := 0;
}
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 98006cca..cf603751 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -37,7 +37,7 @@
)) . font-lock-builtin-face)
`(,(dafny-regexp-opt '(
"assert" "assume" "break" "choose" "then" "else" "havoc" "if" "label" "return" "while" "print"
- "old" "forall" "exists" "new" "foreach" "parallel" "in" "this" "fresh" "allocated"
+ "old" "forall" "exists" "new" "parallel" "in" "this" "fresh" "allocated"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "nat" "int" "object" "set" "seq")) . font-lock-type-face)
)
diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 8fc8bf4e..6f9ec810 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -20,7 +20,7 @@ namespace Demo
"assert", "assume", "new", "this", "object", "refines", "replaces", "by",
"unlimited", "module", "imports",
"if", "then", "else", "while", "invariant",
- "break", "label", "return", "foreach", "parallel", "havoc", "print",
+ "break", "label", "return", "parallel", "havoc", "print",
"returns", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
"function", "free",
@@ -238,7 +238,6 @@ namespace Demo
| "if" + Condition + Statement + PreferShiftHere() + "else" + Statement
| "while" + Condition + loopSpec.Star() + Statement
| "for" + LParen + expression.Q() + Semi + expression.Q() + Semi + expression.Q() + RParen + Statement
- | "foreach" + LParen + ident + "in" + expression + RParen + Statement
| blockStatement
| expression + Semi
| "break" + Semi
@@ -286,7 +285,6 @@ namespace Demo
| "break"
| "label"
| "return"
- | "foreach"
| "parallel"
| "havoc"
| "print"
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 5e61d2d6..f80acc26 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -251,7 +251,6 @@ namespace DafnyLanguage
case "exists":
case "false":
case "forall":
- case "foreach":
case "free":
case "fresh":
case "function":
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index 809c6fc4..1bbab1b7 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -13,7 +13,7 @@
% expressions
match,case,false,true,null,old,fresh,allocated,choose,this,
% statements
- assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,foreach,parallel,
+ assert,assume,print,new,havoc,if,then,else,while,invariant,break,label,return,parallel,
},
literate=%
{:}{$\colon$}1
diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index 4014e427..2d0aeab3 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -8,7 +8,7 @@ syntax case match
syntax keyword dafnyFunction function method constructor
syntax keyword dafnyTypeDef class datatype
syntax keyword dafnyConditional if then else match case
-syntax keyword dafnyRepeat foreach while parallel
+syntax keyword dafnyRepeat while parallel
syntax keyword dafnyStatement havoc assume assert return new print break label
syntax keyword dafnyKeyword var ghost returns null static this refines replaces by
syntax keyword dafnyType bool nat int seq set object array array2 array3
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 15:00:12 +0000