diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 149 |
1 files changed, 13 insertions, 136 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 15d39460..c0aae345 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -3,39 +3,29 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------*/
-
/*---------------------------------------------------------------------------
// Dafny
// Rustan Leino, first created 25 January 2008
//--------------------------------------------------------------------------*/
-
using System.Collections.Generic;
using System.Numerics;
using Microsoft.Boogie;
using System.IO;
using System.Text;
-
-
COMPILER Dafny
-
/*--------------------------------------------------------------------------*/
-
static List<ModuleDecl/*!*/> theModules;
static BuiltIns theBuiltIns;
-
-
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument("dummyAttrArg");
static int anonymousIds = 0;
-
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
public bool IsUnlimited;
}
-
// helper routine for parsing call statements
private static Expression/*!*/ ConvertToLocal(Expression/*!*/ e)
{
@@ -47,7 +37,6 @@ Contract.Ensures(Contract.Result<Expression>() != null); }
return e; // cannot convert to IdentifierExpr (or is already an IdentifierExpr)
}
-
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "modules".
@@ -68,7 +57,6 @@ public static int Parse (string/*!*/ filename, List<ModuleDecl/*!*/>/*!*/ module }
}
}
-
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "modules".
@@ -82,7 +70,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! Errors errors = new Errors();
return Parse(s, filename, modules, builtIns, errors);
}
-
///<summary>
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "modules".
@@ -108,7 +95,6 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*! theBuiltIns = oldBuiltIns;
return parser.errors.count;
}
-
/*--------------------------------------------------------------------------*/
CHARACTERS
letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
@@ -116,25 +102,20 @@ CHARACTERS posDigit = "123456789".
special = "'_?\\".
glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
-
cr = '\r'.
lf = '\n'.
tab = '\t'.
-
space = ' '.
quote = '"'.
-
nondigit = letter + special.
idchar = nondigit + digit.
nonquote = letter + digit + space + glyph.
-
/* exclude the characters in 'array' */
nondigitMinusA = nondigit - 'a'.
idcharMinusA = idchar - 'a'.
idcharMinusR = idchar - 'r'.
idcharMinusY = idchar - 'y'.
idcharMinusPosDigit = idchar - posDigit.
-
/*------------------------------------------------------------------------*/
TOKENS
ident = nondigitMinusA {idchar} /* if char 0 is not an 'a', then anything else is fine */
@@ -147,23 +128,16 @@ TOKENS digits = digit {digit}.
arrayToken = 'a' 'r' 'r' 'a' 'y' [posDigit {digit}].
string = quote {nonquote} quote.
-
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
-
IGNORE cr + lf + tab
-
-
/*------------------------------------------------------------------------*/
PRODUCTIONS
-
Dafny
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;
Attributes attrs; IToken/*!*/ id; List<string/*!*/> theImports;
-
List<MemberDecl/*!*/> membersDefaultClass = new List<MemberDecl/*!*/>();
ModuleDecl module;
-
// to support multiple files, create a default module only if theModules doesn't already contain one
DefaultModuleDecl defaultModule = null;
foreach (ModuleDecl mdecl in theModules) {
@@ -206,7 +180,6 @@ Dafny .)
EOF
.
-
ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
@@ -227,16 +200,15 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c> "{" (. bodyStart = t; .)
{ ClassMemberDecl<members, true>
}
- "}"
- (. if (optionalId == null)
+ "}"
+ (. if (optionalId == null)
c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);
- else
+ else
c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
.)
.
-
ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.>
= (. Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
@@ -247,13 +219,12 @@ ClassMemberDecl<.List<MemberDecl/*!*/>/*!*/ mm, bool allowConstructors.> | "static" (. mmod.IsStatic = true; .)
| "unlimited" (. mmod.IsUnlimited = true; .)
}
- ( FieldDecl<mmod, mm>
+ ( FieldDecl<mmod, mm>
| FunctionDecl<mmod, out f> (. mm.Add(f); .)
| MethodDecl<mmod, allowConstructors, out m> (. mm.Add(m); .)
- | CouplingInvDecl<mmod, mm>
+ | CouplingInvDecl<mmod, mm>
)
.
-
DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
@@ -276,7 +247,6 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt> dt.BodyEndTok = t;
.)
.
-
DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.>
= (. Contract.Requires(cce.NonNullElements(ctors));
Attributes attrs = null;
@@ -288,7 +258,6 @@ DatatypeMemberDecl<.List<DatatypeCtor/*!*/>/*!*/ ctors.> [ FormalsOptionalIds<formals> ]
(. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)
.
-
FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
@@ -304,7 +273,6 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.> }
";"
.
-
CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
@@ -317,17 +285,15 @@ CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.> if (mmod.IsStatic) { SemErr(t, "coupling invariants cannot be declared 'static'"); }
if (mmod.IsGhost) { SemErr(t, "coupling invariants cannot be declared 'ghost'"); }
.)
- { Attribute<ref attrs> }
+ { Attribute<ref attrs> }
Ident<out id> (. ids.Add(id); .)
{ "," Ident<out id> (. ids.Add(id); .)
}
- "by"
+ "by"
Expression<out e>
";"
- (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)
+ (. mm.Add(new CouplingInvariant(ids, e, attrs)); .)
.
-
-
GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>
/* isGhost always returns as false if allowGhostKeyword is false */
= (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
@@ -337,14 +303,12 @@ GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out boo ]
IdentType<out id, out ty>
.
-
IdentType<out IToken/*!*/ id, out Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
Ident<out id>
":"
Type<out ty>
.
-
LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
= (. IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
@@ -353,7 +317,6 @@ LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost> ]
(. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
.
-
IdentTypeOptional<out BoundVar/*!*/ var>
= (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
@@ -362,7 +325,6 @@ IdentTypeOptional<out BoundVar/*!*/ var> ]
(. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
.
-
TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ ty, out bool isGhost>
= (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
@@ -389,9 +351,7 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t }
.)
.
-
/*------------------------------------------------------------------------*/
-
GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
= (. Contract.Requires(cce.NonNullElements(typeArgs));
IToken/*!*/ id; .)
@@ -401,9 +361,7 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.> }
">"
.
-
/*------------------------------------------------------------------------*/
-
MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
IToken/*!*/ id;
@@ -447,11 +405,9 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m> [ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
Formals<false, !mmod.IsGhost, outs>
]
-
{ 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);
else if (isConstructor)
@@ -462,7 +418,6 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m> m.BodyEndTok = bodyEnd;
.)
.
-
MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
List<Expression/*!*/>/*!*/ decreases.>
= (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
@@ -480,8 +435,7 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/ | "decreases" DecreasesList<decreases, false> ";"
)
.
-
-Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
+Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; .)
"("
[
@@ -491,8 +445,7 @@ Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.> ]
")"
.
-
-FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
+FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; .)
"("
[
@@ -502,14 +455,11 @@ FormalsOptionalIds<.List<Formal/*!*/>/*!*/ formals.> ]
")"
.
-
/*------------------------------------------------------------------------*/
-
Type<out Type/*!*/ ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; .)
TypeAndToken<out tok, out ty>
.
-
TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List<Type/*!*/>/*!*/ gt;
@@ -523,7 +473,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty> }
ty = new SetType(gt[0]);
.)
-
| "seq" (. tok = t; gt = new List<Type/*!*/>(); .)
GenericInstantiation<gt> (. if (gt.Count != 1) {
SemErr("seq type expects exactly one type argument");
@@ -533,7 +482,6 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty> | ReferenceType<out tok, out ty>
)
.
-
ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
@@ -554,7 +502,6 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty> [ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
)
.
-
GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
= (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .)
"<"
@@ -563,9 +510,7 @@ GenericInstantiation<.List<Type/*!*/>/*!*/ gt.> }
">"
.
-
/*------------------------------------------------------------------------*/
-
FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
= (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
Attributes attrs = null;
@@ -588,7 +533,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> (. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute<ref attrs> }
- Ident<out id>
+ Ident<out id>
[ GenericParameters<typeArgs> ]
Formals<true, isFunctionMethod, formals>
":"
@@ -601,7 +546,6 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f> f.BodyEndTok = bodyEnd;
.)
.
-
FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>
= (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; .)
@@ -614,7 +558,6 @@ FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ r | "decreases" DecreasesList<decreases, false> ";"
)
.
-
PossiblyWildExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr; .)
@@ -625,7 +568,6 @@ PossiblyWildExpression<out Expression/*!*/ e> | Expression<out e>
)
.
-
PossiblyWildFrameExpression<out FrameExpression/*!*/ fe>
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; .)
/* A reads clause can list a wildcard, which allows the enclosing function to
@@ -638,7 +580,6 @@ PossiblyWildFrameExpression<out FrameExpression/*!*/ fe> | FrameExpression<out fe>
)
.
-
FrameExpression<out FrameExpression/*!*/ fe>
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; .)
Expression<out e>
@@ -646,16 +587,13 @@ FrameExpression<out FrameExpression/*!*/ fe> ]
(. fe = new FrameExpression(e, fieldName); .)
.
-
FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
"{" (. bodyStart = t; .)
Expression<out e>
"}" (. bodyEnd = t; .)
.
-
/*------------------------------------------------------------------------*/
-
BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd>
= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);
List<Statement/*!*/> body = new List<Statement/*!*/>();
@@ -666,13 +604,11 @@ BlockStmt<out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd> "}" (. bodyEnd = t;
block = new BlockStmt(bodyStart, body); .)
.
-
Stmt<.List<Statement/*!*/>/*!*/ ss.>
= (. Statement/*!*/ s;
.)
OneStmt<out s> (. ss.Add(s); .)
.
-
OneStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
@@ -702,7 +638,6 @@ OneStmt<out Statement/*!*/ s> | ReturnStmt<out s>
)
.
-
ReturnStmt<out Statement/*!*/ s>
= (.
IToken returnTok = null;
@@ -738,7 +673,6 @@ UpdateStmt<out Statement/*!*/ s> )
(. s = new UpdateStmt(x, lhss, rhss); .)
.
-
Rhs<out AssignmentRhs r, Expression receiverForInitCall>
= (. IToken/*!*/ x, newToken; Expression/*!*/ e;
List<Expression> ee = null;
@@ -766,17 +700,13 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall> r = new TypeRhs(newToken, ty, initCall);
}
.)
-
/* One day, the choose expression should be treated just as a special case of a method call. */
| "choose" (. x = t; .)
Expression<out e> (. r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e)); .)
-
| "*" (. r = new HavocRhs(t); .)
-
| Expression<out e> (. r = new ExprRhs(e); .)
)
.
-
VarDeclStatement<.out Statement/*!*/ s.>
= (. IToken x = null, assignTok = null; bool isGhost = false;
VarDecl/*!*/ d;
@@ -810,7 +740,6 @@ VarDeclStatement<.out Statement/*!*/ s.> s = new VarDeclStmt(x, lhss, update);
.)
.
-
IfStmt<out Statement/*!*/ ifStmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out ifStmt) != null); IToken/*!*/ x;
Expression guard;
@@ -836,7 +765,6 @@ IfStmt<out Statement/*!*/ ifStmt> (. ifStmt = new AlternativeStmt(x, alternatives); .)
)
.
-
AlternativeBlock<.out List<GuardedAlternative> alternatives.>
= (. alternatives = new List<GuardedAlternative>();
IToken x;
@@ -853,7 +781,6 @@ AlternativeBlock<.out List<GuardedAlternative> alternatives.> }
"}"
.
-
WhileStmt<out Statement/*!*/ stmt>
= (. Contract.Ensures(Contract.ValueAtReturn(out stmt) != null); IToken/*!*/ x;
Expression guard;
@@ -877,7 +804,6 @@ WhileStmt<out Statement/*!*/ stmt> (. stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); .)
)
.
-
LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
@@ -898,7 +824,6 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!* ] ";"
}
.
-
DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
= (. Expression/*!*/ e; .)
PossiblyWildExpression<out e> (. if (!allowWildcard && e is WildcardExpr) {
@@ -915,7 +840,6 @@ DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.> .)
}
.
-
Guard<out Expression e> /* null represents demonic-choice */
= (. Expression/*!*/ ee; e = null; .)
"("
@@ -924,7 +848,6 @@ Guard<out Expression e> /* null represents demonic-choice */ )
")"
.
-
MatchStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
@@ -937,7 +860,6 @@ MatchStmt<out Statement/*!*/ s> "}"
(. s = new MatchStmt(x, e, cases); .)
.
-
CaseStatement<out MatchCaseStmt/*!*/ c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ x, id, arg;
@@ -955,9 +877,7 @@ CaseStatement<out MatchCaseStmt/*!*/ c> { Stmt<body> }
(. c = new MatchCaseStmt(x, id.val, arguments, body); .)
.
-
/*------------------------------------------------------------------------*/
-
ForeachStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
IToken/*!*/ x, boundVar;
@@ -988,19 +908,16 @@ ForeachStmt<out Statement/*!*/ s> }
.)
.
-
AssertStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"assert" (. x = t; .)
Expression<out e> ";" (. s = new AssertStmt(x, e); .)
.
-
AssumeStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
"assume" (. x = t; .)
Expression<out e> ";" (. s = new AssumeStmt(x, e); .)
.
-
PrintStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
@@ -1011,13 +928,11 @@ PrintStmt<out Statement/*!*/ s> }
";" (. s = new PrintStmt(x, args); .)
.
-
/*------------------------------------------------------------------------*/
Expression<out Expression/*!*/ e>
=
EquivExpression<out e>
.
-
/*------------------------------------------------------------------------*/
EquivExpression<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
@@ -1026,9 +941,7 @@ EquivExpression<out Expression/*!*/ e0> ImpliesExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Iff, e0, e1); .)
}
.
-
EquivOp = "<==>" | '\u21d4'.
-
/*------------------------------------------------------------------------*/
ImpliesExpression<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
@@ -1037,9 +950,7 @@ ImpliesExpression<out Expression/*!*/ e0> ImpliesExpression<out e1> (. e0 = new BinaryExpr(x, BinaryExpr.Opcode.Imp, e0, e1); .)
]
.
-
ImpliesOp = "==>" | '\u21d2'.
-
/*------------------------------------------------------------------------*/
LogicalExpression<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; .)
@@ -1056,10 +967,8 @@ LogicalExpression<out Expression/*!*/ e0> }
]
.
-
AndOp = "&&" | '\u2227'.
OrOp = "||" | '\u2228'.
-
/*------------------------------------------------------------------------*/
RelationalExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
@@ -1143,7 +1052,6 @@ RelationalExpression<out Expression/*!*/ e> }
.)
.
-
RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .)
@@ -1160,7 +1068,6 @@ RelOp<out IToken/*!*/ x, out BinaryExpr.Opcode op> | '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .)
)
.
-
/*------------------------------------------------------------------------*/
Term<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; .)
@@ -1169,14 +1076,12 @@ Term<out Expression/*!*/ e0> Factor<out e1> (. e0 = new BinaryExpr(x, op, e0, e1); .)
}
.
-
AddOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryExpr.Opcode.Add/*(dummy)*/; .)
( "+" (. x = t; op = BinaryExpr.Opcode.Add; .)
| "-" (. x = t; op = BinaryExpr.Opcode.Sub; .)
)
.
-
/*------------------------------------------------------------------------*/
Factor<out Expression/*!*/ e0>
= (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op; .)
@@ -1185,7 +1090,6 @@ Factor<out Expression/*!*/ e0> UnaryExpression<out e1> (. e0 = new BinaryExpr(x, op, e0, e1); .)
}
.
-
MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/; .)
( "*" (. x = t; op = BinaryExpr.Opcode.Mul; .)
@@ -1193,7 +1097,6 @@ MulOp<out IToken/*!*/ x, out BinaryExpr.Opcode op> | "%" (. x = t; op = BinaryExpr.Opcode.Mod; .)
)
.
-
/*------------------------------------------------------------------------*/
UnaryExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; e = dummyExpr; .)
@@ -1209,7 +1112,6 @@ UnaryExpression<out Expression/*!*/ e> { Suffix<ref e> }
)
.
-
Lhs<out Expression e>
= (. e = null; // to please the compiler
.)
@@ -1220,9 +1122,7 @@ Lhs<out Expression e> { Suffix<ref e> }
)
.
-
NegOp = "!" | '\u00ac'.
-
/* A ConstAtomExpression is never an l-value. Also, a ConstAtomExpression is never followed by
* an open paren (but could very well have a suffix that starts with a period or a square bracket).
* (The "Also..." part may change if expressions in Dafny could yield functions.)
@@ -1251,7 +1151,6 @@ ConstAtomExpression<out Expression/*!*/ e> ")"
)
.
-
DisplayExpr<out Expression e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null);
IToken/*!*/ x; List<Expression/*!*/>/*!*/ elements;
@@ -1265,7 +1164,6 @@ DisplayExpr<out Expression e> "]"
)
.
-
EndlessExpression<out Expression e>
= (. IToken/*!*/ x;
Expression e0, e1;
@@ -1280,7 +1178,6 @@ EndlessExpression<out Expression e> | ComprehensionExpr<out e>
)
.
-
MatchExpression<out Expression/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
@@ -1294,7 +1191,6 @@ MatchExpression<out Expression/*!*/ e> }
(. e = new MatchExpr(x, e, cases); .)
.
-
CaseExpression<out MatchCaseExpr/*!*/ c>
= (. Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ x, id, arg;
List<BoundVar/*!*/> arguments = new List<BoundVar/*!*/>();
@@ -1310,9 +1206,7 @@ CaseExpression<out MatchCaseExpr/*!*/ c> "=>"
Expression<out body> (. c = new MatchCaseExpr(x, id.val, arguments, body); .)
.
-
/*------------------------------------------------------------------------*/
-
DottedIdentifiersAndFunction<out Expression e>
= (. IToken id; IToken openParen = null;
List<Expression> args = null;
@@ -1328,7 +1222,6 @@ DottedIdentifiersAndFunction<out Expression e> ]
(. e = new IdentifierSequence(idents, openParen, args); .)
.
-
Suffix<ref Expression/*!*/ e>
= (. Contract.Requires(e != null); Contract.Ensures(e!=null); IToken/*!*/ id, x; List<Expression/*!*/>/*!*/ args;
Expression e0 = null; Expression e1 = null; Expression/*!*/ ee; bool anyDots = false;
@@ -1341,7 +1234,6 @@ Suffix<ref Expression/*!*/ e> [ Expressions<args> ]
")" (. e = new FunctionCallExpr(id, id.val, e, args); .)
] (. if (!func) { e = new FieldSelectExpr(id, e, id.val); } .)
-
| "[" (. x = t; .)
( Expression<out ee> (. e0 = ee; .)
( ".." (. anyDots = true; .)
@@ -1384,9 +1276,7 @@ Suffix<ref Expression/*!*/ e> "]"
)
.
-
/*------------------------------------------------------------------------*/
-
QuantifierGuts<out Expression/*!*/ q>
= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null); IToken/*!*/ x = Token.NoToken;
bool univ = false;
@@ -1417,11 +1307,9 @@ QuantifierGuts<out Expression/*!*/ q> }
.)
.
-
Forall = "forall" | '\u2200'.
Exists = "exists" | '\u2203'.
QSep = "::" | '\u2022'.
-
ComprehensionExpr<out Expression/*!*/ q>
= (. Contract.Ensures(Contract.ValueAtReturn(out q) != null);
IToken/*!*/ x = Token.NoToken;
@@ -1444,22 +1332,18 @@ ComprehensionExpr<out Expression/*!*/ q> q = new SetComprehension(x, bvars, range, body);
.)
.
-
Expressions<.List<Expression/*!*/>/*!*/ args.>
= (. Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; .)
Expression<out e> (. args.Add(e); .)
{ "," Expression<out e> (. args.Add(e); .)
}
.
-
/*------------------------------------------------------------------------*/
-
Attribute<ref Attributes attrs>
= "{"
AttributeBody<ref attrs>
"}"
.
-
AttributeBody<ref Attributes attrs>
= (. string aName;
List<Attributes.Argument/*!*/> aArgs = new List<Attributes.Argument/*!*/>();
@@ -1471,14 +1355,12 @@ AttributeBody<ref Attributes attrs> }
] (. attrs = new Attributes(aName, aArgs, attrs); .)
.
-
AttributeArg<out Attributes.Argument/*!*/ arg>
= (. Contract.Ensures(Contract.ValueAtReturn(out arg) != null); Expression/*!*/ e; arg = dummyAttrArg; .)
( string (. arg = new Attributes.Argument(t.val.Substring(1, t.val.Length-2)); .)
| Expression<out e> (. arg = new Attributes.Argument(e); .)
)
.
-
AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs>
= (. List<Expression/*!*/> es = new List<Expression/*!*/>();
.)
@@ -1489,21 +1371,17 @@ AttributeOrTrigger<ref Attributes attrs, ref Triggers trigs> )
"}"
.
-
/*------------------------------------------------------------------------*/
-
Idents<.List<string/*!*/>/*!*/ ids.>
= (. IToken/*!*/ id; .)
Ident<out id> (. ids.Add(id.val); .)
{ "," Ident<out id> (. ids.Add(id.val); .)
}
.
-
Ident<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
ident (. x = t; .)
.
-
Nat<out BigInteger n>
=
digits
@@ -1513,7 +1391,6 @@ Nat<out BigInteger n> SemErr("incorrectly formatted number");
n = BigInteger.Zero;
}
- .)
+ .)
.
-
-END Dafny.
\ No newline at end of file +END Dafny.
|