/*-----------------------------------------------------------------------------
//
// 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
/*--------------------------------------------------------------------------*/
readonly Expression/*!*/ dummyExpr;
readonly AssignmentRhs/*!*/ dummyRhs;
readonly FrameExpression/*!*/ dummyFrameExpr;
readonly Statement/*!*/ dummyStmt;
readonly ModuleDecl theModule;
readonly BuiltIns theBuiltIns;
readonly bool theVerifyThisFile;
int anonymousIds = 0;
struct MemberModifiers {
public bool IsGhost;
public bool IsStatic;
public bool IsProtected;
}
///
/// Parses top-level things (modules, classes, datatypes, class members) from "filename"
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///
public static int Parse (string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, Errors/*!*/ errors, bool verifyThisFile=true) /* throws System.IO.IOException */ {
Contract.Requires(filename != null);
Contract.Requires(module != null);
string s;
if (filename == "stdin.dfy") {
s = Microsoft.Boogie.ParserHelper.Fill(System.Console.In, new List());
return Parse(s, filename, module, builtIns, errors, verifyThisFile);
} else {
using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
s = Microsoft.Boogie.ParserHelper.Fill(reader, new List());
return Parse(s, DafnyOptions.Clo.UseBaseNameForFileName ? Path.GetFileName(filename) : filename, module, builtIns, errors, verifyThisFile);
}
}
}
///
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner.
///
public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(module != null);
Errors errors = new Errors();
return Parse(s, filename, module, builtIns, errors, verifyThisFile);
}
///
/// Parses top-level things (modules, classes, datatypes, class members)
/// and appends them in appropriate form to "module".
/// Returns the number of parsing errors encountered.
/// Note: first initialize the Scanner with the given Errors sink.
///
public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, BuiltIns builtIns,
Errors/*!*/ errors, bool verifyThisFile=true) {
Contract.Requires(s != null);
Contract.Requires(filename != null);
Contract.Requires(module != null);
Contract.Requires(errors != null);
byte[]/*!*/ buffer = cce.NonNull( UTF8Encoding.Default.GetBytes(s));
MemoryStream ms = new MemoryStream(buffer,false);
Scanner scanner = new Scanner(ms, errors, filename);
Parser parser = new Parser(scanner, errors, module, builtIns, verifyThisFile);
parser.Parse();
return parser.errors.count;
}
public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, ModuleDecl module, BuiltIns builtIns, bool verifyThisFile=true)
: this(scanner, errors) // the real work
{
// initialize readonly fields
dummyExpr = new LiteralExpr(Token.NoToken);
dummyRhs = new ExprRhs(dummyExpr, null);
dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
dummyStmt = new ReturnStmt(Token.NoToken, Token.NoToken, null);
theModule = module;
theBuiltIns = builtIns;
theVerifyThisFile = verifyThisFile;
}
bool IsAttribute() {
Token x = scanner.Peek();
return la.kind == _lbrace && x.kind == _colon;
}
bool IsAlternative() {
Token x = scanner.Peek();
return la.kind == _lbrace && x.kind == _case;
}
bool IsLoopSpec() {
return la.kind == _invariant | la.kind == _decreases | la.kind == _modifies;
}
bool IsFunctionDecl() {
switch (la.kind) {
case _function:
case _predicate:
case _copredicate:
return true;
case _inductive:
return scanner.Peek().kind != _lemma;
default:
return false;
}
}
bool IsParenStar() {
scanner.ResetPeek();
Token x = scanner.Peek();
return la.kind == _openparen && x.kind == _star;
}
bool IsEquivOp() {
return la.val == "<==>" || la.val == "\u21d4";
}
bool IsImpliesOp() {
return la.val == "==>" || la.val == "\u21d2";
}
bool IsExpliesOp() {
return la.val == "<==" || la.val == "\u21d0";
}
bool IsAndOp() {
return la.val == "&&" || la.val == "\u2227";
}
bool IsOrOp() {
return la.val == "||" || la.val == "\u2228";
}
bool IsRelOp() {
return la.val == "=="
|| la.val == "<"
|| la.val == ">"
|| la.val == "<="
|| la.val == ">="
|| la.val == "!="
|| la.val == "in"
|| la.kind == _notIn
|| la.val =="!"
|| la.val == "\u2260"
|| la.val == "\u2264"
|| la.val == "\u2265";
}
bool IsAddOp() {
return la.val == "+" || la.val == "-";
}
bool IsMulOp() {
return la.kind == _star || la.val == "/" || la.val == "%";
}
bool IsQSep() {
return la.kind == _doublecolon || la.kind == _bullet;
}
bool IsNonFinalColon() {
return la.kind == _colon && scanner.Peek().kind != _rbracket;
}
bool IsMapDisplay() {
return la.kind == _map && scanner.Peek().kind == _lbracket;
}
bool IsIMapDisplay() {
return la.kind == _imap && scanner.Peek().kind == _lbracket;
}
bool IsISetDisplay() {
return la.kind == _iset && scanner.Peek().kind == _lbrace;
}
bool IsSuffix() {
return la.kind == _dot || la.kind == _lbracket || la.kind == _openparen;
}
string UnwildIdent(string x, bool allowWildcardId) {
if (x.StartsWith("_")) {
if (allowWildcardId && x.Length == 1) {
return "_v" + anonymousIds++;
} else {
SemErr("cannot declare identifier beginning with underscore");
}
}
return x;
}
bool IsLambda(bool allowLambda)
{
if (!allowLambda) {
return false;
}
scanner.ResetPeek();
Token x;
// peek at what might be a signature of a lambda expression
if (la.kind == _ident) {
// cool, that's the entire candidate signature
} else if (la.kind != _openparen) {
return false; // this is not a lambda expression
} else {
int identCount = 0;
x = scanner.Peek();
while (x.kind != _closeparen) {
if (identCount != 0) {
if (x.kind != _comma) {
return false; // not the signature of a lambda
}
x = scanner.Peek();
}
if (x.kind != _ident) {
return false; // not a lambda expression
}
identCount++;
x = scanner.Peek();
if (x.kind == _colon) {
// a colon belongs only in a lamdba signature, so this must be a lambda (or something ill-formed)
return true;
}
}
}
// What we have seen so far could have been a lambda signature or could have been some
// other expression (in particular, an identifier, a parenthesized identifier, or a
// tuple all of whose subexpressions are identifiers).
// It is a lambda expression if what follows is something that must be a lambda.
x = scanner.Peek();
return x.kind == _darrow || x.kind == _arrow || x.kind == _reads || x.kind == _requires;
}
bool IsIdentParen() {
Token x = scanner.Peek();
return la.kind == _ident && x.kind == _openparen;
}
bool IsIdentColonOrBar() {
Token x = scanner.Peek();
return la.kind == _ident && (x.kind == _colon || x.kind == _verticalbar);
}
bool SemiFollowsCall(bool allowSemi, Expression e) {
return allowSemi && la.kind == _semi && e is ApplySuffix;
}
bool CloseOptionalBrace(bool usesOptionalBrace) {
return usesOptionalBrace && la.kind == _rbrace;
}
bool IsNotEndOfCase() {
return la.kind != _EOF && la.kind != _rbrace && la.kind != _case;
}
/* The following is the largest lookahead there is. It needs to check if what follows
* can be nothing but "<" Type { "," Type } ">".
*/
bool IsGenericInstantiation() {
scanner.ResetPeek();
IToken pt = la;
if (!IsTypeList(ref pt)) {
return false;
}
/* There are ambiguities in the parsing. For example:
* F( a < b , c > (d) )
* can either be a unary function F whose argument is a function "a" with type arguments "" and
* parameter "d", or can be a binary function F with the two boolean arguments "a < b" and "c > (d)".
* To make the situation a little better, we (somewhat heuristically) look at the character that
* follows the ">". Note that if we, contrary to a user's intentions, pick "a" out as a function
* with a type instantiation, the user can disambiguate it by making sure the ">" sits inside some
* parentheses, like:
* F( a < b , (c > (d)) )
*/
switch (pt.kind) {
case _dot: // here, we're sure it must have been a type instantiation we saw, because an expression cannot begin with dot
case _openparen: // it was probably a type instantiation of a function/method
case _lbracket: // it is possible that it was a type instantiation
case _lbrace: // it was probably a type instantiation of a function/method
// In the following cases, we're sure we must have read a type instantiation that just ended an expression
case _closeparen:
case _rbracket:
case _rbrace:
case _semi:
case _then:
case _else:
case _case:
case _eq:
case _neq:
case _neqAlt:
case _openAngleBracket:
case _closeAngleBracket:
return true;
default:
return false;
}
}
bool IsTypeList(ref IToken pt) {
if (pt.kind != _openAngleBracket) {
return false;
}
pt = scanner.Peek();
return IsTypeSequence(ref pt, _closeAngleBracket);
}
bool IsTypeSequence(ref IToken pt, int endBracketKind) {
while (true) {
if (!IsType(ref pt)) {
return false;
}
if (pt.kind == endBracketKind) {
// end of type list
pt = scanner.Peek();
return true;
} else if (pt.kind == _comma) {
// type list continues
pt = scanner.Peek();
} else {
// not a type list
return false;
}
}
}
bool IsType(ref IToken pt) {
switch (pt.kind) {
case _bool:
case _char:
case _nat:
case _int:
case _real:
case _object:
case _string:
pt = scanner.Peek();
return true;
case _arrayToken:
case _set:
case _iset:
case _multiset:
case _seq:
case _map:
case _imap:
pt = scanner.Peek();
return IsTypeList(ref pt);
case _ident:
while (true) {
// invariant: next token is an ident
pt = scanner.Peek();
if (pt.kind == _openAngleBracket && !IsTypeList(ref pt)) {
return false;
}
if (pt.kind != _dot) {
// end of the type
return true;
}
pt = scanner.Peek(); // get the _dot
if (pt.kind != _ident) {
return false;
}
}
case _openparen:
pt = scanner.Peek();
return IsTypeSequence(ref pt, _closeparen);
default:
return false;
}
}
/*--------------------------------------------------------------------------*/
CHARACTERS
letter = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz".
digit = "0123456789".
posDigit = "123456789".
hexdigit = "0123456789ABCDEFabcdef".
special = "'_?".
glyph = "`~!@#$%^&*()-_=+[{]}|;:',<.>/?\\".
cr = '\r'.
lf = '\n'.
tab = '\t'.
space = ' '.
nondigit = letter + special.
idchar = nondigit + digit.
nonidchar = ANY - idchar.
/* exclude the characters in 'array' and '\'' */
nondigitMinusATick = nondigit - 'a' - '\''.
idcharMinusA = idchar - 'a'.
idcharMinusR = idchar - 'r'.
idcharMinusY = idchar - 'y'.
idcharMinusPosDigit = idchar - posDigit.
idcharMinusTick = idchar - '\''.
/* string literals */
charChar = ANY - '\'' - '\\' - cr - lf.
stringChar = ANY - '"' - '\\' - cr - lf.
verbatimStringChar = ANY - '"'.
/*------------------------------------------------------------------------*/
TOKENS
ident = nondigitMinusATick {idchar} /* if char 0 is not an 'a' or '\'', then anything else is fine */
| 'a' [ idcharMinusR {idchar} ] /* if char 0 is an 'a', then either there is no char 1 or char 1 is not an 'r' */
| 'a' 'r' [ idcharMinusR {idchar} ] /* etc. */
| 'a' 'r' 'r' [ idcharMinusA {idchar} ]
| 'a' 'r' 'r' 'a' [ idcharMinusY {idchar} ]
| 'a' 'r' 'r' 'a' 'y' idcharMinusPosDigit {idchar}
| 'a' 'r' 'r' 'a' 'y' posDigit {idchar} nondigit {idchar}
| "'" [ idchar ] /* if char 0 is a '\'' and length is 1 or 2, then it is an identifier */
| "'" idchar idcharMinusTick /* if char 0 is '\'' and length is 3, then it is an identifier provided char 2 is not '\'' */
| "'" idchar idchar idchar { idchar } /* if char 0 is '\'' and length exceeds 3, then it is an identifier */
.
digits = digit {['_'] digit}.
hexdigits = "0x" hexdigit {['_'] hexdigit}.
decimaldigits = digit {['_'] digit} '.' digit {['_'] digit}.
arrayToken = "array" [posDigit {digit}].
bool = "bool".
char = "char".
int = "int".
nat = "nat".
real = "real".
object = "object".
string = "string".
set = "set".
iset = "iset".
multiset = "multiset".
seq = "seq".
map = "map".
imap = "imap".
charToken =
"'"
( charChar
| "\\\'" | "\\\"" | "\\\\" | "\\0" | "\\n" | "\\r" | "\\t"
| "\\u" hexdigit hexdigit hexdigit hexdigit
)
"'".
stringToken =
'"'
{ stringChar
| "\\\'" | "\\\"" | "\\\\" | "\\0" | "\\n" | "\\r" | "\\t"
| "\\u" hexdigit hexdigit hexdigit hexdigit
}
'"'
| '@' '"' { verbatimStringChar | "\"\"" } '"'.
colon = ':'.
comma = ','.
verticalbar = '|'.
doublecolon = "::".
bullet = '\u2022'.
dot = '.'.
semi = ';'.
darrow = "=>".
arrow = "->".
assume = "assume".
calc = "calc".
case = "case".
then = "then".
else = "else".
decreases = "decreases".
invariant = "invariant".
function = "function".
predicate = "predicate".
inductive = "inductive".
lemma = "lemma".
copredicate = "copredicate".
modifies = "modifies".
reads = "reads".
requires = "requires".
lbrace = '{'.
rbrace = '}'.
lbracket = '['.
rbracket = ']'.
openparen = '('.
closeparen = ')'.
openAngleBracket = '<'.
closeAngleBracket = '>'.
eq = "==".
neq = "!=".
neqAlt = '\u2260'.
star = '*'.
notIn = "!in" CONTEXT (nonidchar).
ellipsis = "...".
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
IGNORE cr + lf + tab
/*------------------------------------------------------------------------*/
PRODUCTIONS
Dafny
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;
List membersDefaultClass = new List();
ModuleDecl submodule;
// to support multiple files, create a default module only if theModule is null
DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef;
// theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl)
TraitDecl/*!*/ trait;
Contract.Assert(defaultModule != null);
.)
{ "include" stringToken (. {
string parsedFile = t.filename;
bool isVerbatimString;
string includedFile = Util.RemoveParsedStringQuotes(t.val, out isVerbatimString);
includedFile = Util.RemoveEscaping(includedFile, isVerbatimString);
string fullPath = includedFile;
if (!Path.IsPathRooted(includedFile)) {
string basePath = Path.GetDirectoryName(parsedFile);
includedFile = Path.Combine(basePath, includedFile);
fullPath = Path.GetFullPath(includedFile);
}
defaultModule.Includes.Add(new Include(t, includedFile, fullPath));
}
.)
}
{ SubModuleDecl (. defaultModule.TopLevelDecls.Add(submodule); .)
| ClassDecl (. defaultModule.TopLevelDecls.Add(c); .)
| DatatypeDecl (. defaultModule.TopLevelDecls.Add(dt); .)
| NewtypeDecl (. defaultModule.TopLevelDecls.Add(td); .)
| OtherTypeDecl (. defaultModule.TopLevelDecls.Add(td); .)
| IteratorDecl (. defaultModule.TopLevelDecls.Add(iter); .)
| TraitDecl (. defaultModule.TopLevelDecls.Add(trait); .)
| ClassMemberDecl
}
(. // find the default class in the default module, then append membersDefaultClass to its member list
DefaultClassDecl defaultClass = null;
foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {
defaultClass = topleveldecl as DefaultClassDecl;
if (defaultClass != null) {
defaultClass.Members.AddRange(membersDefaultClass);
break;
}
}
if (defaultClass == null) { // create the default class here, because it wasn't found
defaultClass = new DefaultClassDecl(defaultModule, membersDefaultClass);
defaultModule.TopLevelDecls.Add(defaultClass);
} .)
EOF
.
SubModuleDecl
= (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; TopLevelDecl td; IteratorDecl iter;
Attributes attrs = null; IToken/*!*/ id;
TraitDecl/*!*/ trait;
List namedModuleDefaultClassMembers = new List();;
List idRefined = null, idPath = null, idAssignment = null;
ModuleDefinition module;
ModuleDecl sm;
submodule = null; // appease compiler
bool isAbstract = false;
bool opened = false;
.)
( [ "abstract" (. isAbstract = true; .) ]
"module"
{ Attribute[ }
NoUSIdent
[ "refines" QualifiedModuleName ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); .)
"{" (. module.BodyStartTok = t; .)
{ SubModuleDecl (. module.TopLevelDecls.Add(sm); .)
| ClassDecl (. module.TopLevelDecls.Add(c); .)
| TraitDecl (. module.TopLevelDecls.Add(trait); .)
| DatatypeDecl (. module.TopLevelDecls.Add(dt); .)
| NewtypeDecl (. module.TopLevelDecls.Add(td); .)
| OtherTypeDecl (. module.TopLevelDecls.Add(td); .)
| IteratorDecl (. module.TopLevelDecls.Add(iter); .)
| ClassMemberDecl
}
"}" (. module.BodyEndTok = t;
module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers));
submodule = new LiteralModuleDecl(module, parent); .)
|
"import" ["opened" (.opened = true;.)]
NoUSIdent
[ "=" QualifiedModuleName
(. submodule = new AliasModuleDecl(idPath, id, parent, opened); .)
| "as" QualifiedModuleName ["default" QualifiedModuleName ]
(. submodule = new ModuleFacadeDecl(idPath, id, parent, idAssignment, opened); .)
]
[ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in the next big version of Dafny, don't allow the semi-colon at all.
(. errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
]
(. if (submodule == null) {
idPath = new List();
idPath.Add(id);
submodule = new AliasModuleDecl(idPath, id, parent, opened);
}
.)
)
.
/* This production is used to parse module names, where it is known that it is a module name that is expected. */
QualifiedModuleName<.out List ids.>
= (. IToken id; ids = new List(); .)
Ident (. ids.Add(id); .)
{ "." Ident (. ids.Add(id); .)
}
.
ClassDecl
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
Type trait = null;
List/*!*/ traits = new List();
Attributes attrs = null;
List typeArgs = new List();
List members = new List();
IToken bodyStart;
.)
SYNC
"class"
{ Attribute][ }
NoUSIdent
[ GenericParameters ]
["extends"
Type (. traits.Add(trait); .)
{"," Type (. traits.Add(trait); .) }
]
"{" (. bodyStart = t; .)
{ ClassMemberDecl
}
"}"
(. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traits);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
.)
.
TraitDecl
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out trait) != null);
IToken/*!*/ id;
Attributes attrs = null;
List typeArgs = new List(); //traits should not support type parameters at the moment
List members = new List();
IToken bodyStart;
.)
SYNC
"trait"
{ Attribute][ }
NoUSIdent
[ GenericParameters ]
"{" (. bodyStart = t; .)
{ ClassMemberDecl
}
"}"
(. trait = new TraitDecl(id, id.val, module, typeArgs, members, attrs);
trait.BodyStartTok = bodyStart;
trait.BodyEndTok = t;
.)
.
ClassMemberDecl<.List mm, bool allowConstructors, bool moduleLevelDecl.>
= (. Contract.Requires(cce.NonNullElements(mm));
Method/*!*/ m;
Function/*!*/ f;
MemberModifiers mmod = new MemberModifiers();
IToken staticToken = null, protectedToken = null;
.)
{ "ghost" (. mmod.IsGhost = true; .)
| "static" (. mmod.IsStatic = true; staticToken = t; .)
| "protected" (. mmod.IsProtected = true; protectedToken = t; .)
}
( (. if (moduleLevelDecl) {
SemErr(la, "fields are not allowed to be declared at the module level; instead, wrap the field in a 'class' declaration");
mmod.IsStatic = false;
mmod.IsProtected = false;
}
.)
FieldDecl
| IF(IsFunctionDecl())
(. if (moduleLevelDecl && staticToken != null) {
errors.Warning(staticToken, "module-level functions are always non-instance, so the 'static' keyword is not allowed here");
mmod.IsStatic = false;
}
.)
FunctionDecl (. mm.Add(f); .)
| (. if (moduleLevelDecl && staticToken != null) {
errors.Warning(staticToken, "module-level methods are always non-instance, so the 'static' keyword is not allowed here");
mmod.IsStatic = false;
}
if (protectedToken != null) {
SemErr(protectedToken, "only functions, not methods, can be declared 'protected'");
mmod.IsProtected = false;
}
.)
MethodDecl (. mm.Add(m); .)
)
.
DatatypeDecl
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out dt)!=null);
IToken/*!*/ id;
Attributes attrs = null;
List typeArgs = new List();
List ctors = new List();
IToken bodyStart = Token.NoToken; // dummy assignment
bool co = false;
.)
SYNC
( "datatype"
| "codatatype" (. co = true; .)
)
{ Attribute][ }
NoUSIdent
[ GenericParameters ]
"=" (. bodyStart = t; .)
DatatypeMemberDecl
{ "|" DatatypeMemberDecl }
[ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in the next big version of Dafny, don't allow the semi-colon at all.
(. errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
]
(. if (co) {
dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
} else {
dt = new IndDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);
}
dt.BodyStartTok = bodyStart;
dt.BodyEndTok = t;
.)
.
DatatypeMemberDecl<.List/*!*/ ctors.>
= (. Contract.Requires(cce.NonNullElements(ctors));
Attributes attrs = null;
IToken/*!*/ id;
List formals = new List();
.)
{ Attribute][ }
NoUSIdent
[ FormalsOptionalIds ]
(. ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); .)
.
FieldDecl<.MemberModifiers mmod, List/*!*/ mm.>
= (. Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
.)
SYNC
"var"
(. if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
.)
{ Attribute][ }
FIdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
{ "," FIdentType (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
}
OldSemi
.
NewtypeDecl
= (. IToken id, bvId;
Attributes attrs = null;
td = null;
Type baseType = null;
Expression wh;
.)
"newtype"
{ Attribute][ }
NoUSIdent
"="
( IF(IsIdentColonOrBar())
NoUSIdent
[ ":" Type ] (. if (baseType == null) { baseType = new OperationTypeProxy(true, true, false, false, false, false); } .)
"|"
Expression (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, new BoundVar(bvId, bvId.val, baseType), wh, attrs); .)
| Type (. td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); .)
)
.
OtherTypeDecl
= (. IToken id;
Attributes attrs = null;
var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
var typeArgs = new List();
td = null;
Type ty;
.)
"type"
{ Attribute][ }
NoUSIdent
( "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
[ GenericParameters ]
|
[ GenericParameters ]
[ "="
Type (. td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); .)
]
) (. if (td == null) {
td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
}
.)
[ SYNC ";"
// This semi-colon used to be required, but it seems silly to have it.
// To stage the transition toward not having it at all, let's make it optional for now. Then,
// in the next big version of Dafny, don't allow the semi-colon at all.
(. errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); .)
]
.
GIdentType
/* isGhost always returns as false if allowGhostKeyword is false */
= (. Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
isGhost = false; .)
[ "ghost" (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
]
IdentType
.
FIdentType
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
id = Token.NoToken;
.)
( WildIdent
| digits (. id = t; .)
)
":"
Type
.
IdentType
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
WildIdent
":"
Type
.
LocalIdentTypeOptional
= (. IToken id; Type ty; Type optType = null;
.)
WildIdent
[ ":" Type (. optType = ty; .)
]
(. var = new LocalVariable(id, id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
.
IdentTypeOptional
= (. Contract.Ensures(Contract.ValueAtReturn(out var) != null);
IToken id; Type ty; Type optType = null;
.)
WildIdent
[ ":" Type (. optType = ty; .)
]
(. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
.
TypeIdentOptional
= (.Contract.Ensures(Contract.ValueAtReturn(out id)!=null);
Contract.Ensures(Contract.ValueAtReturn(out ty)!=null);
Contract.Ensures(Contract.ValueAtReturn(out identName)!=null);
string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false; .)
[ "ghost" (. isGhost = true; .)
]
( TypeAndToken
[ ":"
(. /* try to convert ty to an identifier */
UserDefinedType udt = ty as UserDefinedType;
if (udt != null && udt.TypeArgs.Count == 0) {
name = udt.Name;
} else {
SemErr(id, "invalid formal-parameter name in datatype constructor");
}
.)
Type
]
| digits (. id = t; name = id.val;.)
":"
Type
)
(. if (name != null) {
identName = name;
} else {
identName = "#" + anonymousIds++;
}
.)
.
/*------------------------------------------------------------------------*/
IteratorDecl
= (. Contract.Ensures(Contract.ValueAtReturn(out iter) != null);
IToken/*!*/ id;
Attributes attrs = null;
List/*!*/ typeArgs = new List();
List ins = new List();
List outs = new List();
List reads = new List();
List mod = new List();
List decreases = new List();
List req = new List();
List ens = new List();
List yieldReq = new List();
List yieldEns = new List();
List dec = new List();
Attributes readsAttrs = null;
Attributes modAttrs = null;
Attributes decrAttrs = null;
BlockStmt body = null;
IToken signatureEllipsis = null;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
SYNC
"iterator"
{ Attribute][ }
NoUSIdent
(
[ GenericParameters ]
Formals
[ ( "yields"
| "returns" (. SemErr(t, "iterators don't have a 'returns' clause; did you mean 'yields'?"); .)
)
Formals
]
| "..." (. signatureEllipsis = t; .)
)
{ IteratorSpec }
[ BlockStmt
]
(. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
new Specification(reads, readsAttrs),
new Specification(mod, modAttrs),
new Specification(decreases, decrAttrs),
req, ens, yieldReq, yieldEns,
body, attrs, signatureEllipsis);
iter.BodyStartTok = bodyStart;
iter.BodyEndTok = bodyEnd;
.)
.
/*------------------------------------------------------------------------*/
GenericParameters<.List/*!*/ typeArgs.>
= (. Contract.Requires(cce.NonNullElements(typeArgs));
IToken/*!*/ id;
TypeParameter.EqualitySupportValue eqSupport;
.)
"<"
NoUSIdent (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
{ "," NoUSIdent (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
}
">"
.
/*------------------------------------------------------------------------*/
MethodDecl
= (. Contract.Ensures(Contract.ValueAtReturn(out m) !=null);
IToken/*!*/ id = Token.NoToken;
bool hasName = false; IToken keywordToken;
Attributes attrs = null;
List/*!*/ typeArgs = new List();
List ins = new List();
List outs = new List();
List req = new List();
List mod = new List();
List ens = new List();
List dec = new List();
Attributes decAttrs = null;
Attributes modAttrs = null;
BlockStmt body = null;
bool isLemma = false;
bool isConstructor = false;
bool isIndLemma = false;
bool isCoLemma = false;
IToken signatureEllipsis = null;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
.)
SYNC
( "method"
| "lemma" (. isLemma = true; .)
| "colemma" (. isCoLemma = true; .)
| "comethod" (. isCoLemma = true;
errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'");
.)
| "inductive" "lemma" (. isIndLemma = true; .)
| "constructor" (. if (allowConstructor) {
isConstructor = true;
} else {
SemErr(t, "constructors are allowed only in classes");
}
.)
) (. keywordToken = t; .)
(. if (isLemma) {
if (mmod.IsGhost) {
SemErr(t, "lemmas cannot be declared 'ghost' (they are automatically 'ghost')");
}
} else if (isConstructor) {
if (mmod.IsGhost) {
SemErr(t, "constructors cannot be declared 'ghost'");
}
if (mmod.IsStatic) {
SemErr(t, "constructors cannot be declared 'static'");
}
} else if (isIndLemma) {
if (mmod.IsGhost) {
SemErr(t, "inductive lemmas cannot be declared 'ghost' (they are automatically 'ghost')");
}
} else if (isCoLemma) {
if (mmod.IsGhost) {
SemErr(t, "colemmas cannot be declared 'ghost' (they are automatically 'ghost')");
}
}
.)
{ Attribute][ }
[ NoUSIdent (. hasName = true; .)
]
(. if (!hasName) {
id = keywordToken;
if (!isConstructor) {
SemErr(la, "a method must be given a name (expecting identifier)");
}
}
.)
(
[ GenericParameters ]
Formals
[ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .)
Formals
]
| "..." (. signatureEllipsis = t; .)
)
{ MethodSpec }
[ BlockStmt
]
(.
if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported") && !Attributes.Contains(attrs, "decl") && theVerifyThisFile) {
SemErr(t, "a method with an ensures clause must have a body, unless given the :axiom attribute");
}
IToken tok = theVerifyThisFile ? id : new IncludeToken(id);
if (isConstructor) {
m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis);
} else if (isIndLemma) {
m = new InductiveLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis);
} else if (isCoLemma) {
m = new CoLemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis);
} else if (isLemma) {
m = new Lemma(tok, id.val, mmod.IsStatic, typeArgs, ins, outs,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis);
} else {
m = new Method(tok, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs,
req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), body, attrs, signatureEllipsis);
}
m.BodyStartTok = bodyStart;
m.BodyEndTok = bodyEnd;
.)
.
MethodSpec<.List/*!*/ req, List/*!*/ mod, List/*!*/ ens,
List/*!*/ decreases, ref Attributes decAttrs, ref Attributes modAttrs.>
= (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null;
.)
SYNC
( "modifies" { IF(IsAttribute()) Attribute][ }
FrameExpression (. mod.Add(fe); .)
{ "," FrameExpression (. mod.Add(fe); .)
}
OldSemi
| [ "free" (. isFree = true;
errors.Warning(t, "the 'free' keyword is soon to be deprecated");
.)
]
( "requires" Expression OldSemi (. req.Add(new MaybeFreeExpression(e, isFree)); .)
| "ensures"
{ IF(IsAttribute()) Attribute][ }
Expression OldSemi (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)
)
| "decreases" { IF(IsAttribute()) Attribute][ } DecreasesList OldSemi
)
.
IteratorSpec<.List/*!*/ reads, List/*!*/ mod, List decreases,
List/*!*/ req, List/*!*/ ens,
List/*!*/ yieldReq, List/*!*/ yieldEns,
ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs.>
= (. Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
.)
SYNC
( "reads" { IF(IsAttribute()) Attribute][ }
FrameExpression (. reads.Add(fe); .)
{ "," FrameExpression (. reads.Add(fe); .)
}
OldSemi
| "modifies" { IF(IsAttribute()) Attribute][ }
FrameExpression (. mod.Add(fe); .)
{ "," FrameExpression (. mod.Add(fe); .)
}
OldSemi
| [ "free" (. isFree = true;
errors.Warning(t, "the 'free' keyword is soon to be deprecated");
.)
]
[ "yield" (. isYield = true; .)
]
( "requires" Expression OldSemi (. if (isYield) {
yieldReq.Add(new MaybeFreeExpression(e, isFree));
} else {
req.Add(new MaybeFreeExpression(e, isFree));
}
.)
| "ensures" { IF(IsAttribute()) Attribute][ }
Expression OldSemi (. if (isYield) {
yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
} else {
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
}
.)
)
| "decreases" { IF(IsAttribute()) Attribute][ } DecreasesList OldSemi
)
.
Formals<.bool incoming, bool allowGhostKeyword, List formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken id; Type ty; bool isGhost; .)
"("
[
GIdentType (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
{ "," GIdentType (. formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); .)
}
]
")"
.
FormalsOptionalIds<.List/*!*/ formals.>
= (. Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; .)
"("
[
TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)
{ "," TypeIdentOptional (. formals.Add(new Formal(id, name, ty, true, isGhost)); .)
}
]
")"
.
/*------------------------------------------------------------------------*/
Type
= (. Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; .)
TypeAndToken
.
TypeAndToken
= (. Contract.Ensures(Contract.ValueAtReturn(out tok)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
List gt; List tupleArgTypes = null;
.)
( "bool" (. tok = t; .)
| "char" (. tok = t; ty = new CharType(); .)
| "nat" (. tok = t; ty = new NatType(); .)
| "int" (. tok = t; ty = new IntType(); .)
| "real" (. tok = t; ty = new RealType(); .)
| "object" (. tok = t; ty = new ObjectType(); .)
| "set" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count > 1) {
SemErr("set type expects only one type argument");
}
ty = new SetType(true, gt.Count == 1 ? gt[0] : null);
.)
| "iset" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count > 1) {
SemErr("set type expects only one type argument");
}
ty = new SetType(false, gt.Count == 1 ? gt[0] : null);
.)
| "multiset" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count > 1) {
SemErr("multiset type expects only one type argument");
}
ty = new MultiSetType(gt.Count == 1 ? gt[0] : null);
.)
| "seq" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count > 1) {
SemErr("seq type expects only one type argument");
}
ty = new SeqType(gt.Count == 1 ? gt[0] : null);
.)
| "string" (. tok = t; ty = new UserDefinedType(tok, tok.val, null); .)
| "map" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count == 0) {
ty = new MapType(true, null, null);
} else if (gt.Count != 2) {
SemErr("map type expects two type arguments");
ty = new MapType(true, gt[0], gt.Count == 1 ? new InferredTypeProxy() : gt[1]);
} else {
ty = new MapType(true, gt[0], gt[1]);
}
.)
| "imap" (. tok = t; gt = new List(); .)
[ GenericInstantiation ] (. if (gt.Count == 0) {
ty = new MapType(false, null, null);
} else if (gt.Count != 2) {
SemErr("imap type expects two type arguments");
ty = new MapType(false, gt[0], gt.Count == 1 ? new InferredTypeProxy() : gt[1]);
} else {
ty = new MapType(false, gt[0], gt[1]);
}
.)
| arrayToken (. tok = t; gt = null; .)
[ (. gt = new List(); .)
GenericInstantiation
]
(. int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
ty = theBuiltIns.ArrayType(tok, dims, gt, true);
.)
| "(" (. tok = t; tupleArgTypes = new List(); .)
[ Type (. tupleArgTypes.Add(ty); .)
{ "," Type (. tupleArgTypes.Add(ty); .)
}
]
")" (. if (tupleArgTypes.Count == 1) {
// just return the type 'ty'
} else {
var dims = tupleArgTypes.Count;
var tmp = theBuiltIns.TupleType(tok, dims, true); // make sure the tuple type exists
ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), dims == 0 ? null : tupleArgTypes);
}
.)
| (. Expression e; tok = t; .)
NameSegmentForTypeName (. tok = t; .)
{ "." ident (. tok = t; List typeArgs = null; .)
[ (. typeArgs = new List(); .)
GenericInstantiation
]
(. e = new ExprDotName(tok, e, tok.val, typeArgs); .)
}
(. ty = new UserDefinedType(e.tok, e); .)
)
[ (. Type t2; .)
"->" (. tok = t; .)
Type
(. if (tupleArgTypes != null) {
gt = tupleArgTypes;
} else {
gt = new List{ ty };
}
ty = new ArrowType(tok, gt, t2);
theBuiltIns.CreateArrowTypeDecl(gt.Count);
.)
]
.
GenericInstantiation<.List/*!*/ gt.>
= (. Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; .)
"<"
Type (. gt.Add(ty); .)
{ "," Type (. gt.Add(ty); .)
}
">"
.
/*------------------------------------------------------------------------*/
FunctionDecl
= (. Contract.Ensures(Contract.ValueAtReturn(out f)!=null);
Attributes attrs = null;
IToken/*!*/ id = Token.NoToken; // to please compiler
List typeArgs = new List();
List formals = new List();
Type/*!*/ returnType = new BoolType();
List reqs = new List();
List ens = new List();
List reads = new List();
List decreases;
Expression body = null;
bool isPredicate = false; bool isIndPredicate = false; bool isCoPredicate = false;
bool isFunctionMethod = false;
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
IToken signatureEllipsis = null;
bool missingOpenParen;
.)
/* ----- function ----- */
( "function"
[ "method" (. isFunctionMethod = true; .)
]
(. if (mmod.IsGhost) { SemErr(t, "functions cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
NoUSIdent
(
[ GenericParameters ]
Formals
":"
Type
| "..." (. signatureEllipsis = t; .)
)
/* ----- predicate ----- */
| "predicate" (. isPredicate = true; .)
[ "method" (. isFunctionMethod = true; .)
]
(. if (mmod.IsGhost) { SemErr(t, "predicates cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
NoUSIdent
(
[ GenericParameters ] (. missingOpenParen = true; .)
[ Formals (. missingOpenParen = false; .)
] (. if (missingOpenParen) { errors.Warning(t, "with the new support of higher-order functions in Dafny, parentheses-less predicates are no longer supported; in the new syntax, parentheses are required for the declaration and uses of predicates, even if the predicate takes no additional arguments"); } .)
[ ":" (. SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); .)
]
| "..." (. signatureEllipsis = t; .)
)
/* ----- inductive predicate ----- */
| "inductive" "predicate" (. isIndPredicate = true; .)
(. if (mmod.IsGhost) { SemErr(t, "inductive predicates cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
NoUSIdent
(
[ GenericParameters ]
Formals
[ ":" (. SemErr(t, "inductive predicates do not have an explicitly declared return type; it is always bool"); .)
]
| "..." (. signatureEllipsis = t; .)
)
/* ----- copredicate ----- */
| "copredicate" (. isCoPredicate = true; .)
(. if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
.)
{ Attribute][ }
NoUSIdent
(
[ GenericParameters ]
Formals
[ ":" (. SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool"); .)
]
| "..." (. signatureEllipsis = t; .)
)
)
(. decreases = isIndPredicate || isCoPredicate ? null : new List(); .)
{ FunctionSpec }
[ FunctionBody
]
(. if (DafnyOptions.O.DisallowSoundnessCheating && body == null && ens.Count > 0 && !Attributes.Contains(attrs, "axiom") && !Attributes.Contains(attrs, "imported")) {
SemErr(t, "a function with an ensures clause must have a body, unless given the :axiom attribute");
}
IToken tok = theVerifyThisFile ? id : new IncludeToken(id);
if (isPredicate) {
f = new Predicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, !isFunctionMethod, typeArgs, formals,
reqs, reads, ens, new Specification(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureEllipsis);
} else if (isIndPredicate) {
f = new InductivePredicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, typeArgs, formals,
reqs, reads, ens, body, attrs, signatureEllipsis);
} else if (isCoPredicate) {
f = new CoPredicate(tok, id.val, mmod.IsStatic, mmod.IsProtected, typeArgs, formals,
reqs, reads, ens, body, attrs, signatureEllipsis);
} else {
f = new Function(tok, id.val, mmod.IsStatic, mmod.IsProtected, !isFunctionMethod, typeArgs, formals, returnType,
reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureEllipsis);
}
f.BodyStartTok = bodyStart;
f.BodyEndTok = bodyEnd;
theBuiltIns.CreateArrowTypeDecl(formals.Count);
if (isIndPredicate || isCoPredicate) {
// also create an arrow type for the corresponding prefix predicate
theBuiltIns.CreateArrowTypeDecl(formals.Count + 1);
}
.)
.
FunctionSpec<.List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List decreases.>
= (. Contract.Requires(cce.NonNullElements(reqs));
Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; .)
SYNC
( "requires" Expression OldSemi (. reqs.Add(e); .)
| "reads"
PossiblyWildFrameExpression (. reads.Add(fe); .)
{ "," PossiblyWildFrameExpression (. reads.Add(fe); .)
}
OldSemi
| "ensures" Expression OldSemi (. ens.Add(e); .)
| "decreases" (. if (decreases == null) {
SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
decreases = new List();
}
.)
DecreasesList OldSemi
)
.
PossiblyWildExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr; .)
/* A decreases clause on a loop asks that no termination check be performed.
* Use of this feature is sound only with respect to partial correctness.
*/
( "*" (. e = new WildcardExpr(t); .)
| Expression
)
.
PossiblyWildFrameExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr; .)
/* A reads clause can list a wildcard, which allows the enclosing function to
* read anything. In many cases, and in particular in all cases where
* the function is defined recursively, this makes it next to impossible to make
* any use of the function. Nevertheless, as an experimental feature, the
* language allows it (and it is sound).
*/
( "*" (. fe = new FrameExpression(t, new WildcardExpr(t), null); .)
| FrameExpression
)
.
FrameExpression
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null);
Expression/*!*/ e;
IToken/*!*/ id;
string fieldName = null; IToken feTok = null;
fe = null;
.)
( Expression (. feTok = e.tok; .)
[ "`" Ident (. fieldName = id.val; feTok = id; .)
] (. fe = new FrameExpression(feTok, e, fieldName); .)
|
"`" Ident (. fieldName = id.val; .)
(. fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); .)
)
.
FunctionBody
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
"{" (. bodyStart = t; .)
Expression
"}" (. bodyEnd = t; .)
.
/*------------------------------------------------------------------------*/
BlockStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out block) != null);
List body = new List();
.)
"{" (. bodyStart = t; .)
{ Stmt
}
"}" (. bodyEnd = t;
block = new BlockStmt(bodyStart, bodyEnd, body); .)
.
Stmt<.List/*!*/ ss.>
= (. Statement/*!*/ s;
.)
OneStmt (. ss.Add(s); .)
.
OneStmt
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; IToken/*!*/ id; string label = null;
s = dummyStmt; /* to please the compiler */
BlockStmt bs;
IToken bodyStart, bodyEnd;
int breakCount;
.)
SYNC
( BlockStmt (. s = bs; .)
| AssertStmt
| AssumeStmt
| PrintStmt
| UpdateStmt
| VarDeclStatement
| IfStmt
| WhileStmt
| MatchStmt
| ForallStmt
| CalcStmt
| ModifyStmt
| "label" (. x = t; .)
NoUSIdent ":"
OneStmt (. s.Labels = new LList]