summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Dafny/Dafny.atg35
-rw-r--r--Dafny/Parser.cs363
-rw-r--r--Dafny/Printer.cs4
-rw-r--r--Dafny/Scanner.cs102
-rw-r--r--Test/VSI-Benchmarks/b3.dfy9
-rw-r--r--Test/VSI-Benchmarks/b7.dfy8
-rw-r--r--Test/VSI-Benchmarks/b8.dfy30
-rw-r--r--Test/dafny0/Definedness.dfy8
-rw-r--r--Test/dafny0/NatTypes.dfy2
-rw-r--r--Test/dafny0/Termination.dfy2
-rw-r--r--Test/dafny0/TypeAntecedents.dfy2
-rw-r--r--Test/dafny0/TypeParameters.dfy10
-rw-r--r--Test/dafny1/Celebrity.dfy2
-rw-r--r--Test/dafny1/Rippling.dfy4
-rw-r--r--Test/dafny1/UltraFilter.dfy2
15 files changed, 284 insertions, 299 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index f6e40722..15d39460 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -188,7 +188,7 @@ Dafny
theModules.Add(module); .)
| ClassDecl<defaultModule, out c> (. defaultModule.TopLevelDecls.Add(c); .)
| DatatypeDecl<defaultModule, out dt> (. defaultModule.TopLevelDecls.Add(dt); .)
- | ClassMemberDecl<membersDefaultClass>
+ | ClassMemberDecl<membersDefaultClass, false>
}
(. if (defaultModuleCreatedHere) {
defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));
@@ -225,7 +225,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
[ "refines" Ident<out idRefined> (. optionalId = idRefined; .)
]
"{" (. bodyStart = t; .)
- { ClassMemberDecl<members>
+ { ClassMemberDecl<members, true>
}
"}"
(. if (optionalId == null)
@@ -237,7 +237,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
.)
.
-ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm.>
+ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
= (. Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
Function/*!*/ f;
@@ -248,8 +248,8 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm.>
| "unlimited" (. mmod.IsUnlimited = true; .)
}
( FieldDecl<mmod, mm>
- | FunctionDecl<mmod, out f> (. mm.Add(f); .)
- | MethodDecl<mmod, out m> (. mm.Add(m); .)
+ | FunctionDecl<mmod, out f> (. mm.Add(f); .)
+ | MethodDecl<mmod, allowConstructors, out m> (. mm.Add(m); .)
| CouplingInvDecl<mmod, mm>
)
.
@@ -404,7 +404,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
/*------------------------------------------------------------------------*/
-MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
+MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
IToken/*!*/ id;
Attributes attrs = null;
@@ -422,8 +422,13 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
IToken bodyEnd = Token.NoToken;
.)
( "method"
- | "constructor" (. isConstructor = true; .)
- | "refines" (. isRefinement = true; .)
+ | "constructor" (. if (allowConstructor) {
+ isConstructor = true;
+ } else {
+ SemErr(t, "constructors are only allowed in classes");
+ }
+ .)
+ | "refines" (. isRefinement = true; .)
)
(. if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
if (isConstructor) {
@@ -443,9 +448,9 @@ MethodDecl<MemberModifiers mmod, out Method/*!*/ m>
Formals<false, !mmod.IsGhost, outs>
]
- ( ";" { MethodSpec<req, mod, ens, dec> }
- | { MethodSpec<req, mod, ens, dec> } BlockStmt<out bb, out bodyStart, out bodyEnd> (. body = (BlockStmt)bb; .)
- )
+ { MethodSpec<req, mod, ens, dec> }
+ [ BlockStmt<out bb, out bodyStart, out bodyEnd> (. body = (BlockStmt)bb; .)
+ ]
(. if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
@@ -588,11 +593,9 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
Formals<true, isFunctionMethod, formals>
":"
Type<out returnType>
- ( ";"
- { FunctionSpec<reqs, reads, ens, decreases> }
- | { FunctionSpec<reqs, reads, ens, decreases> }
- FunctionBody<out bb, out bodyStart, out bodyEnd> (. body = bb; .)
- )
+ { FunctionSpec<reqs, reads, ens, decreases> }
+ [ FunctionBody<out bb, out bodyStart, out bodyEnd> (. body = bb; .)
+ ]
(. f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index e12ab7e3..42014762 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
const bool T = true;
const bool x = false;
const int minErrDist = 2;
-
+
public Scanner/*!*/ scanner;
public Errors/*!*/ errors;
@@ -144,10 +144,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (errDist >= minErrDist) errors.SemErr(t, msg);
errDist = 0;
}
-
- public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
- Contract.Requires(tok != null);
- Contract.Requires(msg != null);
+
+ public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(msg != null);
errors.SemErr(tok, msg);
}
@@ -160,15 +160,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
la = t;
}
}
-
+
void Expect (int n) {
if (la.kind==n) Get(); else { SynErr(n); }
}
-
+
bool StartOf (int s) {
return set[s, la.kind];
}
-
+
void ExpectWeak (int n, int follow) {
if (la.kind == n) Get();
else {
@@ -192,7 +192,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
}
-
+
void Dafny() {
ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
@@ -246,7 +246,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
DatatypeDecl(defaultModule, out dt);
defaultModule.TopLevelDecls.Add(dt);
} else {
- ClassMemberDecl(membersDefaultClass);
+ ClassMemberDecl(membersDefaultClass, false);
}
}
if (defaultModuleCreatedHere) {
@@ -316,7 +316,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Expect(7);
bodyStart = t;
while (StartOf(2)) {
- ClassMemberDecl(members);
+ ClassMemberDecl(members, true);
}
Expect(8);
if (optionalId == null)
@@ -359,7 +359,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
}
- void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm) {
+ void ClassMemberDecl(List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors) {
Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
Function/*!*/ f;
@@ -383,7 +383,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (la.kind == 10 || la.kind == 25 || la.kind == 26) {
- MethodDecl(mmod, out m);
+ MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
} else if (la.kind == 20) {
CouplingInvDecl(mmod, mm);
@@ -459,25 +459,20 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Formals(true, isFunctionMethod, formals);
Expect(22);
Type(out returnType);
- if (la.kind == 17) {
- Get();
- while (StartOf(3)) {
- FunctionSpec(reqs, reads, ens, decreases);
- }
- } else if (StartOf(4)) {
- while (StartOf(3)) {
- FunctionSpec(reqs, reads, ens, decreases);
- }
+ while (StartOf(3)) {
+ FunctionSpec(reqs, reads, ens, decreases);
+ }
+ if (la.kind == 7) {
FunctionBody(out bb, out bodyStart, out bodyEnd);
body = bb;
- } else SynErr(106);
+ }
f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
}
- void MethodDecl(MemberModifiers mmod, out Method/*!*/ m) {
+ void MethodDecl(MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m) {
Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
IToken/*!*/ id;
Attributes attrs = null;
@@ -498,11 +493,16 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
Get();
} else if (la.kind == 26) {
Get();
- isConstructor = true;
+ if (allowConstructor) {
+ isConstructor = true;
+ } else {
+ SemErr(t, "constructors are only allowed in classes");
+ }
+
} else if (la.kind == 10) {
Get();
isRefinement = true;
- } else SynErr(107);
+ } else SynErr(106);
if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }
if (isConstructor) {
if (mmod.IsGhost) {
@@ -526,18 +526,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs);
}
- if (la.kind == 17) {
- Get();
- while (StartOf(5)) {
- MethodSpec(req, mod, ens, dec);
- }
- } else if (StartOf(6)) {
- while (StartOf(5)) {
- MethodSpec(req, mod, ens, dec);
- }
+ while (StartOf(4)) {
+ MethodSpec(req, mod, ens, dec);
+ }
+ if (la.kind == 7) {
BlockStmt(out bb, out bodyStart, out bodyEnd);
body = (BlockStmt)bb;
- } else SynErr(108);
+ }
if (isRefinement)
m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);
else if (isConstructor)
@@ -596,7 +591,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
Expect(33);
- if (StartOf(7)) {
+ if (StartOf(5)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
while (la.kind == 19) {
@@ -734,7 +729,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(109); break;
+ default: SynErr(107); break;
}
}
@@ -760,7 +755,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 28) {
Get();
- if (StartOf(8)) {
+ if (StartOf(6)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 19) {
@@ -785,12 +780,12 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out e);
Expect(17);
ens.Add(new MaybeFreeExpression(e, isFree));
- } else SynErr(110);
+ } else SynErr(108);
} else if (la.kind == 32) {
Get();
DecreasesList(decreases, false);
Expect(17);
- } else SynErr(111);
+ } else SynErr(109);
}
void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -799,7 +794,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(7);
bodyStart = t;
- while (StartOf(9)) {
+ while (StartOf(7)) {
Stmt(body);
}
Expect(8);
@@ -880,7 +875,7 @@ List<Expression/*!*/>/*!*/ decreases) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt);
- } else SynErr(112);
+ } else SynErr(110);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
@@ -893,7 +888,7 @@ List<Expression/*!*/>/*!*/ decreases) {
reqs.Add(e);
} else if (la.kind == 42) {
Get();
- if (StartOf(10)) {
+ if (StartOf(8)) {
PossiblyWildFrameExpression(out fe);
reads.Add(fe);
while (la.kind == 19) {
@@ -912,7 +907,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
DecreasesList(decreases, false);
Expect(17);
- } else SynErr(113);
+ } else SynErr(111);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -929,9 +924,9 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 43) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
- } else if (StartOf(8)) {
+ } else if (StartOf(6)) {
FrameExpression(out fe);
- } else SynErr(114);
+ } else SynErr(112);
}
void PossiblyWildExpression(out Expression/*!*/ e) {
@@ -940,9 +935,9 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 43) {
Get();
e = new WildcardExpr(t);
- } else if (StartOf(8)) {
+ } else if (StartOf(6)) {
Expression(out e);
- } else SynErr(115);
+ } else SynErr(113);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1019,7 +1014,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
breakCount++;
}
- } else SynErr(116);
+ } else SynErr(114);
Expect(17);
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
@@ -1028,7 +1023,7 @@ List<Expression/*!*/>/*!*/ decreases) {
ReturnStmt(out s);
break;
}
- default: SynErr(117); break;
+ default: SynErr(115); break;
}
}
@@ -1099,7 +1094,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 22) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(118);
+ } else SynErr(116);
s = new UpdateStmt(x, lhss, rhss);
}
@@ -1172,13 +1167,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 7) {
BlockStmt(out s, out bodyStart, out bodyEnd);
els = s;
- } else SynErr(119);
+ } else SynErr(117);
}
ifStmt = new IfStmt(x, guard, thn, els);
} else if (la.kind == 7) {
AlternativeBlock(out alternatives);
ifStmt = new AlternativeStmt(x, alternatives);
- } else SynErr(120);
+ } else SynErr(118);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -1200,11 +1195,11 @@ List<Expression/*!*/>/*!*/ decreases) {
LoopSpec(out invariants, out decreases, out mod);
BlockStmt(out body, out bodyStart, out bodyEnd);
stmt = new WhileStmt(x, guard, invariants, decreases, mod, body);
- } else if (StartOf(11)) {
+ } else if (StartOf(9)) {
LoopSpec(out invariants, out decreases, out mod);
AlternativeBlock(out alternatives);
stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives);
- } else SynErr(121);
+ } else SynErr(119);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -1278,7 +1273,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(47);
returnTok = t;
- if (StartOf(12)) {
+ if (StartOf(10)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
while (la.kind == 19) {
@@ -1316,7 +1311,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Ident(out x);
Expect(33);
args = new List<Expression/*!*/>();
- if (StartOf(8)) {
+ if (StartOf(6)) {
Expressions(args);
}
Expect(34);
@@ -1338,10 +1333,10 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 43) {
Get();
r = new HavocRhs(t);
- } else if (StartOf(8)) {
+ } else if (StartOf(6)) {
Expression(out e);
r = new ExprRhs(e);
- } else SynErr(122);
+ } else SynErr(120);
}
void Lhs(out Expression e) {
@@ -1352,13 +1347,13 @@ List<Expression/*!*/>/*!*/ decreases) {
while (la.kind == 50 || la.kind == 52) {
Suffix(ref e);
}
- } else if (StartOf(13)) {
+ } else if (StartOf(11)) {
ConstAtomExpression(out e);
Suffix(ref e);
while (la.kind == 50 || la.kind == 52) {
Suffix(ref e);
}
- } else SynErr(123);
+ } else SynErr(121);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -1378,10 +1373,10 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 43) {
Get();
e = null;
- } else if (StartOf(8)) {
+ } else if (StartOf(6)) {
Expression(out ee);
e = ee;
- } else SynErr(124);
+ } else SynErr(122);
Expect(34);
}
@@ -1398,7 +1393,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expression(out e);
Expect(57);
body = new List<Statement>();
- while (StartOf(9)) {
+ while (StartOf(7)) {
Stmt(body);
}
alternatives.Add(new GuardedAlternative(x, e, body));
@@ -1412,7 +1407,7 @@ List<Expression/*!*/>/*!*/ decreases) {
decreases = new List<Expression/*!*/>();
mod = null;
- while (StartOf(14)) {
+ while (StartOf(12)) {
if (la.kind == 29 || la.kind == 59) {
isFree = false;
if (la.kind == 29) {
@@ -1430,7 +1425,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else {
Get();
mod = mod ?? new List<FrameExpression>();
- if (StartOf(8)) {
+ if (StartOf(6)) {
FrameExpression(out fe);
mod.Add(fe);
while (la.kind == 19) {
@@ -1465,7 +1460,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(34);
}
Expect(57);
- while (StartOf(9)) {
+ while (StartOf(7)) {
Stmt(body);
}
c = new MatchCaseStmt(x, id.val, arguments, body);
@@ -1476,10 +1471,10 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 4) {
Get();
arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2));
- } else if (StartOf(8)) {
+ } else if (StartOf(6)) {
Expression(out e);
arg = new Attributes.Argument(e);
- } else SynErr(125);
+ } else SynErr(123);
}
void EquivExpression(out Expression/*!*/ e0) {
@@ -1509,13 +1504,13 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 67) {
Get();
- } else SynErr(126);
+ } else SynErr(124);
}
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(15)) {
+ if (StartOf(13)) {
if (la.kind == 70 || la.kind == 71) {
AndOp();
x = t;
@@ -1547,7 +1542,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 69) {
Get();
- } else SynErr(127);
+ } else SynErr(125);
}
void RelationalExpression(out Expression/*!*/ e) {
@@ -1564,15 +1559,15 @@ List<Expression/*!*/>/*!*/ decreases) {
Term(out e0);
e = e0;
- if (StartOf(16)) {
+ if (StartOf(14)) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
e = new BinaryExpr(x, op, e0, e1);
if (op == BinaryExpr.Opcode.Disjoint)
- acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
- while (StartOf(16)) {
+ while (StartOf(14)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -1603,36 +1598,35 @@ List<Expression/*!*/>/*!*/ decreases) {
break;
case BinaryExpr.Opcode.Neq:
if (hasSeenNeq) { SemErr(x, "a chain cannot have more than one != operator"); }
- if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }
- hasSeenNeq = true; break;
- case BinaryExpr.Opcode.Lt:
- case BinaryExpr.Opcode.Le:
- if (kind == 0) { kind = 1; }
- else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }
- break;
- case BinaryExpr.Opcode.Gt:
- case BinaryExpr.Opcode.Ge:
- if (kind == 0) { kind = 2; }
- else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
- break;
- case BinaryExpr.Opcode.Disjoint:
- if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }
- break;
- default:
- SemErr(x, "this operator cannot be part of a chain");
- kind = 3; break;
- }
-
+ if (kind != 0 && kind != 1 && kind != 2) { SemErr(x, "this operator cannot continue this chain"); }
+ hasSeenNeq = true; break;
+ case BinaryExpr.Opcode.Lt:
+ case BinaryExpr.Opcode.Le:
+ if (kind == 0) { kind = 1; }
+ else if (kind != 1) { SemErr(x, "this operator chain cannot continue with an ascending operator"); }
+ break;
+ case BinaryExpr.Opcode.Gt:
+ case BinaryExpr.Opcode.Ge:
+ if (kind == 0) { kind = 2; }
+ else if (kind != 2) { SemErr(x, "this operator chain cannot continue with a descending operator"); }
+ break;
+ case BinaryExpr.Opcode.Disjoint:
+ if (kind != 4) { SemErr(x, "can only chain disjoint (!!) with itself."); kind = 3; }
+ break;
+ default:
+ SemErr(x, "this operator cannot be part of a chain");
+ kind = 3; break;
+ }
+
Term(out e1);
ops.Add(op); chain.Add(e1);
- if (op == BinaryExpr.Opcode.Disjoint)
- {
+ if (op == BinaryExpr.Opcode.Disjoint) {
e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));
- acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
- }
- else
- e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
-
+ acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.
+ }
+ else
+ e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));
+
}
}
if (chain != null) {
@@ -1646,7 +1640,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 71) {
Get();
- } else SynErr(128);
+ } else SynErr(126);
}
void OrOp() {
@@ -1654,7 +1648,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 73) {
Get();
- } else SynErr(129);
+ } else SynErr(127);
}
void Term(out Expression/*!*/ e0) {
@@ -1730,7 +1724,7 @@ List<Expression/*!*/>/*!*/ decreases) {
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(130); break;
+ default: SynErr(128); break;
}
}
@@ -1752,7 +1746,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 84) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(131);
+ } else SynErr(129);
}
void UnaryExpression(out Expression/*!*/ e) {
@@ -1794,7 +1788,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
break;
}
- default: SynErr(132); break;
+ default: SynErr(130); break;
}
}
@@ -1809,7 +1803,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 86) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(133);
+ } else SynErr(131);
}
void NegOp() {
@@ -1817,7 +1811,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 88) {
Get();
- } else SynErr(134);
+ } else SynErr(132);
}
void EndlessExpression(out Expression e) {
@@ -1836,11 +1830,11 @@ List<Expression/*!*/>/*!*/ decreases) {
e = new ITEExpr(x, e, e0, e1);
} else if (la.kind == 60) {
MatchExpression(out e);
- } else if (StartOf(17)) {
+ } else if (StartOf(15)) {
QuantifierGuts(out e);
} else if (la.kind == 38) {
ComprehensionExpr(out e);
- } else SynErr(135);
+ } else SynErr(133);
}
void DottedIdentifiersAndFunction(out Expression e) {
@@ -1858,7 +1852,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 33) {
Get();
openParen = t; args = new List<Expression>();
- if (StartOf(8)) {
+ if (StartOf(6)) {
Expressions(args);
}
Expect(34);
@@ -1878,7 +1872,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 33) {
Get();
args = new List<Expression/*!*/>(); func = true;
- if (StartOf(8)) {
+ if (StartOf(6)) {
Expressions(args);
}
Expect(34);
@@ -1888,13 +1882,13 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 50) {
Get();
x = t;
- if (StartOf(8)) {
+ if (StartOf(6)) {
Expression(out ee);
e0 = ee;
if (la.kind == 97) {
Get();
anyDots = true;
- if (StartOf(8)) {
+ if (StartOf(6)) {
Expression(out ee);
e1 = ee;
}
@@ -1913,12 +1907,12 @@ List<Expression/*!*/>/*!*/ decreases) {
multipleIndices.Add(ee);
}
- } else SynErr(136);
+ } else SynErr(134);
} else if (la.kind == 97) {
Get();
Expression(out ee);
anyDots = true; e1 = ee;
- } else SynErr(137);
+ } else SynErr(135);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -1942,7 +1936,7 @@ List<Expression/*!*/>/*!*/ decreases) {
}
Expect(51);
- } else SynErr(138);
+ } else SynErr(136);
}
void DisplayExpr(out Expression e) {
@@ -1953,7 +1947,7 @@ List<Expression/*!*/>/*!*/ decreases) {
if (la.kind == 7) {
Get();
x = t; elements = new List<Expression/*!*/>();
- if (StartOf(8)) {
+ if (StartOf(6)) {
Expressions(elements);
}
e = new SetDisplayExpr(x, elements);
@@ -1961,12 +1955,12 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 50) {
Get();
x = t; elements = new List<Expression/*!*/>();
- if (StartOf(8)) {
+ if (StartOf(6)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
Expect(51);
- } else SynErr(139);
+ } else SynErr(137);
}
void ConstAtomExpression(out Expression/*!*/ e) {
@@ -2043,7 +2037,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(34);
break;
}
- default: SynErr(140); break;
+ default: SynErr(138); break;
}
}
@@ -2088,7 +2082,7 @@ List<Expression/*!*/>/*!*/ decreases) {
} else if (la.kind == 100 || la.kind == 101) {
Exists();
x = t;
- } else SynErr(141);
+ } else SynErr(139);
IdentTypeOptional(out bv);
bvars.Add(bv);
while (la.kind == 19) {
@@ -2170,7 +2164,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 99) {
Get();
- } else SynErr(142);
+ } else SynErr(140);
}
void Exists() {
@@ -2178,7 +2172,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 101) {
Get();
- } else SynErr(143);
+ } else SynErr(141);
}
void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {
@@ -2187,11 +2181,11 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(7);
if (la.kind == 22) {
AttributeBody(ref attrs);
- } else if (StartOf(8)) {
+ } else if (StartOf(6)) {
es = new List<Expression/*!*/>();
Expressions(es);
trigs = new Triggers(es, trigs);
- } else SynErr(144);
+ } else SynErr(142);
Expect(8);
}
@@ -2200,7 +2194,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Get();
} else if (la.kind == 103) {
Get();
- } else SynErr(145);
+ } else SynErr(143);
}
void AttributeBody(ref Attributes attrs) {
@@ -2211,7 +2205,7 @@ List<Expression/*!*/>/*!*/ decreases) {
Expect(22);
Expect(1);
aName = t.val;
- if (StartOf(18)) {
+ if (StartOf(16)) {
AttributeArg(out aArg);
aArgs.Add(aArg);
while (la.kind == 19) {
@@ -2227,21 +2221,19 @@ List<Expression/*!*/>/*!*/ decreases) {
public void Parse() {
la = new Token();
- la.val = "";
+ la.val = "";
Get();
Dafny();
- Expect(0);
+ Expect(0);
}
-
+
static readonly bool[,]/*!*/ set = {
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,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,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,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,T,x, x,x,T,x, T,T,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,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
@@ -2262,20 +2254,18 @@ List<Expression/*!*/>/*!*/ decreases) {
public class Errors {
public int count = 0; // number of errors detected
public System.IO.TextWriter/*!*/ errorStream = Console.Out; // error messages go to this stream
- public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
- public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
-
+ public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text
+ public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text
+
public void SynErr(string filename, int line, int col, int n) {
- SynErr(filename, line, col, GetSyntaxErrorString(n));
- }
-
- public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ SynErr(filename, line, col, GetSyntaxErrorString(n));
+ }
+ public virtual void SynErr(string filename, int line, int col, string msg) {
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
- }
-
- string GetSyntaxErrorString(int n) {
+ }
+ string GetSyntaxErrorString(int n) {
string s;
switch (n) {
case 0: s = "EOF expected"; break;
@@ -2384,50 +2374,48 @@ public class Errors {
case 103: s = "\"\\u2022\" expected"; break;
case 104: s = "??? expected"; break;
case 105: s = "invalid ClassMemberDecl"; break;
- case 106: s = "invalid FunctionDecl"; break;
- case 107: s = "invalid MethodDecl"; break;
- case 108: s = "invalid MethodDecl"; break;
- case 109: s = "invalid TypeAndToken"; break;
- case 110: s = "invalid MethodSpec"; break;
- case 111: s = "invalid MethodSpec"; break;
- case 112: s = "invalid ReferenceType"; break;
- case 113: s = "invalid FunctionSpec"; break;
- case 114: s = "invalid PossiblyWildFrameExpression"; break;
- case 115: s = "invalid PossiblyWildExpression"; break;
- case 116: s = "invalid OneStmt"; break;
- case 117: s = "invalid OneStmt"; break;
- case 118: s = "invalid UpdateStmt"; break;
- case 119: s = "invalid IfStmt"; break;
- case 120: s = "invalid IfStmt"; break;
- case 121: s = "invalid WhileStmt"; break;
- case 122: s = "invalid Rhs"; break;
- case 123: s = "invalid Lhs"; break;
- case 124: s = "invalid Guard"; break;
- case 125: s = "invalid AttributeArg"; break;
- case 126: s = "invalid EquivOp"; break;
- case 127: s = "invalid ImpliesOp"; break;
- case 128: s = "invalid AndOp"; break;
- case 129: s = "invalid OrOp"; break;
- case 130: s = "invalid RelOp"; break;
- case 131: s = "invalid AddOp"; break;
- case 132: s = "invalid UnaryExpression"; break;
- case 133: s = "invalid MulOp"; break;
- case 134: s = "invalid NegOp"; break;
- case 135: s = "invalid EndlessExpression"; break;
+ case 106: s = "invalid MethodDecl"; break;
+ case 107: s = "invalid TypeAndToken"; break;
+ case 108: s = "invalid MethodSpec"; break;
+ case 109: s = "invalid MethodSpec"; break;
+ case 110: s = "invalid ReferenceType"; break;
+ case 111: s = "invalid FunctionSpec"; break;
+ case 112: s = "invalid PossiblyWildFrameExpression"; break;
+ case 113: s = "invalid PossiblyWildExpression"; break;
+ case 114: s = "invalid OneStmt"; break;
+ case 115: s = "invalid OneStmt"; break;
+ case 116: s = "invalid UpdateStmt"; break;
+ case 117: s = "invalid IfStmt"; break;
+ case 118: s = "invalid IfStmt"; break;
+ case 119: s = "invalid WhileStmt"; break;
+ case 120: s = "invalid Rhs"; break;
+ case 121: s = "invalid Lhs"; break;
+ case 122: s = "invalid Guard"; break;
+ case 123: s = "invalid AttributeArg"; break;
+ case 124: s = "invalid EquivOp"; break;
+ case 125: s = "invalid ImpliesOp"; break;
+ case 126: s = "invalid AndOp"; break;
+ case 127: s = "invalid OrOp"; break;
+ case 128: s = "invalid RelOp"; break;
+ case 129: s = "invalid AddOp"; break;
+ case 130: s = "invalid UnaryExpression"; break;
+ case 131: s = "invalid MulOp"; break;
+ case 132: s = "invalid NegOp"; break;
+ case 133: s = "invalid EndlessExpression"; break;
+ case 134: s = "invalid Suffix"; break;
+ case 135: s = "invalid Suffix"; break;
case 136: s = "invalid Suffix"; break;
- case 137: s = "invalid Suffix"; break;
- case 138: s = "invalid Suffix"; break;
- case 139: s = "invalid DisplayExpr"; break;
- case 140: s = "invalid ConstAtomExpression"; break;
- case 141: s = "invalid QuantifierGuts"; break;
- case 142: s = "invalid Forall"; break;
- case 143: s = "invalid Exists"; break;
- case 144: s = "invalid AttributeOrTrigger"; break;
- case 145: s = "invalid QSep"; break;
+ case 137: s = "invalid DisplayExpr"; break;
+ case 138: s = "invalid ConstAtomExpression"; break;
+ case 139: s = "invalid QuantifierGuts"; break;
+ case 140: s = "invalid Forall"; break;
+ case 141: s = "invalid Exists"; break;
+ case 142: s = "invalid AttributeOrTrigger"; break;
+ case 143: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
- return s;
+ return s;
}
public void SemErr(IToken/*!*/ tok, string/*!*/ msg) { // semantic errors
@@ -2435,9 +2423,8 @@ public class Errors {
Contract.Requires(msg != null);
SemErr(tok.filename, tok.line, tok.col, msg);
}
-
public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {
- Contract.Requires(msg != null);
+ Contract.Requires(msg != null);
errorStream.WriteLine(errMsgFormat, filename, line, col, msg);
count++;
}
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index e49ce6e9..b9c8601e 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -230,7 +230,7 @@ namespace Microsoft.Dafny {
PrintFormals(f.Formals);
wr.Write(": ");
PrintType(f.ResultType);
- wr.WriteLine(f.Body == null ? ";" : "");
+ wr.WriteLine();
int ind = indent + IndentAmount;
PrintSpec("requires", f.Req, ind);
@@ -277,7 +277,7 @@ namespace Microsoft.Dafny {
}
PrintFormals(method.Outs);
}
- wr.WriteLine(method.Body == null ? ";" : "");
+ wr.WriteLine();
int ind = indent + IndentAmount;
PrintSpec("requires", method.Req, ind);
diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 81f556c8..19157a32 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
// a) whole stream in buffer
// b) part of stream in buffer
// 2) non seekable stream (network, console)
-
+
public const int EOF = 65535 + 1; // char.MaxValue + 1;
const int MIN_BUFFER_LENGTH = 1024; // 1KB
const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB
@@ -31,17 +31,15 @@ public class Buffer {
Stream/*!*/ stream; // input stream (seekable)
bool isUserStream; // was the stream opened by the user?
- [ContractInvariantMethod]
- void ObjectInvariant(){
- Contract.Invariant(buf != null);
- Contract.Invariant(stream != null);
- }
-
-// [NotDelayed]
- public Buffer (Stream/*!*/ s, bool isUserStream) : base() {
+[ContractInvariantMethod]
+void ObjectInvariant(){
+ Contract.Invariant(buf != null);
+ Contract.Invariant(stream != null);}
+ [NotDelayed]
+ public Buffer (Stream/*!*/ s, bool isUserStream) :base() {
Contract.Requires(s != null);
stream = s; this.isUserStream = isUserStream;
-
+
int fl, bl;
if (s.CanSeek) {
fl = (int) s.Length;
@@ -53,12 +51,12 @@ public class Buffer {
buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];
fileLen = fl; bufLen = bl;
-
+
if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)
else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid
if (bufLen == fileLen && s.CanSeek) Close();
}
-
+
protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor
Contract.Requires(b != null);
buf = b.buf;
@@ -75,14 +73,14 @@ public class Buffer {
}
~Buffer() { Close(); }
-
+
protected void Close() {
if (!isUserStream && stream != null) {
stream.Close();
//stream = null;
}
}
-
+
public virtual int Read () {
if (bufPos < bufLen) {
return buf[bufPos++];
@@ -102,7 +100,7 @@ public class Buffer {
Pos = curPos;
return ch;
}
-
+
public string/*!*/ GetString (int beg, int end) {
Contract.Ensures(Contract.Result<string>() != null);
int len = 0;
@@ -141,7 +139,7 @@ public class Buffer {
}
}
}
-
+
// Read the next chunk of bytes from the stream, increases the buffer
// if needed and updates the fields fileLen and bufLen.
// Returns the number of bytes read.
@@ -215,20 +213,19 @@ public class Scanner {
const int noSym = 104;
- [ContractInvariantMethod]
- void objectInvariant(){
- Contract.Invariant(buffer!=null);
- Contract.Invariant(t != null);
- Contract.Invariant(start != null);
- Contract.Invariant(tokens != null);
- Contract.Invariant(pt != null);
- Contract.Invariant(tval != null);
- Contract.Invariant(Filename != null);
- Contract.Invariant(errorHandler != null);
- }
-
+[ContractInvariantMethod]
+void objectInvariant(){
+ Contract.Invariant(buffer!=null);
+ Contract.Invariant(t != null);
+ Contract.Invariant(start != null);
+ Contract.Invariant(tokens != null);
+ Contract.Invariant(pt != null);
+ Contract.Invariant(tval != null);
+ Contract.Invariant(Filename != null);
+ Contract.Invariant(errorHandler != null);
+}
public Buffer/*!*/ buffer; // scanner buffer
-
+
Token/*!*/ t; // current token
int ch; // current input character
int pos; // byte position of current character
@@ -239,13 +236,13 @@ public class Scanner {
Token/*!*/ tokens; // list of tokens already peeked (first token is a dummy)
Token/*!*/ pt; // current peek token
-
+
char[]/*!*/ tval = new char[128]; // text of current token
int tlen; // length of current token
-
+
private string/*!*/ Filename;
private Errors/*!*/ errorHandler;
-
+
static Scanner() {
start = new Hashtable(128);
for (int i = 39; i <= 39; ++i) start[i] = 1;
@@ -293,9 +290,9 @@ public class Scanner {
start[Buffer.EOF] = -1;
}
-
-// [NotDelayed]
- public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {
+
+ [NotDelayed]
+ public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){
Contract.Requires(fileName != null);
Contract.Requires(errorHandler != null);
this.errorHandler = errorHandler;
@@ -305,14 +302,15 @@ public class Scanner {
Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
buffer = new Buffer(stream, false);
Filename = fileName;
+
Init();
} catch (IOException) {
throw new FatalError("Cannot open file " + fileName);
}
}
-
-// [NotDelayed]
- public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {
+
+ [NotDelayed]
+ public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){
Contract.Requires(s != null);
Contract.Requires(errorHandler != null);
Contract.Requires(fileName != null);
@@ -321,9 +319,10 @@ public class Scanner {
buffer = new Buffer(s, true);
this.errorHandler = errorHandler;
this.Filename = fileName;
+
Init();
}
-
+
void Init() {
pos = -1; line = 1; col = 0;
oldEols = 0;
@@ -344,11 +343,11 @@ public class Scanner {
Contract.Ensures(Contract.Result<string>() != null);
int p = buffer.Pos;
int ch = buffer.Read();
- // replace isolated '\r' by '\n' in order to make
+ // replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
while (ch != EOL && ch != Buffer.EOF){
- ch = buffer.Read();
+ ch = buffer.Read();
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
@@ -359,7 +358,7 @@ public class Scanner {
}
void NextCh() {
- if (oldEols > 0) { ch = EOL; oldEols--; }
+ if (oldEols > 0) { ch = EOL; oldEols--; }
else {
// pos = buffer.Pos;
// ch = buffer.Read(); col++;
@@ -367,9 +366,9 @@ public class Scanner {
// // eol handling uniform across Windows, Unix and Mac
// if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
// if (ch == EOL) { line++; col = 0; }
-
+
while (true) {
- pos = buffer.Pos;
+ pos = buffer.Pos;
ch = buffer.Read(); col++;
// replace isolated '\r' by '\n' in order to make
// eol handling uniform across Windows, Unix and Mac
@@ -419,7 +418,7 @@ public class Scanner {
return;
}
-
+
}
}
@@ -556,13 +555,10 @@ public class Scanner {
t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
- if (start.ContainsKey(ch)) {
- Contract.Assert(start[ch] != null);
- state = (int) start[ch];
- }
+ if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }
else { state = 0; }
tlen = 0; AddCh();
-
+
switch (state) {
case -1: { t.kind = eofSym; break; } // NextCh already done
case 0: {
@@ -768,14 +764,14 @@ public class Scanner {
t.val = new String(tval, 0, tlen);
return t;
}
-
+
private void SetScannerBehindT() {
buffer.Pos = t.pos;
NextCh();
line = t.line; col = t.col;
for (int i = 0; i < tlen; i++) NextCh();
}
-
+
// get the next token (possibly a token already seen during peeking)
public Token/*!*/ Scan () {
Contract.Ensures(Contract.Result<Token>() != null);
@@ -796,7 +792,7 @@ public class Scanner {
}
pt = pt.next;
} while (pt.kind > maxT); // skip pragmas
-
+
return pt;
}
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 3de94555..7cf3de07 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -12,13 +12,13 @@
class Queue<T> {
var contents: seq<T>;
- method Init();
+ method Init()
modifies this;
ensures |contents| == 0;
- method Enqueue(x: T);
+ method Enqueue(x: T)
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: T);
+ method Dequeue() returns (x: T)
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
@@ -33,7 +33,7 @@ class Queue<T> {
}
class Comparable {
- function AtMost(c: Comparable): bool;
+ function AtMost(c: Comparable): bool
reads this, c;
}
@@ -96,7 +96,6 @@ class Benchmark3 {
}
-
method RemoveMin(q: Queue<int>) returns (m: int, k: int) //m is the min, k is m's index in q
requires q != null && |q.contents| != 0;
modifies q;
diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index f34f5c00..d6759c5f 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -8,13 +8,13 @@
class Queue<T> {
var contents: seq<T>;
- method Init();
+ method Init()
modifies this;
ensures |contents| == 0;
- method Enqueue(x: T);
+ method Enqueue(x: T)
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: T);
+ method Dequeue() returns (x: T)
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
@@ -101,7 +101,7 @@ class Stream {
class Client {
- method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>);
+ method Sort(q: Queue<int>) returns (r: Queue<int>, perm:seq<int>)
requires q != null;
modifies q;
ensures r != null && fresh(r);
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 0c9d1186..383bccfd 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -6,13 +6,13 @@
class Queue<T> {
var contents: seq<T>;
- method Init();
+ method Init()
modifies this;
ensures |contents| == 0;
- method Enqueue(x: T);
+ method Enqueue(x: T)
modifies this;
ensures contents == old(contents) + [x];
- method Dequeue() returns (x: T);
+ method Dequeue() returns (x: T)
requires 0 < |contents|;
modifies this;
ensures contents == old(contents)[1..] && x == old(contents)[0];
@@ -28,7 +28,7 @@ class Queue<T> {
class Glossary {
- method Sort(q: Queue<Word>) returns (r: Queue<Word>, perm:seq<int>);
+ method Sort(q: Queue<Word>) returns (r: Queue<Word>, perm:seq<int>)
requires q != null;
modifies q;
ensures r != null && fresh(r);
@@ -149,29 +149,29 @@ class Glossary {
class Word
{
- function AtMost(w:Word) :bool;
+ function AtMost(w: Word): bool
}
class ReaderStream {
- ghost var footprint:set<object>;
- var isOpen:bool;
+ ghost var footprint: set<object>;
+ var isOpen: bool;
- function Valid():bool
- reads this, footprint;
+ function Valid(): bool
+ reads this, footprint;
{
null !in footprint && this in footprint && isOpen
}
method Open() //reading
- modifies this;
- ensures Valid() && fresh(footprint -{this});
+ modifies this;
+ ensures Valid() && fresh(footprint -{this});
{
footprint := {this};
isOpen :=true;
}
- method GetWord()returns(x:Word)
- requires Valid() ;
+ method GetWord() returns (x: Word)
+ requires Valid();
modifies footprint;
ensures Valid() && fresh(footprint - old(footprint));
{
@@ -190,8 +190,8 @@ class WriterStream {
var stream:seq<int>;
var isOpen:bool;
- function Valid():bool
- reads this, footprint;
+ function Valid(): bool
+ reads this, footprint;
{
null !in footprint && this in footprint && isOpen
}
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index 8df1a7c5..2063eec4 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -44,17 +44,17 @@ class SoWellformed {
c := true;
}
- method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed);
+ method P(a: SoWellformed, b: int) returns (c: bool, d: SoWellformed)
requires next != null;
modifies this;
ensures next.xyz < 100; // error: may not be well-defined (if body sets next to null)
- method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+ method Q(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
requires next != null;
modifies s;
ensures next.xyz < 100; // error: may not be well-defined (if this in s and body sets next to null)
- method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed);
+ method R(a: SoWellformed, s: set<SoWellformed>) returns (c: bool, d: SoWellformed)
requires next != null && this !in s;
modifies s;
ensures next.xyz < 100; // fine
@@ -175,7 +175,7 @@ class StatementTwoShoes {
}
function G(w: int): int { 5 }
- function method H(x: int): int;
+ function method H(x: int): int
method V(s: set<StatementTwoShoes>, a: int, b: int)
modifies s;
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 53d3bf03..e56b4122 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -42,7 +42,7 @@ method Generic<T>(i: int, t0: T, t1: T) returns (r: T) {
r := t1;
}
-function method FenEric<T>(t0: T, t1: T): T;
+function method FenEric<T>(t0: T, t1: T): T
datatype Pair<T> = Pr(T, T);
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index d4d1dfcf..f31935af 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -87,7 +87,7 @@ class Termination {
}
}
- method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);
+ method Traverse<T>(a: List<T>) returns (val: T, b: List<T>)
requires a != List.Nil;
ensures a == List.Cons(val, b);
}
diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 2bedd37d..710e9838 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -88,7 +88,7 @@ method N() returns (k: MyClass)
k := new MyClass;
}
-function NF(): MyClass;
+function NF(): MyClass
function TakesADatatype(a: List): int { 12 }
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index a3698dc0..8f3f8b87 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -17,7 +17,7 @@ class C<U> {
assert kz && (G() || !G());
}
- function G<Y>(): Y;
+ function G<Y>(): Y
}
class SetTest {
@@ -99,7 +99,7 @@ class CClient {
// -------------------------
-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool;
+static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
requires c == c || c in people;
method FindCelebrity3(people: set<int>, ghost c: int)
@@ -110,7 +110,7 @@ method FindCelebrity3(people: set<int>, ghost c: int)
b := F(c, people);
}
-static function F(c: int, people: set<int>): bool;
+static function F(c: int, people: set<int>): bool
requires IsCelebrity(c, people);
function RogerThat<G>(g: G): G
@@ -153,8 +153,8 @@ method LoopyRoger(n: int)
class TyKn_C<T> {
var x: T;
- function G(): T;
- method M() returns (t: T);
+ function G(): T
+ method M() returns (t: T)
}
class TyKn_K {
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index 74512e01..21b895aa 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -1,6 +1,6 @@
// Celebrity example, inspired by the Rodin tutorial
-static function method Knows<Person>(a: Person, b: Person): bool;
+static function method Knows<Person>(a: Person, b: Person): bool
requires a != b; // forbid asking about the reflexive case
static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index fdce6dc7..39e14ea5 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -163,7 +163,7 @@ function mapF(xs: List): List
case Nil => Nil
case Cons(y, ys) => Cons(HardcodedUninterpretedFunction(y), mapF(ys))
}
-function HardcodedUninterpretedFunction(n: Nat): Nat;
+function HardcodedUninterpretedFunction(n: Nat): Nat
function takeWhileAlways(hardcodedResultOfP: Bool, xs: List): List
{
@@ -195,7 +195,7 @@ function filterP(xs: List): List
then Cons(y, filterP(ys))
else filterP(ys)
}
-function HardcodedUninterpretedPredicate(n: Nat): Bool;
+function HardcodedUninterpretedPredicate(n: Nat): Bool
function insort(n: Nat, xs: List): List
{
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index 189ff2b5..c8419890 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -29,7 +29,7 @@ class UltraFilter<G> {
}
// Dafny currently does not have a set comprehension expression, so this method stub will have to do
- method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>);
+ method H(f: set<set<G>>, S: set<G>, M: set<G>) returns (h: set<set<G>>)
ensures (forall X :: X in h <==> M + X in f);
method Lemma_HIsFilter(h: set<set<G>>, f: set<set<G>>, S: set<G>, M: set<G>)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 21:35:40 +0000