! -- Sets ----------------------------------------------------

{ID Head}      = {Letter}
{ID UHead}     = {Letter} + [_]
{ID UTail}     = {Alphanumeric} + [_]
{Hex Digit}    = {Digit} + [ABCDEFabcdef]
{String Chars} = {Printable} - ["\]

! -- Terminals -----------------------------------------------

Identifier = {ID Head}{ID UTail}* | {ID UHead}{ID UTail}+ | '@' {ID UHead}{ID UTail}*
StringLiteral = '"' ( {String Chars} | '\' {Printable} )* '"'
IntLiteral = {Digit}+
HexLiteral = '0' 'x' {Hex Digit}+

Comment Start = '/*'
Comment End = '*/'
Comment Line = '//'

! -- Global Declarations ------------------------------------------------------------------

<Specification> ::= <GlobalDecls> 

<GlobalDecls> ::= <GlobalDecls> <GlobalDecl>
                | !empty

<GlobalDecl> ::= <SpecDecl>
               | <Namespace>

<SpecDecl> ::= <ClassDecl> 
             | <EnumDecl> 
             | <RangeDecl>
             | <DelegateDecl>
             | <GroupDecl>
             | <Using> 
         
<SpecDecls> ::= <SpecDecls> <SpecDecl>
              | !empty

<Namespace> ::= <AttributeList> 'namespace' <Refines> '{' <SpecDecls> '}'
              | <AttributeList> 'namespace' Identifier <Refines>
                '{' <SpecDecls> '}'
          
<Refines> ::= 'refines' Identifier
            | !empty

<ClassDecl> ::= <AttributesAndModifiers> 'class' Identifier <Extends> <Inherits> 
                '{' <MemberDecls> '}'

<Extends> ::= 'extends' <Type>
            | !empty

<Abstracts> ::= 'abstracts' <Type>
              | !empty

<ExtendsOrAbstracts> ::= 'abstracts' <Type>
                       | 'extends' <Type>
                       | !empty

<Inherits> ::= ':' <Type>
             | !empty
          
<Using> ::= 'using' <QualifiedName> ';' 

! -- Types --------------------------------------------------------------------------------

<Types> ::= <Types> ',' <Type> 
          | <Type> 

<Type> ::= <PrimitiveType>
         | 'range' '(' <Range> ')'
         | <QualifiedName> <GenericParameters>
     
     
<GenericParameters> ::= '<' <Types> '>'
                      | !empty

<QualifiedName> ::= <QualifiedName> '.' Identifier 
                  | Identifier

<QualifiedNamesEx> ::= <QualifiedNamesEx> ',' <QualifiedName> 
                     | <QualifiedNamesEx> ',' '!' <QualifiedName> 
                     | <QualifiedName>

<IntegerPrimitiveType> ::= 'sbyte' | 'byte' 
                         | 'short' | 'ushort' 
                         | 'int'   | 'uint' 
                         | 'long'  | 'ulong'

<ReferencePrimitiveType> ::= 'string' | 'object' 

<PrimitiveType> ::= <IntegerPrimitiveType> 
                  | <ReferencePrimitiveType> 
                  | 'bool' 
                  | 'any'
  
<Literal> ::= 'null' | 'true' | 'false' | StringLiteral | IntLiteral | HexLiteral
  
! -- Modifiers and Attributes -------------------------------------------------------------
      
<Modifier> ::= 'static' 
             | 'synthetic'
             | 'abstract'
             | 'base'
             | 'readonly'

<Modifiers> ::= <Modifiers> <Modifier> 
              | <Modifier> 

<AttributesAndModifiers> ::= <Attributes> <Modifiers> 
                           | <Attributes> 
                           | <Modifiers> 
                           | !empty

<AttributeList> ::= <Attributes> 
                  | !empty

<Attributes> ::= <Attributes> <Attribute> 
               | <Attribute> 

<Attribute> ::= '[' <Expression> ']'

! -- Members and Inner Declarations -------------------------------------------------------

<MemberDecls> ::= <MemberDecls> <MemberDecl> 
                | !empty

<MemberDecl> ::= <FieldDecl> 
               | <MethodDecl> 
               | <StructDecl> 
               | <EnumDecl> 
               | <RangeDecl>
               | <RuleDecl> 
               | <PropertyDecl> 
               | <GroupDecl>

<FieldDecl> ::= <AttributesAndModifiers> <Type> <NullitySpec>
                <FieldVariableList> ';' 
              | <AttributesAndModifiers> 'const' <Type> 
                <FieldVariableList> ';' 

<FieldVariableList> ::= <FieldVariableList> ',' <FieldVariable> 
                      | <FieldVariable> 

<FieldVariable> ::= Identifier 
                  | Identifier '=' <Expression> 

<PropertyDecl> ::= <AttributesAndModifiers> <Type> <NullitySpec> Identifier 
                   '{' <PropertyAccessors> '}'
                 | <AttributesAndModifiers> <Type> <NullitySpec> Identifier 
                   '[' <Type> Identifier ']' '{' <PropertyAccessors> '}'
                 | <AttributesAndModifiers> <Type> <NullitySpec> 'this' 
                   '[' <Type> Identifier ']' '{' <PropertyAccessors> '}'
                 | <AttributesAndModifiers> '_' Identifier 
                   '{' <PropertyAccessors> '}'
                 | <AttributesAndModifiers> '_' Identifier 
                   '[' <Type> Identifier ']' '{' <PropertyAccessors> '}'

<PropertyAccessors> ::= <PropertyGetter> <PropertySetter> 
                      | <PropertySetter> <PropertyGetter> 
                      | <PropertyGetter> 
                      | <PropertySetter> 

<PropertyGetter> ::= <AttributeList> 'get' <ContractDeclListOrSemicolon> 

<PropertySetter> ::= <AttributeList> 'set' <ContractDeclListOrSemicolon>

<MethodDecl> ::= <AttributesAndModifiers> <MethodSignature> 
                 <ContractDeclListOrSemicolon>
               | <AttributesAndModifiers> <CtorSignature> 
                 <ContractDeclListOrSemicolon>

<MethodSignature> ::= <Type> <NullitySpec> Identifier '(' <ParameterList> ')'
                    | 'void' Identifier '(' <ParameterList> ')'
                    | '_' Identifier '(' <ParameterList> ')'
                    | 'instance' Identifier '(' <ParameterList> ')'
                
<CtorSignature> ::= Identifier '(' <ParameterList> ')'

<NullitySpec> ::= '!' 
                | !empty

<ContractDeclListOrSemicolon> ::= <ContractDeclList> <MethodBody> 
                                | ';' 

<ContractDeclList> ::= <ContractDeclList> <ContractDecl>  
                     | !empty

<ContractDecl> ::= 'requires' <Expression> <OtherwiseClause> ';'
                 | 'ensures' <Expression> <OtherwiseClause> ';'

<OtherwiseClause> ::= 'otherwise' <RequiresAction> 
                    | !empty

<RequiresAction> ::= 'wait'
                   | 'notice'
                   | 'warning'
                   | 'error'

<MethodBody> ::= <Block> 
               | !empty

<DelegateDecl> ::= <AttributeList> 'delegate' <MethodSignature> ';'

<GroupDecl> ::= <AttributesAndModifiers> 'group' <MethodSignature> '=' 
                '{' <QualifiedNamesEx> '}' ';'

<StructDecl> ::= <AttributesAndModifiers> <StructOrUnion> Identifier 
                 '{' <FieldOrStructDecls> '}'

<FieldOrStructDecls> ::= <FieldOrStructDecls> <FieldDecl> 
                       | <FieldOrStructDecls> <StructDecl> 
                       | <FieldOrStructDecls> <PropertyDecl> 
                       | !empty

<StructOrUnion> ::= 'struct' 
                  | 'union' 

<EnumDecl> ::= <AttributesAndModifiers> <EnumOrflags> Identifier 
               <ExtendsOrAbstracts> '{' <EnumFieldDeclList> '}'

<EnumOrflags> ::= 'enum' 
                | 'flags' 

<EnumFieldDeclList> ::= <EnumFieldDecls> 
                      | !empty

<EnumFieldDecls> ::= <EnumFieldDecls> ',' <EnumVariable> 
                   | <EnumVariable> 

<EnumVariable> ::= <FieldVariable> 
                 | Identifier '=' <Range> 
                 | Identifier '=' '{' <RangeItemList> '}'

<Range> ::= <Expression> '..' <Expression> 

<RangeItemList> ::= <RangeItemList> ',' <RangeItem> 
                  | <RangeItem> 

<RangeItem> ::= <Range> 
              | <Expression> 

<RangeDecl> ::= <AttributesAndModifiers> 'range' Identifier <Abstracts> '=' 
                <Range> ';'
         
! -- Rules --------------------------------------------------------------------------------
          
<RuleDecl> ::= <AttributesAndModifiers> 'rule' <RuleSeverity> 
               <RuleSpecificationList> ';' 
             | <AttributesAndModifiers> 'rule' <RuleSeverity> Identifier 
               <RuleSpecificationList> ';' 

<RuleSeverity> ::= 'notice' 
                 | 'warning' 
                 | 'error'
                 | !empty 

<RuleSpecificationList> ::= <RuleSpecificationList> ',' <RuleSpecification> 
                          | <RuleSpecification> 

<RuleSpecification> ::= <Quantification> <RulePattern> 

<Quantification> ::= 'forall' '(' <QuantifiedVariableList> ')'
                   | !empty

<QuantifiedVariableList> ::= <QuantifiedVariableList> ',' <QuantifiedVariable>
                           | <QuantifiedVariable> 

<QuantifiedVariable> ::= <Type> Identifier 

! -- Temporal Patterns -------------------------------------------------------------------

<RulePattern> ::= <RuleExpression> 'is' 'universal' <RuleScope> 
                | <RuleExpression> 'is' 'absent' <RuleScope> 
                | <RuleExpression> 'exists' <RuleScope> 
                | <RuleExpression> 'precedes' <RuleExpression> <RuleScope> 
                | <RuleExpression> 'leads' 'to' <RuleExpression> <RuleScope> 
                | <RuleExpression> 'responds' 'to' <RuleExpression> <RuleScope> 
                | <RuleExpression> 'corresponds' 'to' <RuleExpression> <RuleScope> 

<RuleScope> ::= 'globally' 
              | 'before' <RuleExpression> 
              | 'after' <RuleExpression> 
              | 'after' <RuleExpression> 'until' <RuleExpression> 
              | 'between' <RuleExpression> 'and' <RuleExpression> 

<RuleExpression> ::= '{' <Expression> '}'

! -- Parameters and Arguments ------------------------------------------------------------

<ParameterList> ::= <Parameters> 
                  | !empty

<Parameters> ::= <Parameters> ',' <Parameter> 
               | <Parameter> 

<ArgumentList> ::= <Arguments> 
                 | !empty

<Arguments> ::= <Arguments> ',' <Argument> 
              | <Argument> 

<Parameter> ::= <AttributeList> <ParamModifier> <Type> <NullitySpec> Identifier 
              | <AttributeList> 'out' 'instance' 
              | <AttributeList> 'instance' 
              | '_' 
              | '...'

<Argument> ::= <ParamModifier> <Expression> 
             | 'in' <Expression> 'out' <Expression>
             | '_' 
             | '...'

<ParamModifier> ::= 'out' | 'ref' | !empty

! -- Expressions -------------------------------------------------------------------------

<PrimaryExpression> ::= <Literal> 
                      | <ConstructExpression> 
                      | <NewExpression>
                      | <ChooseExpression>
                      | <ElementAccessExpression>
                      | <MemberAccessExpression>
                      | <SpecialVariableAccess>
                      | <AnyMemberAccess>
                      | <InvocationExpression> 
                      | <PostIncExpression>
                      | <PostDecExpression>
                      | '(' <Expression> ')'

<ConstructExpression> ::= <Construct> '(' <Expression> ')'

<Construct> ::= 'old' 

<NewExpression> ::= 'new' <Type> '(' <ArgumentList> ')'

<ChooseExpression> ::= <ChooseConstruct> '(' 'bool' ')'
                     | <ChooseConstruct> '(' <Range> ')'
                     | <ChooseConstruct> '(' <Expression> ')'
                     | <ChooseConstruct> '{' <Expression> ',' <Expressions> '}'

<ChooseConstruct> ::= 'choose' | 'max' | 'min'

<Expressions> ::= <Expressions> ',' <Expression>
                | <Expression>
                 
<InvocationExpression> ::= <PrimaryExpression> '(' <ArgumentList> ')' 
                           <InvocationEvent>

<InvocationEvent> ::= '::' 'succeeded' 
                    | '::' 'failed' 
                    | '::' 'entered' 
                    | '::' 'returned'
                    | !empty
                    
<SpecialVariableAccess> ::= 'thread'     | 'this'     | 'result'     | 'value'
                      
<AnyMemberAccess> ::= 'any' <AccessEvent>
                    | <QualifiedName> '.' 'any' <AccessEvent>

<ElementAccessExpression> ::= <PrimaryExpression> '[' <Expression> ']'

<MemberAccessExpression> ::= <QualifiedName> <AccessEvent>
                           | <SpecialVariableAccess> '.' <QualifiedName> 
                             <AccessEvent>

<AccessEvent> ::= '::' 'written'
                | '::' 'read'
                | '::' 'get'
                | '::' 'set'
                | !empty

<UnaryExpression> ::= <PrimaryExpression> 
                    | '+' <UnaryExpression> 
                    | '-' <UnaryExpression> 
                    | '!' <UnaryExpression> 
                    | '~' <UnaryExpression> 
                    | <PreIncExpression>
                    | <PreDecExpression>

<PreIncExpression> ::= '++' <UnaryExpression>
                 
<PreDecExpression> ::= '--' <UnaryExpression>
                 
<PostIncExpression> ::= <PrimaryExpression> '++'
                  
<PostDecExpression> ::= <PrimaryExpression> '--'

<MulExpression> ::= <MulExpression> '*' <UnaryExpression> 
                  | <MulExpression> '/' <UnaryExpression> 
                  | <MulExpression> '%' <UnaryExpression> 
                  | <UnaryExpression> 

<AddExpression> ::= <AddExpression> '+' <MulExpression> 
                  | <AddExpression> '-' <MulExpression> 
                  | <MulExpression> 

<ShiftExpression> ::= <ShiftExpression> '<<' <AddExpression> 
                    | <ShiftExpression> '>>' <AddExpression> 
                    | <AddExpression> 

<RelExpression> ::= <RelExpression> '<' <ShiftExpression> 
                  | <RelExpression> '>' <ShiftExpression> 
                  | <RelExpression> '<=' <ShiftExpression> 
                  | <RelExpression> '>=' <ShiftExpression> 
                  | <RelExpression> 'is' <QualifiedName>
                  | <RelExpression> 'as' <QualifiedName>
                  | <ShiftExpression> 

<EquExpression> ::= <EquExpression> '==' <RelExpression> 
                  | <EquExpression> '!=' <RelExpression> 
                  | <EquExpression> '===' <RelExpression> 
                  | <EquExpression> '!==' <RelExpression> 
                  | <RelExpression> 

<BitAndExpression> ::= <BitAndExpression> '&' <EquExpression> 
                     | <EquExpression> 

<BitXorExpression> ::= <BitXorExpression> '^' <BitAndExpression> 
                     | <BitAndExpression> 

<BitOrExpression> ::= <BitOrExpression> '|' <BitXorExpression> 
                    | <BitXorExpression> 

<AndExpression> ::= <AndExpression> '&&' <BitOrExpression> 
                  | <BitOrExpression> 

<OrExpression> ::= <OrExpression> '||' <AndExpression> 
                 | <AndExpression> 

<ImpliesExpression> ::= <ImpliesExpression> '==>' <OrExpression> 
                      | <OrExpression> 

<ConditionalExpression> ::= <ImpliesExpression>
                          | <ImpliesExpression> '?' <Expression> ':' <Expression> 

<AssignmentExpression> ::= <PrimaryExpression> <AssignmentOperator> <Expression> 

<AssignmentOperator> ::= '=' | '+=' | '-=' | '*=' | '/=' | '%=' 
                       | '&=' | '|=' | '^=' | '>>=' | '<<=' | ':='

<Expression> ::= <AssignmentExpression> 
               | <ConditionalExpression> 
    
<StatementExpression> ::= <AssignmentExpression> 
                        | <InvocationExpression> 
                        | <PreIncExpression>
                        | <PreDecExpression>
                        | <PostIncExpression>
                        | <PostDecExpression>

! -- Statements --------------------------------------------------------------------------

<Block> ::= '{' <StatementList> '}'

<StatementList> ::= <StatementList> <Statement> 
                  | !empty

<Statement> ::= <EmbeddedStatement>
              | <LocalDeclStatement>
              | <LabelStatement>

<EmbeddedStatement> ::= ';' 
                      | <ExpressionStatement> 
                      | <ReturnStatement> 
                      | <BreakStatement>
                      | <GotoStatement>
                      | <IfStatement>
                      | <LoopStatement>
                      | <SelectStatement>
                      | <AtomicStatement>
                      | <AssertStatement>
                      | <AssumeStatement>
                      | <AsyncStatement>
                      | <TryWithStatement>
                      | <RaiseStatement>
                      | <Block>

<ExpressionStatement> ::= <StatementExpression> ';' 

<ReturnStatement> ::= 'return' <Expression> ';' 
                    | 'return' ';' 

<BreakStatement> ::= 'break' ';'
               
<GotoStatement> ::= 'goto' Identifier ';'

<IfStatement> ::= 'if' '(' <Expression> ')' <EmbeddedStatement>
                | 'if' '(' <Expression> ')' <EmbeddedStatement> 'else' 
                  <EmbeddedStatement>

<LoopStatement> ::= 'while' '(' <Expression> ')' 
                    <EmbeddedStatement>
                  | 'foreach' '(' <Type> Identifier 'in' <Expression> ')' 
                    <EmbeddedStatement>
                  | 'anytimes' '(' <QualifiedName> ')' 
                    <EmbeddedStatement>

<SelectStatement> ::= 'select' <SelectQualifiers> '{' <WaitStatements> '}'
                
<SelectQualifiers> ::= <SelectQualifiers> <SelectQualifier> 
                     | !empty

<SelectQualifier> ::= 'end' 
                    | 'first'

<WaitStatements> ::= <WaitStatements> <WaitStatement> 
                   | <WaitStatement>

<WaitStatement> ::= 'wait' '(' <Expression> ')' '->' <EmbeddedStatement>
                  | 'timeout' '->' <EmbeddedStatement>

<AtomicStatement> ::= 'atomic' <Block>

<AssertStatement> ::= 'assert' '(' <Expression> ')' ';'
                    | 'assert' '(' <Expression> ',' StringLiteral ')' ';'
                
<AssumeStatement> ::= 'assume' '(' <Expression> ')' ';'

<LabelStatement> ::= 'base' ':'
                   | 'extracted' ':'
                   | 'group' Identifier ':'
                   | Identifier ':'
                
<AsyncStatement> ::= 'async' <InvocationExpression> 'with' <Expression> ';'
                   | 'async' <InvocationExpression> ';'

<LocalDeclStatement> ::= <Type> Identifier ';' 
                       | <Type> Identifier '=' <Expression> ';' 

<TryWithStatement> ::= 'try' <Block> 'with' '{' <WithClauses> '}'

<WithClauses> ::= <WithClauses> <WithClause> 
                | <WithClause>

<WithClause> ::= Identifier '->' <EmbeddedStatement>
               | 'any' '->' <EmbeddedStatement>
           
<RaiseStatement> ::= 'raise' Identifier ';'