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;
 }

 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());
 }

 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;
 }

 internal ITypeDeclarationMember/*?*/ ParseTypeDeclarationMember(IName typeName)
   //^ ensures result == null || result is TypeDeclarationMember || result is NestedTypeDeclaration;
 {
   //^ assume this.currentToken != Token.EndOfFile; //assume this method is called directly after construction and then never again.
   //TODO: special treatment for enum members
   this.GetNextToken();
   SourceLocationBuilder slb = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
   List<ITypeDeclarationMember> members = new List<ITypeDeclarationMember>(1);
   this.ParseTypeMembers(slb, typeName, members, Parser.EndOfFile|Parser.TypeMemberStart|Token.RightBrace|Parser.AttributeOrNamespaceOrTypeDeclarationStart);
   if (members.Count != 1 || this.currentToken != Token.EndOfFile) return null;
   ITypeDeclarationMember result = members[0];
   //^ assume result is TypeDeclarationMember || result is NestedTypeDeclaration; //TODO: obtain this from post condition of ParseTypeMembers
   return result;
 }

 private void ParseRestOfEnum(SourceLocationBuilder sctx, TypeDeclaration type, List<ITypeDeclarationMember> members, TokenSet followers)
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   TypeExpression texpr = new NamedTypeExpression(new SimpleName(type.Name, type.Name.SourceLocation, false));
   this.Skip(Token.LeftBrace);
   while (this.currentToken == Token.LeftBracket || Parser.IdentifierOrNonReservedKeyword[this.currentToken]){
     this.ParseEnumMember(texpr, members, followers|Token.Comma|Token.RightBrace);
     if (this.currentToken == Token.RightBrace) break;
     this.Skip(Token.Comma);
     if (this.currentToken == Token.RightBrace) break;
   }
   sctx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
   this.Skip(Token.RightBrace);
   if (this.currentToken == Token.Semicolon)
     this.GetNextToken();
   this.SkipTo(followers);
 }

 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 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 ParseNestedNamespaceDeclaration(List<INamespaceDeclarationMember> parentMembers, TokenSet followers)
   //^ requires this.currentToken == Token.Namespace;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   SourceLocationBuilder nsCtx = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
   this.GetNextToken();
   if (!Parser.IdentifierOrNonReservedKeyword[this.currentToken]) 
     this.HandleError(Error.ExpectedIdentifier);
   NameDeclaration nsName = this.ParseNameDeclaration();
   nsCtx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
   List<INamespaceDeclarationMember> nestedMembers = new List<INamespaceDeclarationMember>();
   List<Ast.SourceCustomAttribute> nestedSourceAttributes = new List<Ast.SourceCustomAttribute>();
   NestedNamespaceDeclaration nestedNamespace = new NestedNamespaceDeclaration(nsName, nestedMembers, nestedSourceAttributes, nsCtx);
   parentMembers.Add(nestedNamespace);
   while (this.currentToken == Token.Dot) {
     this.GetNextToken();
     if (!Parser.IdentifierOrNonReservedKeyword[this.currentToken])
       this.HandleError(Error.ExpectedIdentifier);
     nsName = this.ParseNameDeclaration();
     parentMembers = nestedMembers;
     nestedMembers = new List<INamespaceDeclarationMember>();
     nestedSourceAttributes = new List<SourceCustomAttribute>();
     nestedNamespace = new NestedNamespaceDeclaration(nsName, nestedMembers, nestedSourceAttributes, nsCtx);
     parentMembers.Add(nestedNamespace);
   }
   this.Skip(Token.LeftBrace);
   this.ParseNamespaceBody(nestedMembers, null, followers|Token.RightBrace);
   nsCtx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
   this.SkipOverTo(Token.RightBrace, followers);
 }

 private static CompileTimeConstant GetConstantOfSmallestIntegerTypeThatIncludes(ulong ul, TypeCode tc, SourceLocationBuilder ctx) {
   CompileTimeConstant result;
   if (ul <= int.MaxValue && tc == TypeCode.Empty)
     result = new CompileTimeConstant((int)ul, tc == TypeCode.Empty, ctx);
   else if (ul <= uint.MaxValue && (tc == TypeCode.Empty || tc == TypeCode.UInt32))
     result = new CompileTimeConstant((uint)ul, tc == TypeCode.Empty, ctx);
   else if (ul <= long.MaxValue && (tc == TypeCode.Empty || tc == TypeCode.Int64))
     result = new CompileTimeConstant((long)ul, tc == TypeCode.Empty, ctx);
   else
     result = new CompileTimeConstant(ul, tc == TypeCode.Empty, ctx);
   return result;
 }

 private Expression ParseQualifiedName(Expression qualifier, TokenSet followers)
   //^ requires this.currentToken == Token.Arrow || this.currentToken == Token.Dot || this.currentToken == Token.DoubleColon;
   //^ requires this.currentToken == Token.DoubleColon ==> qualifier is SimpleName || qualifier is RootNamespaceExpression;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   Token tok = this.currentToken;
   SourceLocationBuilder slb = new SourceLocationBuilder(qualifier.SourceLocation);
   this.GetNextToken();
   SimpleName name = this.ParseSimpleName(followers);
   slb.UpdateToSpan(name.SourceLocation);
   Expression result;
   if (tok == Token.Arrow) 
     result = new PointerQualifiedName(qualifier, name, slb);
   else if (tok == Token.DoubleColon) 
     result = new AliasQualifiedName(qualifier, name, slb);
   else {
     //^ assert tok == Token.Dot;
     result = new QualifiedName(qualifier, name, slb);
   }
   //^ assume followers[this.currentToken] || this.currentToken == Token.EndOfFile;
   return result;
 }

 private Expression ParseCastExpression(TokenSet followers)
   //^ requires this.currentToken == Token.LeftParenthesis;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   SourceLocationBuilder slb = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
   int position = this.scanner.CurrentDocumentPosition();
   this.GetNextToken();
   List<IErrorMessage> savedErrors = this.scannerAndParserErrors;
   this.scannerAndParserErrors = new List<IErrorMessage>(0);
   TypeExpression targetType = this.ParseTypeExpression(false, false, followers|Token.RightParenthesis);
   bool isCast = false;
   bool isLambda = false;
   if (this.currentToken == Token.RightParenthesis && this.scannerAndParserErrors.Count == 0) {
     if (targetType is NamedTypeExpression) {
       Token nextTok = this.PeekNextToken();
       isCast = Parser.CastFollower[nextTok];
       isLambda = nextTok == Token.Lambda;
     } else
       //Parsed a type expression that cannot also be a value expression.
       isCast = true;
   }
   this.scannerAndParserErrors = savedErrors;
   Expression expression;
   if (!isCast) {
     //Encountered an error while trying to parse (type expr) and there is some reason to be believe that this might not be a type argument list at all.
     //Back up the scanner and let the caller carry on as if it knew that < is the less than operator
     this.scanner.RestoreDocumentPosition(position);
     this.currentToken = Token.None;
     this.GetNextToken();
     if (isLambda)
       expression = this.ParseLambda(followers);
     else
       expression = this.ParseParenthesizedExpression(true, followers);
   } else {
     this.Skip(Token.RightParenthesis);
     Expression valueToCast = this.ParseUnaryExpression(followers);
     slb.UpdateToSpan(valueToCast.SourceLocation);
     expression = new Cast(valueToCast, targetType, slb);
   }
   for (; ; ) {
     switch (this.currentToken) {
       case Token.Arrow:
       case Token.Dot:
       case Token.LeftBracket:
         expression = this.ParseIndexerCallOrSelector(expression, followers);
         break;
       default:
         goto done;
     }
   }
 done:
   this.SkipTo(followers);
   return expression;
 }

 private List<Expression> ParseArrayInitializers(uint rank, TypeExpression elementType, TokenSet followers, bool doNotSkipClosingBrace, SourceLocationBuilder ctx)
   //^ requires this.currentToken == Token.LeftBrace;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   this.GetNextToken();
   List<Expression> initialValues = new List<Expression>();
   if (this.currentToken == Token.RightBrace) {
     ctx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
     this.GetNextToken();
     initialValues.TrimExcess();
     return initialValues;
   }
   while (true) {
     if (rank > 1) {
       List<Expression> elemArrayInitializers;
       SourceLocationBuilder ectx = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
       if (this.currentToken == Token.LeftBrace) {
         elemArrayInitializers = this.ParseArrayInitializers(rank-1, elementType, followers|Token.Comma|Token.LeftBrace, false, ectx);
       } else {
         elemArrayInitializers = new List<Expression>(0);
         this.SkipTo(followers|Token.Comma|Token.LeftBrace, Error.ExpectedLeftBrace);
       }
       CreateArray elemArr = new CreateArray(elementType, elemArrayInitializers.AsReadOnly(), new List<Expression>(0).AsReadOnly(), rank-1, new List<Expression>(0).AsReadOnly(), ectx);
       initialValues.Add(elemArr);
     } else {
       if (this.currentToken == Token.LeftBrace) {
         this.HandleError(Error.ArrayInitInBadPlace);
         SourceLocationBuilder ectx = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
         //^ assume this.currentToken == Token.LeftBrace;
         List<Expression> elemArrayInitializers = this.ParseArrayInitializers(1, elementType, followers|Token.Comma|Token.LeftBrace, false, ectx);
         CreateArray elemArr = new CreateArray(elementType, elemArrayInitializers.AsReadOnly(), new List<Expression>(0).AsReadOnly(), 1, new List<Expression>(0).AsReadOnly(), ectx);
         initialValues.Add(elemArr);
       } else
         initialValues.Add(this.ParseExpression(followers|Token.Comma|Token.RightBrace));
     }
     if (this.currentToken != Token.Comma) break;
     this.GetNextToken();
     if (this.currentToken == Token.RightBrace) break;
   }
   ctx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
   if (!doNotSkipClosingBrace) {
     this.Skip(Token.RightBrace);
     this.SkipTo(followers);
   }
   initialValues.TrimExcess();
   return initialValues;
 }

 private Expression ParseArrayInitializer(ArrayTypeExpression arrayTypeExpression, TokenSet followers)
   //^ requires this.currentToken == Token.LeftBrace;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   uint rank = arrayTypeExpression.Rank;
   SourceLocationBuilder slb = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
   List<Expression> initializers = this.ParseArrayInitializers(rank, arrayTypeExpression.ElementType, followers, false, slb);
   //^ assert followers[this.currentToken] || this.currentToken == Token.EndOfFile;
   List<Expression> lowerBounds = new List<Expression>(0);
   List<Expression> sizes = new List<Expression>(0);
   Expression result = new CreateArray(arrayTypeExpression.ElementType, initializers, lowerBounds, rank, sizes, slb);
   //^ assume followers[this.currentToken] || this.currentToken == Token.EndOfFile;
   return result;
 }

 private CompileTimeConstant ParseHexLiteral()
   //^ requires this.currentToken == Token.HexLiteral;
 {
   string tokStr = this.scanner.GetTokenSource();
   //^ assume tokStr.StartsWith("0x") || tokStr.StartsWith("0X"); //The scanner should not return a Token.HexLiteral when this is not the case.
   SourceLocationBuilder ctx = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
   TypeCode tc = this.scanner.ScanNumberSuffix();
   ctx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
   CompileTimeConstant result;
   switch (tc) {
     case TypeCode.Single:
     case TypeCode.Double:
     case TypeCode.Decimal:
       this.HandleError(Error.ExpectedSemicolon);
       goto default;
     default:
       ulong ul;
       //^ assume tokStr.Length >= 2;
       if (!UInt64.TryParse(tokStr.Substring(2), System.Globalization.NumberStyles.HexNumber, System.Globalization.CultureInfo.InvariantCulture, out ul)) {
         this.HandleError(ctx, Error.IntOverflow);
         ul = 0;
       }
       result = GetConstantOfSmallestIntegerTypeThatIncludes(ul, tc, ctx);
       break;
   }
   //^ assume this.currentToken == Token.HexLiteral; //follows from the precondition
   this.GetNextToken();
   return result;
 }

 private CompileTimeConstant ParseIntegerLiteral() 
   //^ requires this.currentToken == Token.IntegerLiteral;
 {
   string tokStr = this.scanner.GetTokenSource();
   SourceLocationBuilder ctx = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
   TypeCode tc = this.scanner.ScanNumberSuffix();
   ctx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
   CompileTimeConstant result;
   switch (tc) {
     case TypeCode.Single:
       float f;
       if (!Single.TryParse(tokStr, System.Globalization.NumberStyles.None, System.Globalization.CultureInfo.InvariantCulture, out f)) {
         this.HandleError(ctx, Error.FloatOverflow);
         f = float.NaN;
       }
       result = new CompileTimeConstant(f, false, ctx);
       break;
     case TypeCode.Double:
       double d;
       if (!Double.TryParse(tokStr, System.Globalization.NumberStyles.None, System.Globalization.CultureInfo.InvariantCulture, out d)) {
         this.HandleError(ctx, Error.FloatOverflow);
         d = double.NaN;
       }
       result = new CompileTimeConstant(d, false, ctx);
       break;
     case TypeCode.Decimal:
       decimal m;
       if (!decimal.TryParse(tokStr, System.Globalization.NumberStyles.None, System.Globalization.CultureInfo.InvariantCulture, out m)) {
         this.HandleError(ctx, Error.IntOverflow);
         m = decimal.Zero;
       }
       result = new CompileTimeConstant(m, false, ctx);
       break;
     default:
       ulong ul;
       if (!UInt64.TryParse(tokStr, System.Globalization.NumberStyles.None, System.Globalization.CultureInfo.InvariantCulture, out ul)) {
         this.HandleError(ctx, Error.IntOverflow);
         ul = 0;
       }
       result = GetConstantOfSmallestIntegerTypeThatIncludes(ul, tc, ctx);
       break;
   }
   //^ assume this.currentToken == Token.IntegerLiteral; //follows from the precondition
   this.GetNextToken();
   return result;
 }

 private Expression ParseTypeofSizeofOrDefault(TokenSet followers)
   //^ requires this.currentToken == Token.Typeof || this.currentToken == Token.Sizeof || this.currentToken == Token.Default;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   Token tok = this.currentToken;
   SourceLocationBuilder slb = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
   this.GetNextToken();
   this.Skip(Token.LeftParenthesis);
   TypeExpression type = this.ParseTypeExpression(false, true, followers|Token.RightParenthesis);
   slb.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
   this.SkipOverTo(Token.RightParenthesis, followers);
   Expression result;
   if (tok == Token.Typeof) 
     result = new TypeOf(type, slb);
   else if (tok == Token.Sizeof)
     result = new SizeOf(type, slb);
   else {
     //^ assert tok == Token.Default;
     result = new DefaultValue(type, slb);
   }
   //^ assume followers[this.currentToken] || this.currentToken == Token.EndOfFile;
   return result;
 }

 private CompileTimeConstant ParseRealLiteral()
   //^ requires this.currentToken == Token.RealLiteral;
 {
   string tokStr = this.scanner.GetTokenSource();
   SourceLocationBuilder ctx = new SourceLocationBuilder(this.scanner.SourceLocationOfLastScannedToken);
   TypeCode tc = this.scanner.ScanNumberSuffix();
   ctx.UpdateToSpan(this.scanner.SourceLocationOfLastScannedToken);
   CompileTimeConstant result;
   string/*?*/ typeName = null;
   switch (tc) {
     case TypeCode.Single:
       typeName = "float";
       float fVal;
       if (!Single.TryParse(tokStr, System.Globalization.NumberStyles.Float, System.Globalization.CultureInfo.InvariantCulture, out fVal))
         this.HandleError(ctx, Error.FloatOverflow, typeName);
       else if (fVal == 0f && tokStr.IndexOfAny(nonZeroDigits) >= 0)
         this.HandleError(ctx, Error.FloatOverflow, typeName);
       result = new CompileTimeConstant(fVal, false, ctx);
       break;
     case TypeCode.Empty:
     case TypeCode.Double:
       typeName = "double";
       double dVal;
       if (!Double.TryParse(tokStr, System.Globalization.NumberStyles.Float, System.Globalization.CultureInfo.InvariantCulture, out dVal))
         this.HandleError(ctx, Error.FloatOverflow, typeName);
       else if (dVal == 0d && tokStr.IndexOfAny(nonZeroDigits) >= 0)
         this.HandleError(ctx, Error.FloatOverflow, typeName);
       result = new CompileTimeConstant(dVal, tc == TypeCode.Empty, ctx);
       break;
     case TypeCode.Decimal:
       typeName = "decimal";
       decimal decVal;
       if (!Decimal.TryParse(tokStr, System.Globalization.NumberStyles.Float, System.Globalization.CultureInfo.InvariantCulture, out decVal))
         this.HandleError(ctx, Error.FloatOverflow, typeName);
       result = new CompileTimeConstant(decVal, false, ctx);
       break;
     default:
       this.HandleError(Error.ExpectedSemicolon);
       goto case TypeCode.Empty;
   }
   //^ assume this.currentToken == Token.RealLiteral; //follows from the precondition
   this.GetNextToken();
   return result;
 }

 private Expression ParseGenericInstance(Expression expression, TokenSet followers)
   //^ requires this.currentToken == Token.LessThan;
   //^ ensures followers[this.currentToken] || this.currentToken == Token.EndOfFile;
 {
   int position = this.scanner.CurrentDocumentPosition();
   SourceLocationBuilder slb = new SourceLocationBuilder(expression.SourceLocation);
   List<IErrorMessage> savedErrors = this.scannerAndParserErrors;
   this.scannerAndParserErrors = new List<IErrorMessage>(0);
   List<TypeExpression> argumentTypes = this.ParseTypeArguments(slb, false, followers);
   if (this.scannerAndParserErrors.Count > 0 && (argumentTypes.Count <= 1 || Parser.TypeArgumentListNonFollower[this.currentToken])) {
     //Encountered an error while trying to parse <...type args...> and there is some reason to be believe that this might not be a type argument list at all.
     //Back up the scanner and let the caller carry on as if it knew that < is the less than operator
     this.scannerAndParserErrors = savedErrors;
     this.scanner.RestoreDocumentPosition(position);
     this.currentToken = Token.None;
     this.GetNextToken();
     //^ assume this.currentToken == Token.LessThan;
     return expression;
   }
   savedErrors.AddRange(this.scannerAndParserErrors);
   this.scannerAndParserErrors = savedErrors;
   Expression result = new GenericInstanceExpression(expression, argumentTypes, slb);
   //^ assume followers[this.currentToken] || this.currentToken == Token.EndOfFile;
   return result;
 }