private Statement ParseFor(TokenSet followers)
   //^ requires this.currentToken == Token.For;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   SourceLocationBuilder slb = new SourceLocationBuilder(this.scanner.CurrentSourceLocation);
   this.GetNextToken();
   if (this.currentToken == Token.Each) return this.ParseForEach(slb, followers);
   SmallBasicSimpleName variableName = this.ParseSimpleName(followers|Parser.ExpressionStart|Token.Equals|Token.To|Token.Step|Token.EndOfLine);
   variableName.rootClass = this.rootClass;
   this.Skip(Token.Equals);
   Expression startValue = this.ParseExpression(followers|Parser.ExpressionStart|Token.To|Token.Step|Token.EndOfLine);
   variableName.expressionToInferTargetTypeFrom = startValue;
   SourceLocationBuilder rslb = new SourceLocationBuilder(startValue.SourceLocation);
   this.Skip(Token.To);
   Expression endValue = this.ParseExpression(followers|Parser.ExpressionStart|Token.Step|Token.EndOfLine);
   rslb.UpdateToSpan(endValue.SourceLocation);
   Expression/*?*/ stepValue = null;
   if (this.currentToken == Token.Step) {
     this.GetNextToken();
     stepValue = this.ParseExpression(followers|Token.EndOfLine);
   }
   this.Skip(Token.EndOfLine);
   BlockStatement body = this.ParseStatementBlock(followers|Token.Next);
   slb.UpdateToSpan(body.SourceLocation);
   ForRangeStatement result = new ForRangeStatement(null, variableName, new Range(startValue, endValue, rslb), stepValue, body, slb); //TODO Spec#: Range should not be ambiguous
   this.SkipClosingKeyword(Token.Next, followers);
   return result;
 }

 private BlockStatement ParseStatementBlock(TokenSet followers) {
   SourceLocationBuilder slb = new SourceLocationBuilder(this.scanner.CurrentSourceLocation);
   List<Statement> statements = new List<Statement>();
   this.ParseStatements(statements, followers);
   slb.UpdateToSpan(this.scanner.CurrentSourceLocation);
   return new BlockStatement(statements, slb);
 }

 private Statement ParseDo(TokenSet followers)
   //^ requires this.currentToken == Token.Do;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   SourceLocationBuilder slb = new SourceLocationBuilder(this.scanner.CurrentSourceLocation);
   this.GetNextToken();
   this.Skip(Token.While);
   Expression condition = this.ParseExpression(followers|Token.EndOfLine);
   this.Skip(Token.EndOfLine);
   BlockStatement body = this.ParseStatementBlock(followers|Token.Loop);
   slb.UpdateToSpan(this.scanner.CurrentSourceLocation);
   WhileDoStatement result = new WhileDoStatement(condition, body, slb);
   this.SkipClosingKeyword(Token.Loop, followers);
   return result;
 }

 private void ParseStatements(List<Statement> statements, TokenSet followers)
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   while (Parser.StatementStart[this.currentToken]) {
     switch (this.currentToken) {
       case Token.Do: statements.Add(this.ParseDo(followers)); break;
       case Token.For: statements.Add(this.ParseFor(followers)); break;
       case Token.Gosub: statements.Add(this.ParseGosub(followers)); break;
       case Token.Goto: statements.Add(this.ParseGoto(followers)); break;
       case Token.Identifier: statements.Add(this.ParseAssignmentOrCallOrLabel(followers)); break;
       case Token.If: statements.Add(this.ParseIf(followers)); break;
       case Token.Return: statements.Add(this.ParseReturn(followers)); break;
       case Token.EndOfLine: this.GetNextToken(); break;
       default: this.SkipTo(followers); break;
     }
   }
 }

 protected override Expression ParseBraceLabeledExpression(SourceLocationBuilder slb, TokenSet followers)
 {
     var lab = (VccLabeledExpression)this.ParseLabeledExpression(followers | Token.RightBrace);
       this.Skip(Token.RightBrace);
       var body = this.ParseExpression(followers);
       var labString = lab.Label.Name.Value;
       var labName = new VccByteStringLiteral(labString, lab.Label.SourceLocation);
       var labArg = lab.Expression;
       if (labArg is DummyExpression)
     labArg = new CompileTimeConstant(1, false, lab.Label.SourceLocation);
       if (labString == "use") { // this condition is sort of a hack, it should likely look at some function \lbl_use(...) or something
     labArg = new VccByteStringLiteral(labArg.SourceLocation.Source, labArg.SourceLocation);
       }
       var args = new[] { labName, labArg, body };
       slb.UpdateToSpan(body.SourceLocation);
       return new VccMethodCall(this.GetSimpleNameFor("\\labeled_expression"), args, slb.GetSourceLocation());
 }

        public void TestGetByName()
        {
            TokenSet a = new TokenSet((IRandom)m_Random.MockInstance);
            a.Name = "a";

            TokenSet a2 = new TokenSet((IRandom)m_Random.MockInstance);
            a2.Name = "a";

            Assert.IsNull(m_TokenSetCollection.FindByName("a"));

            m_TokenSetCollection.Add(a);
            Assert.AreSame(a, m_TokenSetCollection.FindByName("a"));

            m_TokenSetCollection.Add(a2);
            Assert.AreSame(a, m_TokenSetCollection.FindByName("a"));

            Assert.IsNull(m_TokenSetCollection.FindByName("b"));
        }

        public void TestCountByName()
        {
            TokenSet a = new TokenSet((IRandom)m_Random.MockInstance);
            a.Name = "a";

            TokenSet a2 = new TokenSet((IRandom)m_Random.MockInstance);
            a2.Name = "a";

            Assert.AreEqual(0, m_TokenSetCollection.CountByName("a"));

            m_TokenSetCollection.Add(a);
            Assert.AreEqual(1, m_TokenSetCollection.CountByName("a"));

            m_TokenSetCollection.Add(a2);
            Assert.AreEqual(2, m_TokenSetCollection.CountByName("a"));

            Assert.AreEqual(0, m_TokenSetCollection.CountByName("b"));
        }

 protected override List<Expression> ParseArgumentList(SourceLocationBuilder slb, TokenSet followers)
 {
     var result = new List<Expression>();
       this.Skip(Token.LeftParenthesis);
       while (this.currentToken != Token.RightParenthesis) {
     if (this.currentToken == Token.Specification) {
       result.Add(this.ParseSpecArgument(followers | Token.Comma | Token.Specification | Token.RightParenthesis));
       continue;
     }
     result.Add(this.ParseArgumentExpression(followers | Token.Comma | Token.Specification | Token.RightParenthesis));
     if (this.currentToken == Token.Comma) {
       this.GetNextToken();
       continue;
     }
     if (this.currentToken == Token.Specification)
       continue;
     break;
       }
       slb.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
       this.SkipOverTo(Token.RightParenthesis, followers);
       return result;
 }

 private void ParseTypeMembers(SourceLocationBuilder sctx, IName typeName, List<ITypeDeclarationMember> members, TokenSet followers)
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   TokenSet followersOrTypeMemberStart = followers|Parser.TypeMemberStart;
   for (; ; ) {
     SourceLocationBuilder tctx = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
     List<SourceCustomAttribute>/*?*/ attributes = this.ParseAttributes(followersOrTypeMemberStart);
     List<ModifierToken> modifiers = this.ParseModifiers();
     switch (this.currentToken) {
       case Token.Class:
         this.ParseNestedClassDeclaration(members, attributes, this.ConvertToTypeDeclarationFlags(modifiers), tctx, followersOrTypeMemberStart);
         break;
       case Token.Interface:
         this.ParseNestedInterfaceDeclaration(members, attributes, this.ConvertToTypeDeclarationFlags(modifiers), tctx, followersOrTypeMemberStart);
         break;
       case Token.Struct:
         this.ParseNestedStructDeclaration(members, attributes, this.ConvertToTypeDeclarationFlags(modifiers), tctx, followersOrTypeMemberStart);
         break;
       case Token.Enum:
         this.ParseNestedEnumDeclaration(members, attributes, this.ConvertToTypeDeclarationFlags(modifiers), tctx, followersOrTypeMemberStart);
         break;
       case Token.Delegate:
         this.ParseNestedDelegateDeclaration(members, attributes, this.ConvertToTypeDeclarationFlags(modifiers), tctx, followersOrTypeMemberStart);
         break;
       case Token.Const:
         this.ParseConst(members, attributes, modifiers, tctx, followersOrTypeMemberStart);
         break;
       case Token.Invariant:
         goto default;
         //this.ParseInvariant(attributes, modifierTokens, modifierContexts, tctx, followersOrTypeMemberStart);
         //break;
       case Token.Bool:
       case Token.Decimal:
       case Token.Sbyte:
       case Token.Byte:
       case Token.Short:
       case Token.Ushort:
       case Token.Int:
       case Token.Uint:
       case Token.Long:
       case Token.Ulong:
       case Token.Char:
       case Token.Float:
       case Token.Double:
       case Token.Object:
       case Token.String:
       case Token.Void:
       case Token.Identifier:
         this.ParseConstructorOrFieldOrMethodOrPropertyOrStaticInitializer(typeName, members, attributes, modifiers, tctx, followersOrTypeMemberStart);
         break;
       case Token.Event:
         this.ParseEvent(members, attributes, modifiers, tctx, followersOrTypeMemberStart); 
         break;
       case Token.Operator:
       case Token.Explicit:
       case Token.Implicit:
         this.ParseOperator(members, attributes, modifiers, null, tctx, followersOrTypeMemberStart); 
         break;
       case Token.BitwiseNot:
         this.ParseDestructor(typeName, members, attributes, modifiers, tctx, followersOrTypeMemberStart); 
         break;
       default:
         if (Parser.IdentifierOrNonReservedKeyword[this.currentToken]) goto case Token.Identifier;
         sctx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
         this.SkipTo(followers);
         return;
     }
   }
 }

 private void ParseEnumMember(TypeExpression typeExpression, List<ITypeDeclarationMember> members, TokenSet followers)
   //^ requires this.currentToken == Token.LeftBracket || Parser.IdentifierOrNonReservedKeyword[this.currentToken];
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   SourceLocationBuilder sctx = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
   List<SourceCustomAttribute>/*?*/ attributes = this.ParseAttributes(followers|Parser.AttributeOrTypeDeclarationStart|Parser.IdentifierOrNonReservedKeyword);
   if (!Parser.IdentifierOrNonReservedKeyword[this.currentToken])
     this.HandleError(Error.ExpectedIdentifier);
   NameDeclaration name = this.ParseNameDeclaration();
   Expression/*?*/ initializer = null;
   if (this.currentToken == Token.Assign) {
     this.GetNextToken();
     initializer = this.ParseExpression(followers);
   }
   EnumMember member = new EnumMember(attributes, typeExpression, name, initializer, sctx);
   members.Add(member);
   this.SkipTo(followers);
 }

 private void ParseRestOfTypeDeclaration(SourceLocationBuilder sctx, TypeDeclaration type, List<Ast.GenericTypeParameterDeclaration> genericParameters,
   List<TypeExpression> baseTypes, List<ITypeDeclarationMember> members, TokenSet followers)
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   this.ParseGenericTypeParameters(genericParameters, followers|Token.Colon|Token.LeftBrace|Token.Where);
   this.ParseBaseTypes(baseTypes, followers|Token.LeftBrace|Token.Where);
   this.ParseGenericTypeParameterConstraintsClauses(genericParameters, followers|Token.LeftBrace);
   this.Skip(Token.LeftBrace);
   this.ParseTypeMembers(sctx, type.Name, members, followers|Token.RightBrace);
   ISourceLocation tokLoc = this.scanner.SourceLocationOfLastScannedToken;
   //^ assume tokLoc.SourceDocument == sctx.SourceDocument;
   sctx.UpdateToSpan(tokLoc);
   this.Skip(Token.RightBrace);
   if (this.currentToken == Token.Semicolon)
     this.GetNextToken();
   this.SkipTo(followers);
 }

 private void ParseGenericTypeParameterConstraintsClauses(List<Ast.GenericTypeParameterDeclaration> genericTypeParameters, TokenSet followers)
   // ^ requires forall{Ast.GenericTypeParameterDeclaration genericTypeParameter in genericTypeParameters; genericTypeParameter is SpecSharpGenericTypeParameterDeclaration};
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   while (this.currentToken == Token.Where) {
     this.GetNextToken();
     if (!Parser.IdentifierOrNonReservedKeyword[this.currentToken])
       this.HandleError(Error.ExpectedIdentifier);
     NameDeclaration name = this.ParseNameDeclaration();
     SpecSharpGenericTypeParameterDeclaration/*?*/ applicableParameter = null;
     foreach (Ast.GenericTypeParameterDeclaration genericTypeParameter in genericTypeParameters)
       if (genericTypeParameter.Name.UniqueKey == name.UniqueKey) {
         //^ assume genericTypeParameter is SpecSharpGenericTypeParameterDeclaration; //follows from precondition
         applicableParameter = (SpecSharpGenericTypeParameterDeclaration)genericTypeParameter; 
         break; 
       }
     if (applicableParameter == null) {
       this.HandleError(name.SourceLocation, Error.TyVarNotFoundInConstraint);
       applicableParameter = new SpecSharpGenericTypeParameterDeclaration(null, name, (ushort)genericTypeParameters.Count);
     }
     this.Skip(Token.Colon);
     this.ParseGenericTypeParameterConstraints(applicableParameter, followers|Token.Where);
   }
   this.SkipTo(followers);
 }

 private void ParseGenericTypeParameters(List<Ast.GenericTypeParameterDeclaration> genericParameters, TokenSet followers) {
   if (this.currentToken != Token.LessThan) return;
   this.GetNextToken();
   while (this.currentToken != Token.GreaterThan && this.currentToken != Token.Colon && this.currentToken != Token.LeftBrace && this.currentToken != Token.EndOfFile) {
     List<SourceCustomAttribute>/*?*/ attributes = this.ParseAttributes(followers|Parser.IdentifierOrNonReservedKeyword);
     if (!Parser.IdentifierOrNonReservedKeyword[this.currentToken])
       this.HandleError(Error.ExpectedIdentifier);
     NameDeclaration name = this.ParseNameDeclaration();
     genericParameters.Add(new SpecSharpGenericTypeParameterDeclaration(attributes, name, (ushort)genericParameters.Count));
     if (this.currentToken != Token.Comma) break;
     this.GetNextToken();
   }
   if (this.currentToken == Token.RightShift)
     this.currentToken = Token.GreaterThan;
   else
     this.SkipOverTo(Token.GreaterThan, followers);
 }

 private void ParseNestedDelegateDeclaration(List<ITypeDeclarationMember> typeMembers, List<SourceCustomAttribute>/*?*/ attributes, TypeDeclaration.Flags flags, SourceLocationBuilder sctx, TokenSet followers)
   //^ requires this.currentToken == Token.Delegate;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   this.GetNextToken();
   TypeExpression returnType = this.ParseTypeExpression(false, false, followers|Token.LeftParenthesis|Token.Semicolon|Parser.IdentifierOrNonReservedKeyword);
   if (!Parser.IdentifierOrNonReservedKeyword[this.currentToken])
     this.HandleError(Error.ExpectedIdentifier);
   NameDeclaration name = this.ParseNameDeclaration();
   List<Ast.GenericTypeParameterDeclaration> genericParameters = new List<Ast.GenericTypeParameterDeclaration>();
   List<Ast.ParameterDeclaration> parameters = new List<Ast.ParameterDeclaration>();
   SignatureDeclaration signature = new SignatureDeclaration(returnType, parameters, sctx);
   NestedDelegateDeclaration type = new NestedDelegateDeclaration(attributes, flags, name, genericParameters, signature, sctx);
   typeMembers.Add(type);
   this.ParseGenericTypeParameters(genericParameters, followers|Token.LeftParenthesis|Token.Where|Token.Semicolon);
   this.ParseParameters(parameters, Token.RightParenthesis, followers|Token.Where|Token.Semicolon, sctx);
   this.ParseGenericTypeParameterConstraintsClauses(genericParameters, followers|Token.Semicolon);
   sctx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
   if (this.currentToken == Token.Semicolon)
     this.GetNextToken();
   this.SkipTo(followers);
 }

 private void SkipSemiColon(TokenSet followers)
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   if (this.currentToken == Token.Semicolon) {
     this.GetNextToken();
     this.SkipTo(followers);
   } else {
     this.Skip(Token.Semicolon);
     while (!this.scanner.TokenIsFirstAfterLineBreak && this.currentToken != Token.Semicolon && this.currentToken != Token.RightBrace && this.currentToken != Token.EndOfFile
       && (this.currentToken != Token.LeftBrace || !followers[Token.LeftBrace]))
       this.GetNextToken();
     if (this.currentToken == Token.Semicolon) 
       this.GetNextToken();
     this.SkipTo(followers);
   }
 }

 private List<SourceCustomAttribute>/*?*/ ParseAttributes(TokenSet followers) {
   List<SourceCustomAttribute>/*?*/ result = null;
   this.ParseAttributes(ref result, false, followers);
   this.SkipTo(followers);
   return result;
 }

 private void ParseNestedStructDeclaration(List<ITypeDeclarationMember> typeMembers, List<SourceCustomAttribute>/*?*/ attributes, TypeDeclaration.Flags flags, SourceLocationBuilder sctx, TokenSet followers)
   //^ requires this.currentToken == Token.Struct;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   this.GetNextToken();
   if (!Parser.IdentifierOrNonReservedKeyword[this.currentToken])
     this.HandleError(Error.ExpectedIdentifier);
   NameDeclaration name = this.ParseNameDeclaration();
   List<Ast.GenericTypeParameterDeclaration> genericParameters = new List<Ast.GenericTypeParameterDeclaration>();
   List<TypeExpression> baseTypes = new List<TypeExpression>();
   List<ITypeDeclarationMember> members = new List<ITypeDeclarationMember>();
   NestedStructDeclaration type = new NestedStructDeclaration(attributes, flags, name, genericParameters, baseTypes, members, sctx);
   typeMembers.Add(type);
   this.ParseRestOfTypeDeclaration(sctx, type, genericParameters, baseTypes, members, followers);
 }

 private void SkipTo(TokenSet followers)
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   if (followers[this.currentToken]) return;
   Error error = Error.InvalidExprTerm;
   if (this.currentToken == Token.Using)
     error = Error.UsingAfterElements;
   else if (!this.insideBlock)
     error = Error.InvalidMemberDecl;
   this.HandleError(error, this.scanner.GetTokenSource());
   while (!followers[this.currentToken] && this.currentToken != Token.EndOfFile)
     this.GetNextToken();
 }

 private void ParseNestedEnumDeclaration(List<ITypeDeclarationMember> namespaceMembers, List<SourceCustomAttribute>/*?*/ attributes, TypeDeclaration.Flags flags, SourceLocationBuilder sctx, TokenSet followers)
   //^ requires this.currentToken == Token.Enum;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   this.GetNextToken();
   if (!Parser.IdentifierOrNonReservedKeyword[this.currentToken])
     this.HandleError(Error.ExpectedIdentifier);
   NameDeclaration name = this.ParseNameDeclaration();
   TypeExpression/*?*/ underlyingType = null;
   if (this.currentToken == Token.Colon) {
     this.GetNextToken();
     if (this.currentToken != Token.EndOfFile)
       underlyingType = this.ParseTypeExpression(false, false, followers|Token.LeftBrace);
   }
   List<ITypeDeclarationMember> members = new List<ITypeDeclarationMember>();
   NestedEnumDeclaration type = new NestedEnumDeclaration(attributes, flags, name, underlyingType, members, sctx);
   namespaceMembers.Add(type);
   this.ParseRestOfEnum(sctx, type, members, followers);
 }

 private void ParseBaseTypes(List<TypeExpression> baseTypes, TokenSet followers)
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   if (this.currentToken == Token.Colon) {
     this.GetNextToken();
     TokenSet baseTypeStart = Parser.IdentifierOrNonReservedKeyword|Parser.Predefined;
     while (baseTypeStart[this.currentToken]) {
       //^ assume this.currentToken != Token.EndOfFile;
       baseTypes.Add(this.ParseTypeExpression(false, false, followers|Token.Comma));
       if (this.currentToken != Token.Comma) break;
       this.GetNextToken();
     }
   }
   this.SkipTo(followers);
 }