diff options
34 files changed, 478 insertions, 447 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 8cd2f4ae..dbbb6a40 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -448,9 +448,9 @@ namespace Microsoft.Dafny var s = (AlternativeLoopStmt)stmt;
r = new AlternativeLoopStmt(Tok(s.Tok), s.Invariants.ConvertAll(CloneMayBeFreeExpr), CloneSpecExpr(s.Decreases), CloneSpecFrameExpr(s.Mod), s.Alternatives.ConvertAll(CloneGuardedAlternative));
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
- r = new ParallelStmt(Tok(s.Tok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
+ r = new ForallStmt(Tok(s.Tok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
} else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 60084fb8..6e5dd2ef 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1163,26 +1163,26 @@ namespace Microsoft.Dafny { wr.WriteLine("}");
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
- if (s.Kind != ParallelStmt.ParBodyKind.Assign) {
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
+ if (s.Kind != ForallStmt.ParBodyKind.Assign) {
// Call and Proof have no side effects, so they can simply be optimized away.
return;
} else if (s.BoundVars.Count == 0) {
- // the bound variables just spell out a single point, so the parallel statement is equivalent to one execution of the body
+ // the bound variables just spell out a single point, so the forall statement is equivalent to one execution of the body
TrStmt(s.Body, indent);
return;
}
var s0 = (AssignStmt)s.S0;
if (s0.Rhs is HavocRhs) {
- // The parallel statement says to havoc a bunch of things. This can be efficiently compiled
+ // The forall statement says to havoc a bunch of things. This can be efficiently compiled
// into doing nothing.
return;
}
var rhs = ((ExprRhs)s0.Rhs).Expr;
// Compile:
- // parallel (w,x,y,z | Range(w,x,y,z)) {
+ // forall (w,x,y,z | Range(w,x,y,z)) {
// LHS(w,x,y,z) := RHS(w,x,y,z);
// }
// where w,x,y,z have types seq<W>,set<X>,int,bool and LHS has L-1 top-level subexpressions
@@ -1206,7 +1206,7 @@ namespace Microsoft.Dafny { //
// Note, because the .NET Tuple class only supports up to 8 components, the compiler implementation
// here supports arrays only up to 6 dimensions. This does not seem like a serious practical limitation.
- // However, it may be more noticeable if the parallel statement supported parallel assignments in its
+ // However, it may be more noticeable if the forall statement supported forall assignments in its
// body. To support cases where tuples would need more than 8 components, .NET Tuple's would have to
// be nested.
@@ -1231,7 +1231,7 @@ namespace Microsoft.Dafny { var lhs = (MultiSelectExpr)s0.Lhs;
L = 2 + lhs.Indices.Count;
if (8 < L) {
- Error("compiler currently does not support assignments to more-than-6-dimensional arrays in parallel statements");
+ Error("compiler currently does not support assignments to more-than-6-dimensional arrays in forall statements");
return;
}
tupleTypeArgs = TypeName(lhs.Array.Type);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 11b373cc..c52c33f1 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -881,7 +881,7 @@ OneStmt<out Statement/*!*/ s> | IfStmt<out s>
| WhileStmt<out s>
| MatchStmt<out s>
- | ParallelStmt<out s>
+ | ForallStmt<out s>
| CalcStmt<out s>
| "label" (. x = t; .)
NoUSIdent<out id> ":"
@@ -1298,9 +1298,10 @@ PrintStmt<out Statement/*!*/ s> ";" (. s = new PrintStmt(x, args); .)
.
-ParallelStmt<out Statement/*!*/ s>
+ForallStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- IToken/*!*/ x;
+ IToken/*!*/ x = Token.NoToken;
+ bool usesOptionalParen = false;
List<BoundVar/*!*/> bvars = null;
Attributes attrs = null;
Expression range = null;
@@ -1310,8 +1311,13 @@ ParallelStmt<out Statement/*!*/ s> BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
.)
- "parallel" (. x = t; .)
- "("
+ ( "forall" (. x = t; .)
+ | "parallel" (. x = t;
+ errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
+ .)
+ )
+ [ "(" (. usesOptionalParen = true; .)
+ ]
[ (. List<BoundVar/*!*/> bvarsX; Attributes attrsX; Expression rangeX; .)
QuantifierDomain<out bvarsX, out attrsX, out rangeX>
(. bvars = bvarsX; attrs = attrsX; range = rangeX;
@@ -1320,14 +1326,16 @@ ParallelStmt<out Statement/*!*/ s> (. if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
.)
- ")"
+ ( ")" (. if (!usesOptionalParen) { SemErr(t, "found but didn't expect a close parenthesis"); } .)
+ | (. if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); } .)
+ )
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
]
"ensures" Expression<out e> ";" (. ens.Add(new MaybeFreeExpression(e, isFree)); .)
}
BlockStmt<out block, out bodyStart, out bodyEnd>
- (. s = new ParallelStmt(x, bvars, attrs, range, ens, block); .)
+ (. s = new ForallStmt(x, bvars, attrs, range, ens, block); .)
.
CalcStmt<out Statement/*!*/ s>
@@ -1929,7 +1937,7 @@ QuantifierDomain<.out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expre { ","
IdentTypeOptional<out bv> (. bvars.Add(bv); .)
}
- { Attribute<ref attrs> }
+ { IF(IsAttribute()) Attribute<ref attrs> }
[ "|"
Expression<out range>
]
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index e1b1ed15..281bd466 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2957,7 +2957,7 @@ namespace Microsoft.Dafny { }
}
- public class ParallelStmt : Statement
+ public class ForallStmt : Statement
{
public readonly List<BoundVar/*!*/> BoundVars; // note, can be the empty list, in which case Range denotes "true"
public readonly Expression/*!*/ Range;
@@ -2980,7 +2980,7 @@ namespace Microsoft.Dafny { /// * More kinds may be allowed in the future.
/// * One could also allow Call to call non-ghost methods without side effects. However, that
/// would seem pointless in the program, so they are disallowed (to avoid any confusion that
- /// such use of the parallel statement might actually have a point).
+ /// such use of the forall statement might actually have a point).
/// * One could allow Proof even without ensures clauses that "export" what was learned.
/// However, that might give the false impression that the body is nevertheless exported.
/// </summary>
@@ -2996,7 +2996,7 @@ namespace Microsoft.Dafny { Contract.Invariant(Body != null);
}
- public ParallelStmt(IToken tok, List<BoundVar> boundVars, Attributes attrs, Expression range, List<MaybeFreeExpression/*!*/>/*!*/ ens, Statement body)
+ public ForallStmt(IToken tok, List<BoundVar> boundVars, Attributes attrs, Expression range, List<MaybeFreeExpression/*!*/>/*!*/ ens, Statement body)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(boundVars));
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index ba95908b..7252c56f 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1413,7 +1413,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo PrintStmt(out s);
break;
}
- case 1: case 2: case 24: case 28: case 104: case 105: case 106: case 107: case 108: case 109: {
+ case 1: case 2: case 24: case 28: case 105: case 106: case 107: case 108: case 109: case 110: {
UpdateStmt(out s);
break;
}
@@ -1433,11 +1433,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo MatchStmt(out s);
break;
}
- case 80: {
- ParallelStmt(out s);
+ case 80: case 81: {
+ ForallStmt(out s);
break;
}
- case 81: {
+ case 82: {
CalcStmt(out s);
break;
}
@@ -1782,9 +1782,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s = new MatchStmt(x, e, cases);
}
- void ParallelStmt(out Statement/*!*/ s) {
+ void ForallStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
- IToken/*!*/ x;
+ IToken/*!*/ x = Token.NoToken;
+ bool usesOptionalParen = false;
List<BoundVar/*!*/> bvars = null;
Attributes attrs = null;
Expression range = null;
@@ -1794,9 +1795,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
- Expect(80);
- x = t;
- Expect(28);
+ if (la.kind == 80) {
+ Get();
+ x = t;
+ } else if (la.kind == 81) {
+ Get();
+ x = t;
+ errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
+
+ } else SynErr(176);
+ if (la.kind == 28) {
+ Get();
+ usesOptionalParen = true;
+ }
if (la.kind == 1) {
List<BoundVar/*!*/> bvarsX; Attributes attrsX; Expression rangeX;
QuantifierDomain(out bvarsX, out attrsX, out rangeX);
@@ -1806,7 +1817,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
- Expect(30);
+ if (la.kind == 30) {
+ Get();
+ if (!usesOptionalParen) { SemErr(t, "found but didn't expect a close parenthesis"); }
+ } else if (la.kind == 6 || la.kind == 41 || la.kind == 43) {
+ if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); }
+ } else SynErr(177);
while (la.kind == 41 || la.kind == 43) {
isFree = false;
if (la.kind == 41) {
@@ -1819,7 +1835,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ens.Add(new MaybeFreeExpression(e, isFree));
}
BlockStmt(out block, out bodyStart, out bodyEnd);
- s = new ParallelStmt(x, bvars, attrs, range, ens, block);
+ s = new ForallStmt(x, bvars, attrs, range, ens, block);
}
void CalcStmt(out Statement/*!*/ s) {
@@ -1835,7 +1851,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ h;
IToken opTok;
- Expect(81);
+ Expect(82);
x = t;
if (StartOf(19)) {
CalcOp(out opTok, out calcOp);
@@ -1887,7 +1903,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 46) {
Get();
returnTok = t; isYield = true;
- } else SynErr(176);
+ } else SynErr(178);
if (StartOf(21)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
@@ -1993,7 +2009,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(14)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(177);
+ } else SynErr(179);
while (la.kind == 6) {
Attribute(ref attrs);
}
@@ -2014,7 +2030,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 18 || la.kind == 68) {
Suffix(ref e);
}
- } else SynErr(178);
+ } else SynErr(180);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -2059,7 +2075,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(18)) {
BareGuard(out ee);
e = ee;
- } else SynErr(179);
+ } else SynErr(181);
}
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
@@ -2072,20 +2088,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (StartOf(23)) {
if (la.kind == 41 || la.kind == 76) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(180); Get();}
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(182); Get();}
Expect(15);
invariants.Add(invariant);
} else if (la.kind == 44) {
- while (!(la.kind == 0 || la.kind == 44)) {SynErr(181); Get();}
+ while (!(la.kind == 0 || la.kind == 44)) {SynErr(183); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(182); Get();}
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(184); Get();}
Expect(15);
} else {
- while (!(la.kind == 0 || la.kind == 40)) {SynErr(183); Get();}
+ while (!(la.kind == 0 || la.kind == 40)) {SynErr(185); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -2100,7 +2116,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 15)) {SynErr(184); Get();}
+ while (!(la.kind == 0 || la.kind == 15)) {SynErr(186); Get();}
Expect(15);
}
}
@@ -2108,7 +2124,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 41 || la.kind == 76)) {SynErr(185); Get();}
+ while (!(la.kind == 0 || la.kind == 41 || la.kind == 76)) {SynErr(187); Get();}
if (la.kind == 41) {
Get();
isFree = true;
@@ -2129,7 +2145,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(14)) {
Expression(out ee);
e = ee;
- } else SynErr(186);
+ } else SynErr(188);
}
void CaseStatement(out MatchCaseStmt/*!*/ c) {
@@ -2168,7 +2184,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(14)) {
Expression(out e);
arg = new Attributes.Argument(t, e);
- } else SynErr(187);
+ } else SynErr(189);
}
void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {
@@ -2184,7 +2200,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
bvars.Add(bv);
}
- while (la.kind == 6) {
+ while (IsAttribute()) {
Attribute(ref attrs);
}
if (la.kind == 24) {
@@ -2214,47 +2230,47 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 84: {
+ case 85: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 85: {
+ case 86: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 86: {
+ case 87: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 87: {
+ case 88: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 88: case 89: {
+ case 89: case 90: {
EquivOp();
x = t; op = BinaryExpr.Opcode.Iff;
break;
}
- case 90: case 91: {
+ case 91: case 92: {
ImpliesOp();
x = t; op = BinaryExpr.Opcode.Imp;
break;
}
- default: SynErr(188); break;
+ default: SynErr(190); break;
}
}
@@ -2266,7 +2282,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Statement/*!*/ calc;
Token x = la;
- while (la.kind == 6 || la.kind == 81) {
+ while (la.kind == 6 || la.kind == 82) {
if (la.kind == 6) {
BlockStmt(out block, out bodyStart, out bodyEnd);
subhints.Add(block);
@@ -2280,25 +2296,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void EquivOp() {
- if (la.kind == 88) {
+ if (la.kind == 89) {
Get();
- } else if (la.kind == 89) {
+ } else if (la.kind == 90) {
Get();
- } else SynErr(189);
+ } else SynErr(191);
}
void ImpliesOp() {
- if (la.kind == 90) {
+ if (la.kind == 91) {
Get();
- } else if (la.kind == 91) {
+ } else if (la.kind == 92) {
Get();
- } else SynErr(190);
+ } else SynErr(192);
}
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 88 || la.kind == 89) {
+ while (la.kind == 89 || la.kind == 90) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -2309,7 +2325,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 90 || la.kind == 91) {
+ if (la.kind == 91 || la.kind == 92) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -2321,12 +2337,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(24)) {
- if (la.kind == 92 || la.kind == 93) {
+ if (la.kind == 93 || la.kind == 94) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 92 || la.kind == 93) {
+ while (la.kind == 93 || la.kind == 94) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -2337,7 +2353,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 94 || la.kind == 95) {
+ while (la.kind == 95 || la.kind == 96) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -2449,25 +2465,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AndOp() {
- if (la.kind == 92) {
+ if (la.kind == 93) {
Get();
- } else if (la.kind == 93) {
+ } else if (la.kind == 94) {
Get();
- } else SynErr(191);
+ } else SynErr(193);
}
void OrOp() {
- if (la.kind == 94) {
+ if (la.kind == 95) {
Get();
- } else if (la.kind == 95) {
+ } else if (la.kind == 96) {
Get();
- } else SynErr(192);
+ } else SynErr(194);
}
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 == 99 || la.kind == 100) {
+ while (la.kind == 100 || la.kind == 101) {
AddOp(out x, out op);
Factor(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2484,7 +2500,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo case 29: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
Expect(68);
Expression(out k);
@@ -2502,20 +2518,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 82: {
+ case 83: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 84: {
+ case 85: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
Expect(68);
Expression(out k);
@@ -2523,7 +2539,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
break;
}
- case 97: {
+ case 98: {
Get();
x = t; op = BinaryExpr.Opcode.In;
break;
@@ -2533,10 +2549,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.NotIn;
break;
}
- case 98: {
+ case 99: {
Get();
x = t; y = Token.NoToken;
- if (la.kind == 98) {
+ if (la.kind == 99) {
Get();
y = t;
}
@@ -2551,29 +2567,29 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break;
}
- case 85: {
+ case 86: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 86: {
+ case 87: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 87: {
+ case 88: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(193); break;
+ default: SynErr(195); 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 == 58 || la.kind == 101 || la.kind == 102) {
+ while (la.kind == 58 || la.kind == 102 || la.kind == 103) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2582,33 +2598,33 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo 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 == 99) {
+ if (la.kind == 100) {
Get();
x = t; op = BinaryExpr.Opcode.Add;
- } else if (la.kind == 100) {
+ } else if (la.kind == 101) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(194);
+ } else SynErr(196);
}
void UnaryExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr;
switch (la.kind) {
- case 100: {
+ case 101: {
Get();
x = t;
UnaryExpression(out e);
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 98: case 103: {
+ case 99: case 104: {
NegOp();
x = t;
UnaryExpression(out e);
e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 25: case 50: case 60: case 66: case 71: case 77: case 78: case 81: case 112: case 113: case 114: case 115: {
+ case 25: case 50: case 60: case 66: case 71: case 77: case 78: case 80: case 82: case 113: case 114: case 115: {
EndlessExpression(out e);
break;
}
@@ -2645,17 +2661,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo MapComprehensionExpr(x, out e);
} else if (StartOf(26)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(195);
+ } else SynErr(197);
break;
}
- case 2: case 24: case 28: case 104: case 105: case 106: case 107: case 108: case 109: {
+ case 2: case 24: case 28: case 105: case 106: case 107: case 108: case 109: case 110: {
ConstAtomExpression(out e);
while (la.kind == 18 || la.kind == 68) {
Suffix(ref e);
}
break;
}
- default: SynErr(196); break;
+ default: SynErr(198); break;
}
}
@@ -2664,21 +2680,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 58) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
- } else if (la.kind == 101) {
+ } else if (la.kind == 102) {
Get();
x = t; op = BinaryExpr.Opcode.Div;
- } else if (la.kind == 102) {
+ } else if (la.kind == 103) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(197);
+ } else SynErr(199);
}
void NegOp() {
- if (la.kind == 98) {
+ if (la.kind == 99) {
Get();
- } else if (la.kind == 103) {
+ } else if (la.kind == 104) {
Get();
- } else SynErr(198);
+ } else SynErr(200);
}
void EndlessExpression(out Expression e) {
@@ -2692,7 +2708,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
x = t;
Expression(out e);
- Expect(110);
+ Expect(111);
Expression(out e0);
Expect(72);
Expression(out e1);
@@ -2703,7 +2719,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo MatchExpression(out e);
break;
}
- case 112: case 113: case 114: case 115: {
+ case 80: case 113: case 114: case 115: {
QuantifierGuts(out e);
break;
}
@@ -2729,7 +2745,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AssumeExpr(x, e0, e1);
break;
}
- case 81: {
+ case 82: {
CalcStmt(out s);
Expression(out e1);
e = new CalcExpr(s.Tok, (CalcStmt)s, e1);
@@ -2743,7 +2759,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo NamedExpr(out e);
break;
}
- default: SynErr(199); break;
+ default: SynErr(201); break;
}
}
@@ -2759,9 +2775,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id);
idents.Add(id);
}
- if (la.kind == 28 || la.kind == 96) {
+ if (la.kind == 28 || la.kind == 97) {
args = new List<Expression>();
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
id.val = id.val + "#"; Expression k;
Expect(68);
@@ -2788,9 +2804,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 18) {
Get();
Ident(out id);
- if (la.kind == 28 || la.kind == 96) {
+ if (la.kind == 28 || la.kind == 97) {
args = new List<Expression/*!*/>(); func = true;
- if (la.kind == 96) {
+ if (la.kind == 97) {
Get();
id.val = id.val + "#"; Expression k;
Expect(68);
@@ -2813,7 +2829,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(14)) {
Expression(out ee);
e0 = ee;
- if (la.kind == 111) {
+ if (la.kind == 112) {
Get();
anyDots = true;
if (StartOf(14)) {
@@ -2835,15 +2851,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee);
}
- } else SynErr(200);
- } else if (la.kind == 111) {
+ } else SynErr(202);
+ } else if (la.kind == 112) {
Get();
anyDots = true;
if (StartOf(14)) {
Expression(out ee);
e1 = ee;
}
- } else SynErr(201);
+ } else SynErr(203);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -2867,7 +2883,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(69);
- } else SynErr(202);
+ } else SynErr(204);
}
void DisplayExpr(out Expression e) {
@@ -2891,7 +2907,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SeqDisplayExpr(x, elements);
Expect(69);
- } else SynErr(203);
+ } else SynErr(205);
}
void MultiSetExpr(out Expression e) {
@@ -2917,7 +2933,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(30);
} else if (StartOf(27)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(204);
+ } else SynErr(206);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -2958,17 +2974,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = dummyExpr;
switch (la.kind) {
- case 104: {
+ case 105: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 105: {
+ case 106: {
Get();
e = new LiteralExpr(t, true);
break;
}
- case 106: {
+ case 107: {
Get();
e = new LiteralExpr(t);
break;
@@ -2978,12 +2994,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new LiteralExpr(t, n);
break;
}
- case 107: {
+ case 108: {
Get();
e = new ThisExpr(t);
break;
}
- case 108: {
+ case 109: {
Get();
x = t;
Expect(28);
@@ -2992,7 +3008,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new FreshExpr(x, e);
break;
}
- case 109: {
+ case 110: {
Get();
x = t;
Expect(28);
@@ -3017,7 +3033,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(30);
break;
}
- default: SynErr(205); break;
+ default: SynErr(207); break;
}
}
@@ -3053,7 +3069,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 117) {
Get();
- } else SynErr(206);
+ } else SynErr(208);
}
void MatchExpression(out Expression/*!*/ e) {
@@ -3078,13 +3094,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression range;
Expression/*!*/ body;
- if (la.kind == 112 || la.kind == 113) {
+ if (la.kind == 80 || la.kind == 113) {
Forall();
x = t; univ = true;
} else if (la.kind == 114 || la.kind == 115) {
Exists();
x = t;
- } else SynErr(207);
+ } else SynErr(209);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body);
@@ -3147,7 +3163,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 65) {
Get();
exact = false;
- } else SynErr(208);
+ } else SynErr(210);
Expression(out e);
letRHSs.Add(e);
while (la.kind == 26) {
@@ -3200,11 +3216,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void Forall() {
- if (la.kind == 112) {
+ if (la.kind == 80) {
Get();
} else if (la.kind == 113) {
Get();
- } else SynErr(209);
+ } else SynErr(211);
}
void Exists() {
@@ -3212,7 +3228,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get();
} else if (la.kind == 115) {
Get();
- } else SynErr(210);
+ } else SynErr(212);
}
void AttributeBody(ref Attributes attrs) {
@@ -3248,7 +3264,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,T,T, T,T,x,x, T,x,x,T, x,x,T,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, T,T,x,x, T,x,T,x, x,x,x,T, 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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
+ {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,T,T, T,T,x,x, T,x,x,T, x,x,T,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, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,x, x,x,x,T, T,T,T,T, x,T,x,T, x,x,x,T, x,x,x,x, x,T,T,T, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, 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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x},
@@ -3258,25 +3274,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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},
{x,T,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,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},
{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, 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,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,x,T, 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,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,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,T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,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, T,T,x,x, T,x,T,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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,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, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, x,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,T,T,T, T,T,T,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, 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,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, 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,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,T,T, T,x,x,x, x,x,T,x, T,x,x,T, 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,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,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, T,T,x,x, T,x,T,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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
- {x,T,T,x, x,x,T,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, 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,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, 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,T,x, T,x,x,T, T,T,T,T, T,T,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,T,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,T, x,x,x,x},
- {x,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,T, T,x,T,T, 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,T,x, T,x,x,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, x,x,x,x, x,x,x,x, T,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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,T,T, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,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, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, x,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,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x},
+ {x,T,T,x, x,x,T,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,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,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,T,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x},
+ {x,T,T,x, x,x,T,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,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, 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, T,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,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, 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, 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,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, T,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,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,T,T, T,T,T,T, 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,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, x,T,x,x, T,T,T,x, T,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,x, T,T,x,x},
- {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, T,T,x,x, T,T,T,x, T,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,x, x,x,x,x, x,x,T,T, x,x,x,x, T,T,x,x},
- {x,T,T,x, T,x,T,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,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, 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,T,x, T,x,x,T, T,T,T,T, T,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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, T,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,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,T, T,T,T,T, T,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,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, x,T,x,x, T,T,T,x, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, T,T,x,x},
+ {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,T, x,x,x,x, T,T,x,x, T,T,T,x, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,T, T,x,x,x, T,T,x,x},
+ {x,T,T,x, T,x,T,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,T,T, x,T,x,x, x,x,x,x, T,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,T,T,T, T,T,T,x, x,T,T,T, x,x,x,x}
};
} // end Parser
@@ -3381,39 +3397,39 @@ public class Errors { case 77: s = "\"match\" expected"; break;
case 78: s = "\"assert\" expected"; break;
case 79: s = "\"print\" expected"; break;
- case 80: s = "\"parallel\" expected"; break;
- case 81: s = "\"calc\" expected"; break;
- case 82: s = "\"<=\" expected"; break;
- case 83: s = "\">=\" expected"; break;
- case 84: s = "\"!=\" expected"; break;
- case 85: s = "\"\\u2260\" expected"; break;
- case 86: s = "\"\\u2264\" expected"; break;
- case 87: s = "\"\\u2265\" expected"; break;
- case 88: s = "\"<==>\" expected"; break;
- case 89: s = "\"\\u21d4\" expected"; break;
- case 90: s = "\"==>\" expected"; break;
- case 91: s = "\"\\u21d2\" expected"; break;
- case 92: s = "\"&&\" expected"; break;
- case 93: s = "\"\\u2227\" expected"; break;
- case 94: s = "\"||\" expected"; break;
- case 95: s = "\"\\u2228\" expected"; break;
- case 96: s = "\"#\" expected"; break;
- case 97: s = "\"in\" expected"; break;
- case 98: s = "\"!\" expected"; break;
- case 99: s = "\"+\" expected"; break;
- case 100: s = "\"-\" expected"; break;
- case 101: s = "\"/\" expected"; break;
- case 102: s = "\"%\" expected"; break;
- case 103: s = "\"\\u00ac\" expected"; break;
- case 104: s = "\"false\" expected"; break;
- case 105: s = "\"true\" expected"; break;
- case 106: s = "\"null\" expected"; break;
- case 107: s = "\"this\" expected"; break;
- case 108: s = "\"fresh\" expected"; break;
- case 109: s = "\"old\" expected"; break;
- case 110: s = "\"then\" expected"; break;
- case 111: s = "\"..\" expected"; break;
- case 112: s = "\"forall\" expected"; break;
+ case 80: s = "\"forall\" expected"; break;
+ case 81: s = "\"parallel\" expected"; break;
+ case 82: s = "\"calc\" expected"; break;
+ case 83: s = "\"<=\" expected"; break;
+ case 84: s = "\">=\" expected"; break;
+ case 85: s = "\"!=\" expected"; break;
+ case 86: s = "\"\\u2260\" expected"; break;
+ case 87: s = "\"\\u2264\" expected"; break;
+ case 88: s = "\"\\u2265\" expected"; break;
+ case 89: s = "\"<==>\" expected"; break;
+ case 90: s = "\"\\u21d4\" expected"; break;
+ case 91: s = "\"==>\" expected"; break;
+ case 92: s = "\"\\u21d2\" expected"; break;
+ case 93: s = "\"&&\" expected"; break;
+ case 94: s = "\"\\u2227\" expected"; break;
+ case 95: s = "\"||\" expected"; break;
+ case 96: s = "\"\\u2228\" expected"; break;
+ case 97: s = "\"#\" expected"; break;
+ case 98: s = "\"in\" expected"; break;
+ case 99: s = "\"!\" expected"; break;
+ case 100: s = "\"+\" expected"; break;
+ case 101: s = "\"-\" expected"; break;
+ case 102: s = "\"/\" expected"; break;
+ case 103: s = "\"%\" expected"; break;
+ case 104: s = "\"\\u00ac\" expected"; break;
+ case 105: s = "\"false\" expected"; break;
+ case 106: s = "\"true\" expected"; break;
+ case 107: s = "\"null\" expected"; break;
+ case 108: s = "\"this\" expected"; break;
+ case 109: s = "\"fresh\" expected"; break;
+ case 110: s = "\"old\" expected"; break;
+ case 111: s = "\"then\" expected"; break;
+ case 112: s = "\"..\" expected"; break;
case 113: s = "\"\\u2200\" expected"; break;
case 114: s = "\"exists\" expected"; break;
case 115: s = "\"\\u2203\" expected"; break;
@@ -3477,41 +3493,43 @@ public class Errors { case 173: s = "invalid IfStmt"; break;
case 174: s = "invalid WhileStmt"; break;
case 175: s = "invalid WhileStmt"; break;
- case 176: s = "invalid ReturnStmt"; break;
- case 177: s = "invalid Rhs"; break;
- case 178: s = "invalid Lhs"; break;
- case 179: s = "invalid Guard"; break;
- case 180: s = "this symbol not expected in LoopSpec"; break;
- case 181: s = "this symbol not expected in LoopSpec"; break;
+ case 176: s = "invalid ForallStmt"; break;
+ case 177: s = "invalid ForallStmt"; break;
+ case 178: s = "invalid ReturnStmt"; break;
+ case 179: s = "invalid Rhs"; break;
+ case 180: s = "invalid Lhs"; break;
+ case 181: s = "invalid Guard"; break;
case 182: s = "this symbol not expected in LoopSpec"; break;
case 183: s = "this symbol not expected in LoopSpec"; break;
case 184: s = "this symbol not expected in LoopSpec"; break;
- case 185: s = "this symbol not expected in Invariant"; break;
- case 186: s = "invalid BareGuard"; break;
- case 187: s = "invalid AttributeArg"; break;
- case 188: s = "invalid CalcOp"; break;
- case 189: s = "invalid EquivOp"; break;
- case 190: s = "invalid ImpliesOp"; break;
- case 191: s = "invalid AndOp"; break;
- case 192: s = "invalid OrOp"; break;
- case 193: s = "invalid RelOp"; break;
- case 194: s = "invalid AddOp"; break;
- case 195: s = "invalid UnaryExpression"; break;
- case 196: s = "invalid UnaryExpression"; break;
- case 197: s = "invalid MulOp"; break;
- case 198: s = "invalid NegOp"; break;
- case 199: s = "invalid EndlessExpression"; break;
- case 200: s = "invalid Suffix"; break;
- case 201: s = "invalid Suffix"; break;
+ case 185: s = "this symbol not expected in LoopSpec"; break;
+ case 186: s = "this symbol not expected in LoopSpec"; break;
+ case 187: s = "this symbol not expected in Invariant"; break;
+ case 188: s = "invalid BareGuard"; break;
+ case 189: s = "invalid AttributeArg"; break;
+ case 190: s = "invalid CalcOp"; break;
+ case 191: s = "invalid EquivOp"; break;
+ case 192: s = "invalid ImpliesOp"; break;
+ case 193: s = "invalid AndOp"; break;
+ case 194: s = "invalid OrOp"; break;
+ case 195: s = "invalid RelOp"; break;
+ case 196: s = "invalid AddOp"; break;
+ case 197: s = "invalid UnaryExpression"; break;
+ case 198: s = "invalid UnaryExpression"; break;
+ case 199: s = "invalid MulOp"; break;
+ case 200: s = "invalid NegOp"; break;
+ case 201: s = "invalid EndlessExpression"; break;
case 202: s = "invalid Suffix"; break;
- case 203: s = "invalid DisplayExpr"; break;
- case 204: s = "invalid MultiSetExpr"; break;
- case 205: s = "invalid ConstAtomExpression"; break;
- case 206: s = "invalid QSep"; break;
- case 207: s = "invalid QuantifierGuts"; break;
- case 208: s = "invalid LetExpr"; break;
- case 209: s = "invalid Forall"; break;
- case 210: s = "invalid Exists"; break;
+ case 203: s = "invalid Suffix"; break;
+ case 204: s = "invalid Suffix"; break;
+ case 205: s = "invalid DisplayExpr"; break;
+ case 206: s = "invalid MultiSetExpr"; break;
+ case 207: s = "invalid ConstAtomExpression"; break;
+ case 208: s = "invalid QSep"; break;
+ case 209: s = "invalid QuantifierGuts"; break;
+ case 210: s = "invalid LetExpr"; break;
+ case 211: s = "invalid Forall"; break;
+ case 212: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
@@ -3530,6 +3548,12 @@ public class Errors { count++;
}
+ public void Warning(IToken/*!*/ tok, string/*!*/ msg) { // warnings
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
+ Warning(tok.filename, tok.line, tok.col, msg);
+ }
+
public virtual void Warning(string filename, int line, int col, string msg) {
Contract.Requires(msg != null);
errorStream.WriteLine(warningMsgFormat, filename, line, col, msg);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 1ed04767..dbb53243 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -629,16 +629,17 @@ namespace Microsoft.Dafny { Indent(indent);
wr.Write("}");
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
- wr.Write("parallel (");
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
+ wr.Write("forall");
if (s.BoundVars.Count != 0) {
+ wr.Write(" ");
PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range);
}
if (s.Ens.Count == 0) {
- wr.Write(") ");
+ wr.Write(" ");
} else {
- wr.WriteLine(")");
+ wr.WriteLine();
PrintSpec("ensures", s.Ens, indent + IndentAmount);
Indent(indent);
}
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index a49b3b42..f92620fe 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -1313,9 +1313,9 @@ namespace Microsoft.Dafny });
} else if (s is CallStmt) {
reporter.Error(s.Tok, "cannot have call statement");
- } else if (s is ParallelStmt) {
- if (((ParallelStmt)s).Kind == ParallelStmt.ParBodyKind.Assign) // allow Proof and Call (as neither touch any existing state)
- reporter.Error(s.Tok, "cannot have parallel statement");
+ } else if (s is ForallStmt) {
+ if (((ForallStmt)s).Kind == ForallStmt.ParBodyKind.Assign) // allow Proof and Call (as neither touch any existing state)
+ reporter.Error(s.Tok, "cannot have forall statement");
} else {
if (s is WhileStmt || s is AlternativeLoopStmt) {
loopLevels++;
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index bc8b6c27..0250b2a3 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1625,14 +1625,14 @@ namespace Microsoft.Dafny return TailRecursionStatus.NotTailRecursive;
}
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
if (status != TailRecursionStatus.CanBeFollowedByAnything) {
if (status == TailRecursionStatus.NotTailRecursive) {
// an error has already been reported
} else if (reportErrors) {
- Error(tailCall.Tok, "a recursive call inside a parallel statement is not a tail call");
+ Error(tailCall.Tok, "a recursive call inside a forall statement is not a tail call");
}
return TailRecursionStatus.NotTailRecursive;
}
@@ -1840,8 +1840,8 @@ namespace Microsoft.Dafny CheckEqualityTypes(alt.Guard);
alt.Body.Iter(CheckEqualityTypes_Stmt);
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
CheckEqualityTypes(s.Range);
CheckEqualityTypes_Stmt(s.Body);
} else if (stmt is MatchStmt) {
@@ -2065,8 +2065,8 @@ namespace Microsoft.Dafny CheckTypeInference(alt.Guard);
alt.Body.Iter(CheckTypeInference);
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } 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"));
@@ -3610,7 +3610,7 @@ namespace Microsoft.Dafny Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
if (!slhs.SelectOne) {
- Error(stmt, "cannot assign to a range of array elements (try the 'parallel' statement)");
+ Error(stmt, "cannot assign to a range of array elements (try the 'forall' statement)");
}
}
@@ -3770,8 +3770,8 @@ namespace Microsoft.Dafny // any type is fine
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
int prevErrorCount = ErrorCount;
scope.PushMarker();
@@ -3784,7 +3784,7 @@ namespace Microsoft.Dafny ResolveExpression(s.Range, true, codeContext);
Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(s.Range.Type, Type.Bool)) {
- Error(stmt, "range restriction in parallel statement must be of type bool (instead got {0})", s.Range.Type);
+ Error(stmt, "range restriction in forall statement must be of type bool (instead got {0})", s.Range.Type);
}
foreach (var ens in s.Ens) {
ResolveExpression(ens.E, true, codeContext);
@@ -3807,7 +3807,7 @@ namespace Microsoft.Dafny }
s.IsGhost = bodyMustBeSpecOnly;
- // clear the labels for the duration of checking the body, because break statements are not allowed to leave a parallel statement
+ // clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement
var prevLblStmts = labeledStatements;
var prevLoopStack = loopStack;
labeledStatements = new Scope<Statement>();
@@ -3821,33 +3821,33 @@ namespace Microsoft.Dafny // determine the Kind and run some additional checks on the body
if (s.Ens.Count != 0) {
// The only supported kind with ensures clauses is Proof.
- s.Kind = ParallelStmt.ParBodyKind.Proof;
+ s.Kind = ForallStmt.ParBodyKind.Proof;
} else {
// There are three special cases:
- // * Assign, which is the only kind of the parallel statement that allows a heap update.
+ // * Assign, which is the only kind of the forall statement that allows a heap update.
// * Call, which is a single call statement with no side effects or output parameters.
// * A single calc statement, which is a special case of Proof where the postcondition can be inferred.
- // The effect of Assign and the postcondition of Call will be seen outside the parallel
+ // The effect of Assign and the postcondition of Call will be seen outside the forall
// statement.
Statement s0 = s.S0;
if (s0 is AssignStmt) {
- s.Kind = ParallelStmt.ParBodyKind.Assign;
+ s.Kind = ForallStmt.ParBodyKind.Assign;
} else if (s0 is CallStmt) {
- s.Kind = ParallelStmt.ParBodyKind.Call;
+ s.Kind = ForallStmt.ParBodyKind.Call;
} else if (s0 is CalcStmt) {
- s.Kind = ParallelStmt.ParBodyKind.Proof;
+ s.Kind = ForallStmt.ParBodyKind.Proof;
// add the conclusion of the calc as a free postcondition
s.Ens.Add(new MaybeFreeExpression(((CalcStmt)s0).Result, true));
} else {
- s.Kind = ParallelStmt.ParBodyKind.Proof;
+ s.Kind = ForallStmt.ParBodyKind.Proof;
if (s.Body is BlockStmt && ((BlockStmt)s.Body).Body.Count == 0) {
// an empty statement, so don't produce any warning
} else {
- Warning(s.Tok, "the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause");
+ Warning(s.Tok, "the conclusion of the body of this forall statement will not be known outside the forall statement; consider using an 'ensures' clause");
}
}
}
- CheckParallelBodyRestrictions(s.Body, s.Kind);
+ CheckForallStatementBodyRestrictions(s.Body, s.Kind);
}
} else if (stmt is CalcStmt) {
@@ -3881,7 +3881,7 @@ namespace Microsoft.Dafny e0 = e1;
}
- // clear the labels for the duration of checking the hints, because break statements are not allowed to leave a parallel statement
+ // clear the labels for the duration of checking the hints, because break statements are not allowed to leave a forall statement
var prevLblStmts = labeledStatements;
var prevLoopStack = loopStack;
labeledStatements = new Scope<Statement>();
@@ -4016,7 +4016,7 @@ namespace Microsoft.Dafny 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 'parallel' statement)");
+ Error(lhs, "cannot assign to a range of array elements (try the 'forall' statement)");
}
}
// Resolve RHSs
@@ -4385,47 +4385,47 @@ namespace Microsoft.Dafny }
/// <summary>
- /// This method performs some additional checks on the body "stmt" of a parallel statement of kind "kind".
+ /// This method performs some additional checks on the body "stmt" of a forall statement of kind "kind".
/// </summary>
- public void CheckParallelBodyRestrictions(Statement stmt, ParallelStmt.ParBodyKind kind) {
+ public void CheckForallStatementBodyRestrictions(Statement stmt, ForallStmt.ParBodyKind kind) {
Contract.Requires(stmt != null);
if (stmt is PredicateStmt) {
// cool
} else if (stmt is PrintStmt) {
- Error(stmt, "print statement is not allowed inside a parallel statement");
+ Error(stmt, "print statement is not allowed inside a forall statement");
} else if (stmt is BreakStmt) {
- // this case is checked already in the first pass through the parallel body, by doing so from an empty set of labeled statements and resetting the loop-stack
+ // this case is checked already in the first pass through the forall-statement body, by doing so from an empty set of labeled statements and resetting the loop-stack
} else if (stmt is ReturnStmt) {
- Error(stmt, "return statement is not allowed inside a parallel statement");
+ Error(stmt, "return statement is not allowed inside a forall statement");
} else if (stmt is YieldStmt) {
- Error(stmt, "yield statement is not allowed inside a parallel statement");
+ Error(stmt, "yield statement is not allowed inside a forall statement");
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
foreach (var lhs in s.Lhss) {
- CheckParallelBodyLhs(s.Tok, lhs.Resolved, kind);
+ CheckForallStatementBodyLhs(s.Tok, lhs.Resolved, kind);
}
} else if (stmt is ConcreteSyntaxStatement) {
var s = (ConcreteSyntaxStatement)stmt;
foreach (var ss in s.ResolvedStatements) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
} else if (stmt is AssignStmt) {
var s = (AssignStmt)stmt;
- CheckParallelBodyLhs(s.Tok, s.Lhs.Resolved, kind);
+ CheckForallStatementBodyLhs(s.Tok, s.Lhs.Resolved, kind);
var rhs = s.Rhs; // ExprRhs and HavocRhs are fine, but TypeRhs is not
if (rhs is TypeRhs) {
- if (kind == ParallelStmt.ParBodyKind.Assign) {
- Error(rhs.Tok, "new allocation not supported in parallel statements");
+ if (kind == ForallStmt.ParBodyKind.Assign) {
+ Error(rhs.Tok, "new allocation not supported in forall statements");
} else {
var t = (TypeRhs)rhs;
if (t.InitCall != null) {
- CheckParallelBodyRestrictions(t.InitCall, kind);
+ CheckForallStatementBodyRestrictions(t.InitCall, kind);
}
}
} else if (rhs is ExprRhs) {
var r = ((ExprRhs)rhs).Expr.Resolved;
- if (kind == ParallelStmt.ParBodyKind.Assign && r is UnaryExpr && ((UnaryExpr)r).Op == UnaryExpr.Opcode.SetChoose) {
- Error(r, "set choose operator not supported inside the enclosing parallel statement");
+ if (kind == ForallStmt.ParBodyKind.Assign && r is UnaryExpr && ((UnaryExpr)r).Op == UnaryExpr.Opcode.SetChoose) {
+ Error(r, "set choose operator not supported inside the enclosing forall statement");
}
}
} else if (stmt is VarDecl) {
@@ -4436,64 +4436,64 @@ namespace Microsoft.Dafny var idExpr = lhs as IdentifierExpr;
if (idExpr != null) {
if (scope.ContainsDecl(idExpr.Var)) {
- Error(stmt, "body of parallel statement is attempting to update a variable declared outside the parallel statement");
+ Error(stmt, "body of forall statement is attempting to update a variable declared outside the forall statement");
}
} else {
- Error(stmt, "the body of the enclosing parallel statement is not allowed to update heap locations");
+ Error(stmt, "the body of the enclosing forall statement is not allowed to update heap locations");
}
}
if (!s.Method.IsGhost) {
- // The reason for this restriction is that the compiler is going to omit the parallel statement altogether--it has
+ // The reason for this restriction is that the compiler is going to omit the forall statement altogether--it has
// no effect. However, print effects are not documented, so to make sure that the compiler does not omit a call to
// a method that prints something, all calls to non-ghost methods are disallowed. (Note, if this restriction
// is somehow lifted in the future, then it is still necessary to enforce s.Method.Mod.Expressions.Count != 0 for
// calls to non-ghost methods.)
- Error(s, "the body of the enclosing parallel statement is not allowed to call non-ghost methods");
+ Error(s, "the body of the enclosing forall statement is not allowed to call non-ghost methods");
}
} else if (stmt is BlockStmt) {
var s = (BlockStmt)stmt;
scope.PushMarker();
foreach (var ss in s.Body) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
scope.PopMarker();
} else if (stmt is IfStmt) {
var s = (IfStmt)stmt;
- CheckParallelBodyRestrictions(s.Thn, kind);
+ CheckForallStatementBodyRestrictions(s.Thn, kind);
if (s.Els != null) {
- CheckParallelBodyRestrictions(s.Els, kind);
+ CheckForallStatementBodyRestrictions(s.Els, kind);
}
} else if (stmt is AlternativeStmt) {
var s = (AlternativeStmt)stmt;
foreach (var alt in s.Alternatives) {
foreach (var ss in alt.Body) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
}
} else if (stmt is WhileStmt) {
WhileStmt s = (WhileStmt)stmt;
- CheckParallelBodyRestrictions(s.Body, kind);
+ CheckForallStatementBodyRestrictions(s.Body, kind);
} else if (stmt is AlternativeLoopStmt) {
var s = (AlternativeLoopStmt)stmt;
foreach (var alt in s.Alternatives) {
foreach (var ss in alt.Body) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
switch (s.Kind) {
- case ParallelStmt.ParBodyKind.Assign:
- Error(stmt, "a parallel statement with heap updates is not allowed inside the body of another parallel statement");
+ case ForallStmt.ParBodyKind.Assign:
+ Error(stmt, "a forall statement with heap updates is not allowed inside the body of another forall statement");
break;
- case ParallelStmt.ParBodyKind.Call:
- case ParallelStmt.ParBodyKind.Proof:
+ case ForallStmt.ParBodyKind.Call:
+ case ForallStmt.ParBodyKind.Proof:
// these are fine, since they don't update any non-local state
break;
default:
@@ -4508,7 +4508,7 @@ namespace Microsoft.Dafny var s = (MatchStmt)stmt;
foreach (var kase in s.Cases) {
foreach (var ss in kase.Body) {
- CheckParallelBodyRestrictions(ss, kind);
+ CheckForallStatementBodyRestrictions(ss, kind);
}
}
@@ -4517,14 +4517,14 @@ namespace Microsoft.Dafny }
}
- void CheckParallelBodyLhs(IToken tok, Expression lhs, ParallelStmt.ParBodyKind kind) {
+ void CheckForallStatementBodyLhs(IToken tok, Expression lhs, ForallStmt.ParBodyKind kind) {
var idExpr = lhs as IdentifierExpr;
if (idExpr != null) {
if (scope.ContainsDecl(idExpr.Var)) {
- Error(tok, "body of parallel statement is attempting to update a variable declared outside the parallel statement");
+ Error(tok, "body of forall statement is attempting to update a variable declared outside the forall statement");
}
- } else if (kind != ParallelStmt.ParBodyKind.Assign) {
- Error(tok, "the body of the enclosing parallel statement is not allowed to update heap locations");
+ } else if (kind != ForallStmt.ParBodyKind.Assign) {
+ Error(tok, "the body of the enclosing forall statement is not allowed to update heap locations");
}
}
@@ -4599,14 +4599,14 @@ namespace Microsoft.Dafny }
}
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
switch (s.Kind) {
- case ParallelStmt.ParBodyKind.Assign:
- Error(stmt, "a parallel statement with heap updates is not allowed inside a hint");
+ case ForallStmt.ParBodyKind.Assign:
+ Error(stmt, "a forall statement with heap updates is not allowed inside a hint");
break;
- case ParallelStmt.ParBodyKind.Call:
- case ParallelStmt.ParBodyKind.Proof:
+ case ForallStmt.ParBodyKind.Call:
+ case ForallStmt.ParBodyKind.Proof:
// these are fine, since they don't update any non-local state
break;
default:
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index ca20b113..9802a282 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -542,17 +542,17 @@ public class Scanner { case "match": t.kind = 77; break;
case "assert": t.kind = 78; break;
case "print": t.kind = 79; break;
- case "parallel": t.kind = 80; break;
- case "calc": t.kind = 81; break;
- case "in": t.kind = 97; break;
- case "false": t.kind = 104; break;
- case "true": t.kind = 105; break;
- case "null": t.kind = 106; break;
- case "this": t.kind = 107; break;
- case "fresh": t.kind = 108; break;
- case "old": t.kind = 109; break;
- case "then": t.kind = 110; break;
- case "forall": t.kind = 112; break;
+ case "forall": t.kind = 80; break;
+ case "parallel": t.kind = 81; break;
+ case "calc": t.kind = 82; break;
+ case "in": t.kind = 98; break;
+ case "false": t.kind = 105; break;
+ case "true": t.kind = 106; break;
+ case "null": t.kind = 107; break;
+ case "this": t.kind = 108; break;
+ case "fresh": t.kind = 109; break;
+ case "old": t.kind = 110; break;
+ case "then": t.kind = 111; break;
case "exists": t.kind = 114; break;
default: break;
}
@@ -695,49 +695,49 @@ public class Scanner { case 33:
{t.kind = 74; break;}
case 34:
- {t.kind = 83; break;}
- case 35:
{t.kind = 84; break;}
- case 36:
+ case 35:
{t.kind = 85; break;}
- case 37:
+ case 36:
{t.kind = 86; break;}
- case 38:
+ case 37:
{t.kind = 87; break;}
+ case 38:
+ {t.kind = 88; break;}
case 39:
if (ch == '>') {AddCh(); goto case 40;}
else {goto case 0;}
case 40:
- {t.kind = 88; break;}
- case 41:
{t.kind = 89; break;}
- case 42:
+ case 41:
{t.kind = 90; break;}
- case 43:
+ case 42:
{t.kind = 91; break;}
+ case 43:
+ {t.kind = 92; break;}
case 44:
if (ch == '&') {AddCh(); goto case 45;}
else {goto case 0;}
case 45:
- {t.kind = 92; break;}
- case 46:
{t.kind = 93; break;}
- case 47:
+ case 46:
{t.kind = 94; break;}
- case 48:
+ case 47:
{t.kind = 95; break;}
- case 49:
+ case 48:
{t.kind = 96; break;}
+ case 49:
+ {t.kind = 97; break;}
case 50:
- {t.kind = 99; break;}
- case 51:
{t.kind = 100; break;}
- case 52:
+ case 51:
{t.kind = 101; break;}
- case 53:
+ case 52:
{t.kind = 102; break;}
- case 54:
+ case 53:
{t.kind = 103; break;}
+ case 54:
+ {t.kind = 104; break;}
case 55:
{t.kind = 113; break;}
case 56:
@@ -753,10 +753,10 @@ public class Scanner { else if (ch == ':') {AddCh(); goto case 57;}
else {t.kind = 5; break;}
case 60:
- recEnd = pos; recKind = 98;
+ recEnd = pos; recKind = 99;
if (ch == 'i') {AddCh(); goto case 12;}
else if (ch == '=') {AddCh(); goto case 35;}
- else {t.kind = 98; break;}
+ else {t.kind = 99; break;}
case 61:
recEnd = pos; recKind = 14;
if (ch == '=') {AddCh(); goto case 66;}
@@ -783,13 +783,13 @@ public class Scanner { if (ch == '>') {AddCh(); goto case 42;}
else {t.kind = 29; break;}
case 67:
- recEnd = pos; recKind = 111;
+ recEnd = pos; recKind = 112;
if (ch == '.') {AddCh(); goto case 26;}
- else {t.kind = 111; break;}
+ else {t.kind = 112; break;}
case 68:
- recEnd = pos; recKind = 82;
+ recEnd = pos; recKind = 83;
if (ch == '=') {AddCh(); goto case 39;}
- else {t.kind = 82; break;}
+ else {t.kind = 83; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 9252cde5..0fef4319 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1957,10 +1957,10 @@ namespace Microsoft.Dafny { // Also, let Pre be the precondition and VF be the decreases clause.
// Then, insert into the method body what amounts to:
// assume case-analysis-on-parameter[[ y' ]];
- // parallel (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) {
+ // forall (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) {
// this'.M(x, y');
// }
- // Generate bound variables for the parallel statement, and a substitution for the Pre and VF
+ // Generate bound variables for the forall statement, and a substitution for the Pre and VF
// assume case-analysis-on-parameter[[ y' ]];
foreach (var inFormal in m.Ins) {
@@ -2047,14 +2047,14 @@ namespace Microsoft.Dafny { return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, null, null, false, true);
};
-#if VERIFY_CORRECTNESS_OF_TRANSLATION_PARALLEL_RANGE
+#if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
- TrParallelCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
+ TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
#else
- TrParallelCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
+ TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
#endif
}
}
@@ -4779,10 +4779,10 @@ 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 ParallelStmt) {
- AddComment(builder, stmt, "parallel statement");
- var s = (ParallelStmt)stmt;
- if (s.Kind == ParallelStmt.ParBodyKind.Assign) {
+ } else if (stmt is ForallStmt) {
+ AddComment(builder, stmt, "forall statement");
+ var s = (ForallStmt)stmt;
+ if (s.Kind == ForallStmt.ParBodyKind.Assign) {
Contract.Assert(s.Ens.Count == 0);
if (s.BoundVars.Count == 0) {
TrStmt(s.Body, builder, locals, etran);
@@ -4790,13 +4790,13 @@ namespace Microsoft.Dafny { var s0 = (AssignStmt)s.S0;
var definedness = new Bpl.StmtListBuilder();
var updater = new Bpl.StmtListBuilder();
- TrParallelAssign(s, s0, definedness, updater, locals, etran);
+ TrForallAssign(s, s0, definedness, updater, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, updater.Collect(s.Tok)));
builder.Add(CaptureState(stmt.Tok));
}
- } else if (s.Kind == ParallelStmt.ParBodyKind.Call) {
+ } else if (s.Kind == ForallStmt.ParBodyKind.Call) {
Contract.Assert(s.Ens.Count == 0);
if (s.BoundVars.Count == 0) {
TrStmt(s.Body, builder, locals, etran);
@@ -4804,16 +4804,16 @@ namespace Microsoft.Dafny { var s0 = (CallStmt)s.S0;
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
- TrParallelCall(s.Tok, s.BoundVars, s.Range, null, s0, definedness, exporter, locals, etran);
+ TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s0, definedness, exporter, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok)));
builder.Add(CaptureState(stmt.Tok));
}
- } else if (s.Kind == ParallelStmt.ParBodyKind.Proof) {
+ } else if (s.Kind == ForallStmt.ParBodyKind.Proof) {
var definedness = new Bpl.StmtListBuilder();
var exporter = new Bpl.StmtListBuilder();
- TrParallelProof(s, definedness, exporter, locals, etran);
+ TrForallProof(s, definedness, exporter, locals, etran);
// All done, so put the two pieces together
builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok)));
builder.Add(CaptureState(stmt.Tok));
@@ -5101,10 +5101,10 @@ namespace Microsoft.Dafny { return null; // TODO: this can be improved
}
- void TrParallelAssign(ParallelStmt s, AssignStmt s0,
+ void TrForallAssign(ForallStmt s, AssignStmt s0,
Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder updater, Bpl.VariableSeq locals, ExpressionTranslator etran) {
// The statement:
- // parallel (x,y | Range(x,y)) {
+ // forall (x,y | Range(x,y)) {
// (a) E(x,y) . f := G(x,y);
// (b) A(x,y) [ I0(x,y), I1(x,y), ... ] := G(x,y);
// }
@@ -5204,7 +5204,7 @@ namespace Microsoft.Dafny { GetObjFieldDetails(lhsPrime, etran, out objPrime, out FPrime);
definedness.Add(Assert(s0.Tok,
Bpl.Expr.Or(Bpl.Expr.Neq(obj, objPrime), Bpl.Expr.Neq(F, FPrime)),
- "left-hand sides for different parallel-statement bound variables may refer to the same location"));
+ "left-hand sides for different forall-statement bound variables may refer to the same location"));
definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
@@ -5266,7 +5266,7 @@ namespace Microsoft.Dafny { delegate Bpl.Expr ExpressionConverter(Dictionary<IVariable, Expression> substMap, ExpressionTranslator etran);
- void TrParallelCall(IToken tok, List<BoundVar> boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0,
+ void TrForallStmtCall(IToken tok, List<BoundVar> boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0,
Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
Contract.Requires(tok != null);
Contract.Requires(boundVars != null);
@@ -5279,7 +5279,7 @@ namespace Microsoft.Dafny { Contract.Requires(etran != null);
// Translate:
- // parallel (x,y | Range(x,y)) {
+ // forall (x,y | Range(x,y)) {
// E(x,y) . M( Args(x,y) );
// }
// as:
@@ -5327,7 +5327,7 @@ namespace Microsoft.Dafny { // Now for the other branch, where the postcondition of the call is exported.
{
- var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$initHeapParallelStmt#" + otherTmpVarCount, predef.HeapType));
+ var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$initHeapForallStmt#" + otherTmpVarCount, predef.HeapType));
otherTmpVarCount++;
locals.Add(initHeapVar);
var initHeap = new Bpl.IdentifierExpr(tok, initHeapVar);
@@ -5348,7 +5348,7 @@ namespace Microsoft.Dafny { RecordNewObjectsIn_New(tok, iter, initHeap, heapIdExpr, exporter, locals, etran);
}
} else {
- // As an optimization, create the illusion that the $Heap is unchanged by the parallel body.
+ // As an optimization, create the illusion that the $Heap is unchanged by the forall-statement body.
exporter.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(etran.Tick())));
}
@@ -5410,9 +5410,9 @@ namespace Microsoft.Dafny { builder.Add(cmd);
}
- void TrParallelProof(ParallelStmt s, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
+ void TrForallProof(ForallStmt s, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) {
// Translate:
- // parallel (x,y | Range(x,y))
+ // forall (x,y | Range(x,y))
// ensures Post(x,y);
// {
// Body;
@@ -5457,7 +5457,7 @@ namespace Microsoft.Dafny { bool splitHappened; // we actually don't care
foreach (var split in TrSplitExpr(ens.E, etran, out splitHappened)) {
if (split.IsChecked) {
- definedness.Add(Assert(split.E.tok, split.E, "possible violation of postcondition of parallel statement"));
+ definedness.Add(Assert(split.E.tok, split.E, "possible violation of postcondition of forall statement"));
}
}
}
@@ -5467,7 +5467,7 @@ namespace Microsoft.Dafny { // Now for the other branch, where the ensures clauses are exported.
- var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$initHeapParallelStmt#" + otherTmpVarCount, predef.HeapType));
+ var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$initHeapForallStmt#" + otherTmpVarCount, predef.HeapType));
otherTmpVarCount++;
locals.Add(initHeapVar);
var initHeap = new Bpl.IdentifierExpr(s.Tok, initHeapVar);
@@ -5483,7 +5483,7 @@ namespace Microsoft.Dafny { }
}
} else {
- // As an optimization, create the illusion that the $Heap is unchanged by the parallel body.
+ // As an optimization, create the illusion that the $Heap is unchanged by the forall-statement body.
exporter.Add(new Bpl.HavocCmd(s.Tok, new Bpl.IdentifierExprSeq(etran.Tick())));
}
@@ -6509,7 +6509,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Requires(lhs != null);
Contract.Requires(!(lhs is ConcreteSyntaxExpression));
- Contract.Requires(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne)); // these were once allowed, but their functionality is now provided by 'parallel' statements
+ Contract.Requires(!(lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne)); // these were once allowed, but their functionality is now provided by 'forall' statements
Contract.Requires(rhs != null);
Contract.Requires(builder != null);
Contract.Requires(cce.NonNullElements(locals));
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index b8e8805a..6a612cbd 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -282,8 +282,8 @@ namespace DafnyLanguage } else if (stmt is VarDecl) {
var s = (VarDecl)stmt;
IdRegion.Add(regions, s.Tok, s, true, module);
- } else if (stmt is ParallelStmt) {
- var s = (ParallelStmt)stmt;
+ } else if (stmt is ForallStmt) {
+ var s = (ForallStmt)stmt;
s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index a8f63232..45f1c36c 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -271,7 +271,6 @@ namespace DafnyLanguage case "object":
case "old":
case "opened":
- case "parallel":
case "predicate":
case "print":
case "reads":
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy index 612b96ba..53d82207 100644 --- a/Test/VSI-Benchmarks/b5.dfy +++ b/Test/VSI-Benchmarks/b5.dfy @@ -57,12 +57,12 @@ class Queue<T> { tail.next := n;
tail := n;
- parallel (m | m in spine) {
+ forall m | m in spine {
m.tailContents := m.tailContents + [t];
}
contents := head.tailContents;
- parallel (m | m in spine) {
+ forall m | m in spine {
m.footprint := m.footprint + n.footprint;
}
footprint := footprint + n.footprint;
diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy index d3cecc28..06692314 100644 --- a/Test/dafny0/CoPrefix.dfy +++ b/Test/dafny0/CoPrefix.dfy @@ -41,7 +41,7 @@ comethod {:induction false} Theorem0() ghost method Theorem0_Manual()
ensures atmost(zeros(), ones());
{
- parallel (k: nat) {
+ forall k: nat {
Theorem0_Lemma(k);
}
}
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index 43ef4e69..e0c58867 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -208,7 +208,7 @@ iterator DoleOutReferences(u: Cell) yields (r: Cell, c: Cell) assert c in _new; // as is checked here as well
assert r.data == 12; // error: it may have changed
} else {
- parallel (z | z in myCells) {
+ forall z | z in myCells {
z.data := z.data + 1; // we're allowed to modify these, because they are all in _new
}
}
diff --git a/Test/dafny0/LetExpr.dfy b/Test/dafny0/LetExpr.dfy index 11bf4fbe..cd712b7d 100644 --- a/Test/dafny0/LetExpr.dfy +++ b/Test/dafny0/LetExpr.dfy @@ -38,7 +38,7 @@ method M3(a: array<int>) returns (r: int) assert Fib(1000) == 1000; // does it still know this?
- parallel (i | 0 <= i < a.Length) ensures true; {
+ forall i | 0 <= i < a.Length ensures true; {
var j := i+1;
assert j < a.Length ==> a[i] == a[j];
}
diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index ac11c1eb..37004441 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -19,23 +19,23 @@ method ParallelStatement_Resolve( requires a != null && null !in spine;
modifies a, spine;
{
- parallel (i: int | 0 <= i < a.Length && i % 2 == 0) {
+ forall (i: int | 0 <= i < a.Length && i % 2 == 0) {
a[i] := a[(i + 1) % a.Length] + 3;
}
- parallel (o | o in spine) {
+ forall (o | o in spine) {
o.st := o.st + Repr;
}
- parallel (x, y | x in S && 0 <= y+x < 100) {
+ forall (x, y | x in S && 0 <= y+x < 100) {
Lemma(clx, x, y); // error: precondition does not hold (clx may be null)
}
- parallel (x, y | x in S && 0 <= y+x < 100) {
+ forall (x, y | x in S && 0 <= y+x < 100) {
cly.CLemma(x + y); // error: receiver might be null
}
- parallel (p | 0 <= p)
+ forall (p | 0 <= p)
ensures F(p) <= Sum(p) + p - 1; // error (no connection is known between F and Sum)
{
assert 0 <= G(p);
@@ -73,7 +73,7 @@ method M0(S: set<C>) ensures forall o :: o in S ==> o.data == 85;
ensures forall o :: o != null && o !in S ==> o.data == old(o.data);
{
- parallel (s | s in S) {
+ forall (s | s in S) {
s.data := 85;
}
}
@@ -81,18 +81,18 @@ method M0(S: set<C>) method M1(S: set<C>, x: C)
requires null !in S && x in S;
{
- parallel (s | s in S)
+ forall (s | s in S)
ensures s.data < 100;
{
assume s.data == 85;
}
if (*) {
- assert x.data == 85; // error (cannot be inferred from parallel ensures clause)
+ assert x.data == 85; // error (cannot be inferred from forall ensures clause)
} else {
assert x.data < 120;
}
- parallel (s | s in S)
+ forall (s | s in S)
ensures s.data < 70; // error
{
assume s.data == 85;
@@ -104,10 +104,10 @@ method M2() returns (a: array<int>) ensures forall i,j :: 0 <= i < a.Length/2 <= j < a.Length ==> a[i] < a[j];
{
a := new int[250];
- parallel (i: nat | i < 125) {
+ forall (i: nat | i < 125) {
a[i] := 423;
}
- parallel (i | 125 <= i < 250) {
+ forall (i | 125 <= i < 250) {
a[i] := 300 + i;
}
}
@@ -115,7 +115,7 @@ method M2() returns (a: array<int>) method M4(S: set<C>, k: int)
modifies S;
{
- parallel (s | s in S && s != null) {
+ forall (s | s in S && s != null) {
s.n := k; // error: k might be negative
}
}
@@ -124,25 +124,25 @@ method M5() {
if {
case true =>
- parallel (x | 0 <= x < 100) {
+ forall (x | 0 <= x < 100) {
PowerLemma(x, x);
}
assert Pred(34, 34);
case true =>
- parallel (x,y | 0 <= x < 100 && y == x+1) {
+ forall (x,y | 0 <= x < 100 && y == x+1) {
PowerLemma(x, y);
}
assert Pred(34, 35);
case true =>
- parallel (x,y | 0 <= x < y < 100) {
+ forall (x,y | 0 <= x < y < 100) {
PowerLemma(x, y);
}
assert Pred(34, 35);
case true =>
- parallel (x | x in set k | 0 <= k < 100) {
+ forall (x | x in set k | 0 <= k < 100) {
PowerLemma(x, x);
}
assert Pred(34, 34);
@@ -152,17 +152,17 @@ method M5() method Main()
{
var a := new int[180];
- parallel (i | 0 <= i < 180) {
+ forall (i | 0 <= i < 180) {
a[i] := 2*i + 100;
}
var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];
- parallel (i | 0 <= i < |sq|) {
+ forall (i | 0 <= i < |sq|) {
a[20+i] := sq[i];
}
- parallel (t | t in sq) {
+ forall (t | t in sq) {
a[t] := 1000;
}
- parallel (t,u | t in sq && t < 4 && 10 <= u < 10+t) {
+ forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) {
a[u] := 6000 + t;
}
var k := 0;
@@ -178,11 +178,11 @@ method DuplicateUpdate() { var a := new int[180];
var sq := [0, 0, 0, 2, 2, 2, 5, 5, 5];
if (*) {
- parallel (t,u | t in sq && 10 <= u < 10+t) {
+ forall (t,u | t in sq && 10 <= u < 10+t) {
a[u] := 6000 + t; // error: a[10] (and a[11]) are assigned more than once
}
} else {
- parallel (t,u | t in sq && t < 4 && 10 <= u < 10+t) {
+ forall (t,u | t in sq && t < 4 && 10 <= u < 10+t) {
a[u] := 6000 + t; // with the 't < 4' conjunct in the line above, this is fine
}
}
@@ -193,8 +193,8 @@ ghost method DontDoMuch(x: int) }
method OmittedRange() {
- parallel (x) { }
- parallel (x) {
+ forall (x) { }
+ forall (x) {
DontDoMuch(x);
}
}
@@ -210,7 +210,7 @@ ghost static method TwoState0(y: int) }
method TwoState_Main0() {
- parallel (x) { TwoState0(x); }
+ forall (x) { TwoState0(x); }
assert false; // error: this location is indeed reachable (if the translation before it is sound)
}
@@ -222,7 +222,7 @@ ghost static method TwoState1(y: int) }
method TwoState_Main1() {
- parallel (x) { TwoState1(x); }
+ forall (x) { TwoState1(x); }
assert false; // error: this location is indeed reachable (if the translation before it is sound)
}
@@ -231,7 +231,7 @@ method X_Legit(c: TwoState_C) modifies c;
{
c.data := c.data + 1;
- parallel (x | c.data <= x)
+ forall (x | c.data <= x)
ensures old(c.data) < x; // note that the 'old' refers to the method's initial state
{
}
@@ -241,12 +241,12 @@ method X_Legit(c: TwoState_C) // ensures clause.
// However, there's an important difference in the translation, which is that the
// occurrence of 'fresh' here refers to the initial state of the TwoStateMain2
-// method, not the beginning of the 'parallel' statement.
-// Still, care needs to be taken in the translation to make sure that the parallel
+// method, not the beginning of the 'forall' statement.
+// Still, care needs to be taken in the translation to make sure that the forall
// statement's effect on the heap is not optimized away.
method TwoState_Main2()
{
- parallel (x: int)
+ forall (x: int)
ensures exists o: TwoState_C :: o != null && fresh(o);
{
TwoState0(x);
@@ -257,12 +257,12 @@ method TwoState_Main2() // At first glance, this looks like an inlined version of TwoState_Main0 above.
// However, there's an important difference in the translation, which is that the
// occurrence of 'fresh' here refers to the initial state of the TwoStateMain3
-// method, not the beginning of the 'parallel' statement.
-// Still, care needs to be taken in the translation to make sure that the parallel
+// method, not the beginning of the 'forall' statement.
+// Still, care needs to be taken in the translation to make sure that the forall
// statement's effect on the heap is not optimized away.
method TwoState_Main3()
{
- parallel (x: int)
+ forall (x: int)
ensures exists o: TwoState_C :: o != null && fresh(o);
{
var p := new TwoState_C;
@@ -270,7 +270,7 @@ method TwoState_Main3() assert false; // error: this location is indeed reachable (if the translation before it is sound)
}
-// ------- empty parallel statement -----------------------------------------
+// ------- empty forall statement -----------------------------------------
var emptyPar: int;
@@ -278,7 +278,7 @@ method Empty_Parallel0() modifies this;
ensures emptyPar == 8;
{
- parallel () {
+ forall () {
this.emptyPar := 8;
}
}
@@ -290,19 +290,19 @@ ghost method EmptyPar_Lemma(x: int) method Empty_Parallel1()
ensures EmptyPar_P(8);
{
- parallel () {
+ forall {
EmptyPar_Lemma(8);
}
}
method Empty_Parallel2()
{
- parallel ()
+ forall
ensures exists k :: EmptyPar_P(k);
{
var y := 8;
assume EmptyPar_P(y);
}
assert exists k :: EmptyPar_P(k); // yes
- assert EmptyPar_P(8); // error: the parallel statement's ensures clause does not promise this
+ assert EmptyPar_P(8); // error: the forall statement's ensures clause does not promise this
}
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index f260edb5..c740f88c 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -13,16 +13,16 @@ class C { method M0(IS: set<int>)
{
- parallel (i | 0 <= i < 20) {
+ forall (i | 0 <= i < 20) {
i := i + 1; // error: not allowed to assign to bound variable
}
var k := 0;
- parallel (i | 0 <= i < 20) {
- k := k + i; // error: not allowed to assign to local k, since k is not declared inside parallel block
+ forall (i | 0 <= i < 20) {
+ k := k + i; // error: not allowed to assign to local k, since k is not declared inside forall block
}
- parallel (i | 0 <= i < 20)
+ forall (i | 0 <= i < 20)
ensures true;
{
var x := i;
@@ -31,16 +31,16 @@ method M0(IS: set<int>) ghost var y;
var z;
- parallel (i | 0 <= i)
+ forall (i | 0 <= i)
ensures true;
{
var x := i;
x := x + 1;
- y := 18; // (this statement is not allowed, since y is declared outside the parallel, but that check happens only if the first resolution pass of the parallel statement passes, which it doesn't in this case because of the next line)
- z := 20; // error: assigning to a non-ghost variable inside a ghost parallel block
+ y := 18; // (this statement is not allowed, since y is declared outside the forall, but that check happens only if the first resolution pass of the forall statement passes, which it doesn't in this case because of the next line)
+ z := 20; // error: assigning to a non-ghost variable inside a ghost forall block
}
- parallel (i | 0 <= i)
+ forall (i | 0 <= i)
ensures true;
{
ghost var x := i;
@@ -48,15 +48,15 @@ method M0(IS: set<int>) }
var ia := new int[20];
- parallel (i | 0 <= i < 20) {
+ forall (i | 0 <= i < 20) {
ia[i] := choose IS; // error: set choose not allowed
}
var ca := new C[20];
- parallel (i | 0 <= i < 20) {
+ forall (i | 0 <= i < 20) {
ca[i] := new C; // error: new allocation not allowed
}
- parallel (i | 0 <= i < 20)
+ forall (i | 0 <= i < 20)
ensures true;
{
var c := new C; // allowed
@@ -69,27 +69,27 @@ method M0(IS: set<int>) }
method M1() {
- parallel (i | 0 <= i < 20) {
+ forall (i | 0 <= i < 20) {
assert i < 100;
if (i == 17) { break; } // error: nothing to break out of
}
- parallel (i | 0 <= i < 20) ensures true; {
- if (i == 8) { return; } // error: return not allowed inside parallel block
+ forall (i | 0 <= i < 20) ensures true; {
+ if (i == 8) { return; } // error: return not allowed inside forall block
}
var m := 0;
label OutsideLoop:
while (m < 20) {
- parallel (i | 0 <= i < 20) {
- if (i == 17) { break; } // error: not allowed to break out of loop that sits outside parallel
+ forall (i | 0 <= i < 20) {
+ if (i == 17) { break; } // error: not allowed to break out of loop that sits outside forall
if (i == 8) { break break; } // error: ditto (also: attempt to break too far)
if (i == 9) { break OutsideLoop; } // error: ditto
}
m := m + 1;
}
- parallel (i | 0 <= i < 20) {
+ forall (i | 0 <= i < 20) {
var j := 0;
while (j < i) {
if (j == 6) { break; } // fine
@@ -102,7 +102,7 @@ method M1() { method M2() {
var a := new int[100];
- parallel (x | 0 <= x < 100) {
- a[x] :| assume a[x] > 0; // error: not allowed to update heap location in a parallel statement with an assume
+ forall (x | 0 <= x < 100) {
+ a[x] :| assume a[x] > 0; // error: not allowed to update heap location in a forall statement with an assume
}
}
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index c55d6140..2f12fdd2 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -144,7 +144,7 @@ class Modifies { method F(s: set<Modifies>)
modifies s;
{
- parallel (m | m in s && m != null && 2 <= m.x) {
+ forall 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
- parallel (m | m in s && m == this) {
+ forall m | m in s && m == this {
m.x := m.x + 1;
}
if (s <= {this}) {
- parallel (m | m in s) {
+ forall (m | m in s) {
m.x := m.x + 1;
}
F(s);
}
- parallel (m | m in s) ensures true; { assert m == null || m.x < m.x + 10; }
- parallel (m | m != null && m in s) {
+ forall (m | m in s) ensures true; { assert m == null || m.x < m.x + 10; }
+ forall (m | m != null && m in s) {
m.x := m.x + 1; // error: may violate modifies clause
}
}
@@ -304,7 +304,7 @@ class SomeType requires null !in stack;
modifies stack;
{
- parallel (n | n in stack) {
+ forall n | n in stack {
n.x := 10;
}
}
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy index b6ef0d68..758f5f44 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;
- parallel (s | s in S) ensures true; { assert s == null || s.H() == 5; }
- parallel (s | s != null && s in S) {
+ forall s | s in S ensures true; { assert s == null || s.H() == 5; }
+ forall s | s != null && s in S {
s.x := 0;
}
diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy index 0edfab81..8396ec5c 100644 --- a/Test/dafny1/Queue.dfy +++ b/Test/dafny1/Queue.dfy @@ -85,12 +85,12 @@ class Queue<T> { tail.next := n;
tail := n;
- parallel (m | m in spine) {
+ forall m | m in spine {
m.tailContents := m.tailContents + [t];
}
contents := head.tailContents;
- parallel (m | m in spine) {
+ forall m | m in spine {
m.footprint := m.footprint + n.footprint;
}
footprint := footprint + n.footprint;
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 79803f35..bbfab50d 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -209,7 +209,7 @@ ghost method Window(xs: List, ys: List) }
}
-// In the following we use a combination of calc and parallel
+// In the following we use a combination of calc and forall
function ith<a>(xs: List, i: nat): a
requires i < length(xs);
@@ -253,7 +253,7 @@ ghost method lemma_extensionality(xs: List, ys: List) }
Cons(y, xrest);
{
- parallel (j: nat | j < length(xrest)) {
+ forall (j: nat | j < length(xrest)) {
calc {
ith(xrest, j);
ith(xs, j + 1);
diff --git a/Test/dafny3/InductionVsCoinduction.dfy b/Test/dafny3/InductionVsCoinduction.dfy index 26e57c7f..2f8c2a9e 100644 --- a/Test/dafny3/InductionVsCoinduction.dfy +++ b/Test/dafny3/InductionVsCoinduction.dfy @@ -75,7 +75,7 @@ ghost method {:induction false} SAppendIsAssociativeK(k:nat, a:Stream, b:Stream, ghost method SAppendIsAssociative(a:Stream, b:Stream, c:Stream)
ensures SAppend(SAppend(a, b), c) == SAppend(a, SAppend(b, c));
{
- parallel (k:nat) { SAppendIsAssociativeK(k, a, b, c); }
+ forall k:nat { SAppendIsAssociativeK(k, a, b, c); }
// assert for clarity only, postcondition follows directly from it
assert (forall k:nat :: SAppend(SAppend(a, b), c) ==#[k] SAppend(a, SAppend(b, c)));
}
diff --git a/Test/dafny3/Iter.dfy b/Test/dafny3/Iter.dfy index 3af868ca..c5e8f3a3 100644 --- a/Test/dafny3/Iter.dfy +++ b/Test/dafny3/Iter.dfy @@ -32,7 +32,7 @@ class List<T> { {
if (n == a.Length) {
var b := new T[2 * a.Length];
- parallel (i | 0 <= i < a.Length) {
+ forall i | 0 <= i < a.Length {
b[i] := a[i];
}
assert b[..n] == a[..n] == Contents;
diff --git a/Test/dafny3/SimpleInduction.dfy b/Test/dafny3/SimpleInduction.dfy index 5331b808..700b531c 100644 --- a/Test/dafny3/SimpleInduction.dfy +++ b/Test/dafny3/SimpleInduction.dfy @@ -22,7 +22,7 @@ ghost method FibLemma(n: nat) }
/*
- The 'parallel' statement has the effect of applying its body simultaneously
+ The 'forall' statement has the effect of applying its body simultaneously
to all values of the bound variables---in the first example, to all k
satisfying 0 <= k < n, and in the second example, to all non-negative n.
*/
@@ -30,7 +30,7 @@ ghost method FibLemma(n: nat) ghost method FibLemma_Alternative(n: nat)
ensures Fib(n) % 2 == 0 <==> n % 3 == 0;
{
- parallel (k | 0 <= k < n) {
+ forall k | 0 <= k < n {
FibLemma_Alternative(k);
}
}
@@ -38,7 +38,7 @@ ghost method FibLemma_Alternative(n: nat) ghost method FibLemma_All()
ensures forall n :: 0 <= n ==> (Fib(n) % 2 == 0 <==> n % 3 == 0);
{
- parallel (n | 0 <= n) {
+ forall n | 0 <= n {
FibLemma(n);
}
}
diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy index 757d6a37..1198c7e0 100644 --- a/Test/dafny3/Streams.dfy +++ b/Test/dafny3/Streams.dfy @@ -59,7 +59,7 @@ comethod Theorem0_Alt(M: Stream<X>) ghost method Theorem0_Par(M: Stream<X>)
ensures map_fg(M) == map_f(map_g(M));
{
- parallel (k: nat) {
+ forall k: nat {
Theorem0_Ind(k, M);
}
}
@@ -99,7 +99,7 @@ comethod Theorem1_Alt(M: Stream<X>, N: Stream<X>) ghost method Theorem1_Par(M: Stream<X>, N: Stream<X>)
ensures map_f(append(M, N)) == append(map_f(M), map_f(N));
{
- parallel (k: nat) {
+ forall k: nat {
Theorem1_Ind(k, M, N);
}
}
diff --git a/Test/dafny3/Zip.dfy b/Test/dafny3/Zip.dfy index 371b012a..80e8cd91 100644 --- a/Test/dafny3/Zip.dfy +++ b/Test/dafny3/Zip.dfy @@ -8,7 +8,7 @@ properties, drawing from: Some proofs are automatic (EvenZipLemma), whereas some others require a single
recursive call to be made explicitly.
-Note that the automatically inserted parallel statement
+Note that the automatically inserted forall statement
is in principle strong enough in all cases above, but the incompletness
of reasoning with quantifiers in SMT solvers make the explicit calls
necessary.
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy index 4373136b..e1a93730 100644 --- a/Test/vstte2012/BreadthFirstSearch.dfy +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -85,7 +85,7 @@ class BreadthFirstSearch<Vertex(==)> ghost var pathToV := Find(source, v, paths);
if (v == dest) {
- parallel (p | IsPath(source, dest, p))
+ forall p | IsPath(source, dest, p)
ensures |pathToV| <= |p|;
{
Lemma_IsPath_R(source, dest, p, AllVertices);
@@ -110,7 +110,7 @@ class BreadthFirstSearch<Vertex(==)> // show that "dest" in not in any reachability set, no matter
// how many successors one follows
- parallel (nn)
+ forall nn
ensures dest !in R(source, nn, AllVertices);
{
if (Value(nn) < Value(dd)) {
@@ -122,7 +122,7 @@ class BreadthFirstSearch<Vertex(==)> // Now, show what what the above means in terms of IsPath. More
// precisely, show that there is no path "p" from "source" to "dest".
- parallel (p | IsPath(source, dest, p))
+ forall p | IsPath(source, dest, p)
// this and the previous two lines will establish the
// absurdity of a "p" satisfying IsPath(source, dest, p)
ensures false;
@@ -130,7 +130,7 @@ class BreadthFirstSearch<Vertex(==)> Lemma_IsPath_R(source, dest, p, AllVertices);
// a consequence of Lemma_IsPath_R is:
// dest in R(source, ToNat(|p|), AllVertices)
- // but that contradicts the conclusion of the preceding parallel statement
+ // but that contradicts the conclusion of the preceding forall statement
}
d := -1; // indicate "no path"
diff --git a/Test/vstte2012/Combinators.dfy b/Test/vstte2012/Combinators.dfy index 46daf48d..dcc2e22d 100644 --- a/Test/vstte2012/Combinators.dfy +++ b/Test/vstte2012/Combinators.dfy @@ -225,7 +225,7 @@ ghost method Lemma_FindAndStep(t: Term) returns (r: Term, C: Context, u: Term) // that FindAndStep(b) gives C[Step(u)].
return Apply(t.car, r), value_C(t.car, C), u;
} else {
- parallel (C,u | IsContext(C) && t == EvalExpr(C,u))
+ forall C,u | IsContext(C) && t == EvalExpr(C,u)
ensures Step(u) == u;
{
// The following assert and the first assert of each "case" are
@@ -442,7 +442,7 @@ ghost method VerificationTask3() ensures forall n: nat ::
TerminatingReduction(ks(n)) == if n % 2 == 0 then K else Apply(K, K);
{
- parallel (n: nat) {
+ forall n: nat {
VT3(n);
}
}
diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy index 47ed19a4..1aa06408 100644 --- a/Test/vstte2012/Tree.dfy +++ b/Test/vstte2012/Tree.dfy @@ -116,7 +116,7 @@ ghost method lemma1(t: Tree, s:seq<int>) ghost method lemma2(s: seq<int>)
ensures (exists t: Tree :: toList(0,t) == s) ==> build(s).Res?;
{
- parallel(t | toList(0,t) == s) {
+ forall t | toList(0,t) == s {
lemma1(t, s);
}
}
@@ -130,7 +130,7 @@ ghost method lemma2(s: seq<int>) ghost method completeness()
ensures forall s: seq<int> :: ((exists t: Tree :: toList(0,t) == s) ==> build(s).Res?);
{
- parallel(s) {
+ forall s {
lemma2(s);
}
}
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index d1bdcf12..b043150c 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -40,7 +40,7 @@ `(,(dafny-regexp-opt '(
"assert" "assume" "break" "choose" "then" "else" "if" "label" "return" "yield"
"while" "print" "where"
- "old" "forall" "exists" "new" "parallel" "calc" "in" "this" "fresh"
+ "old" "forall" "exists" "new" "calc" "in" "this" "fresh"
"match" "case" "false" "true" "null")) . font-lock-keyword-face)
`(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "multiset" "map" "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 dd910820..fe7c6638 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -22,7 +22,7 @@ namespace Demo "assert", "assume", "new", "this", "object", "refines",
"abstract", "module", "import", "as", "default", "opened",
"if", "then", "else", "while", "invariant",
- "break", "label", "return", "yield", "parallel", "print",
+ "break", "label", "return", "yield", "print",
"returns", "yields", "requires", "ensures", "modifies", "reads", "decreases",
"bool", "nat", "int", "false", "true", "null",
"function", "predicate", "copredicate", "free",
@@ -293,7 +293,6 @@ namespace Demo | "label"
| "return"
| "yield"
- | "parallel"
| "calc"
| "print"
| "returns"
diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty index 4a3f6dbc..e3007b75 100644 --- a/Util/latex/dafny.sty +++ b/Util/latex/dafny.sty @@ -16,12 +16,13 @@ match,case,false,true,null,old,fresh,choose,this,
% statements
assert,assume,print,new,if,then,else,while,invariant,break,label,return,yield,
- parallel,where,calc
+ where,calc
},
literate=%
{:}{$\colon$}1
{::}{$\bullet$}2
{:=}{$:$$=$}2
+ {:|}{${:}\!\!|$}2
{!}{$\lnot$}1
{!!}{$\not\cap$}1
{==}{$=$}1
@@ -31,7 +32,6 @@ {<=}{$\le$}1
{>=}{$\ge$}1
% the following isn't actually Dafny, but it gives the option to produce nicer latex
- {|=>}{$\Rightarrow$}2
{<=set}{$\subseteq$}1
{+set}{$\cup$}1
{*set}{$\cap$}1
diff --git a/Util/vim/dafny.vim b/Util/vim/dafny.vim index b329f0f7..31f27c51 100644 --- a/Util/vim/dafny.vim +++ b/Util/vim/dafny.vim @@ -10,7 +10,7 @@ syntax keyword method constructor comethod syntax keyword dafnyTypeDef class datatype codatatype type iterator syntax keyword abstract module import opened as default syntax keyword dafnyConditional if then else match case -syntax keyword dafnyRepeat while parallel +syntax keyword dafnyRepeat while syntax keyword dafnyStatement assume assert return yield new print break label where calc syntax keyword dafnyKeyword var ghost returns yields null static this refines syntax keyword dafnyType bool nat int seq set multiset object array array2 array3 map |