| CompilationUnit |
::= |
( PackageDeclaration )? ( ImportDeclaration )* ( TypeDeclaration )* <EOF> |
| PackageDeclaration |
::= |
"package" Name ";" |
| ImportDeclaration |
::= |
"import" Name ( "." "*" )? ";" |
| TypeDeclaration |
::= |
( ClassDeclaration | InterfaceDeclaration | ";" ) |
| ClassDeclaration |
::= |
( "abstract" | "final" | "public" | "strictfp" )* UnmodifiedClassDeclaration |
| UnmodifiedClassDeclaration |
::= |
"class" <IDENTIFIER> ( "extends" Name )? ( "implements" NameList )? ClassBody |
| ClassBody |
::= |
"{" ( ClassBodyDeclaration )* ( ClassInvariantClause )? "}" |
| NestedClassDeclaration |
::= |
( "static" | "abstract" | "final" | "public" | "protected" | "private" | "strictfp" )* UnmodifiedClassDeclaration |
| ClassBodyDeclaration |
::= |
( Initializer | NestedClassDeclaration | NestedInterfaceDeclaration | ConstructorDeclaration | MethodDeclaration | FieldDeclaration ) |
| MethodDeclarationLookahead |
::= |
( "public" | "protected" | "private" | "static" | "abstract" | "final" | "native" | "synchronized" | "strictfp" )* ResultType <IDENTIFIER> "(" |
| InterfaceDeclaration |
::= |
( "abstract" | "public" | "strictfp" )* UnmodifiedInterfaceDeclaration |
| NestedInterfaceDeclaration |
::= |
( "static" | "abstract" | "final" | "public" | "protected" | "private" | "strictfp" )* UnmodifiedInterfaceDeclaration |
| UnmodifiedInterfaceDeclaration |
::= |
"interface" <IDENTIFIER> ( "extends" NameList )? "{" ( InterfaceMemberDeclaration )* "}" |
| InterfaceMemberDeclaration |
::= |
( NestedClassDeclaration | NestedInterfaceDeclaration | MethodDeclaration | FieldDeclaration ) |
| FieldDeclaration |
::= |
( "public" | "protected" | "private" | "static" | "final" | "transient" | "volatile" )* Type VariableDeclarator ( "," VariableDeclarator )* ";" |
| VariableDeclarator |
::= |
VariableDeclaratorId ( "=" VariableInitializer )? |
| VariableDeclaratorId |
::= |
<IDENTIFIER> ( "[" "]" )* |
| VariableInitializer |
::= |
( ArrayInitializer | Expression ) |
| ArrayInitializer |
::= |
"{" ( VariableInitializer ( "," VariableInitializer )* )? ( "," )? "}" |
| MethodDeclaration |
::= |
( "public" | "protected" | "private" | "static" | "abstract" | "final" | "native" | "synchronized" | "strictfp" )* ResultType MethodDeclarator ( "throws" NameList )? ( "{" MethodBodyBlock "}" | ";" ) |
| MethodDeclarator |
::= |
<IDENTIFIER> FormalParameters ( "[" "]" )* |
| FormalParameters |
::= |
"(" ( FormalParameter ( "," FormalParameter )* )? ")" |
| FormalParameter |
::= |
( "final" )? Type VariableDeclaratorId |
| ConstructorDeclaration |
::= |
( "public" | "protected" | "private" )? <IDENTIFIER> FormalParameters ( "throws" NameList )? "{" ( ExplicitConstructorInvocation )? MethodBodyBlock "}" |
| ExplicitConstructorInvocation |
::= |
( "this" Arguments ";" | ( PrimaryExpression "." )? "super" Arguments ";" ) |
| Initializer |
::= |
( "static" )? Block |
| Type |
::= |
( PrimitiveType | Name ) ( "[" "]" )* |
| PrimitiveType |
::= |
( "boolean" | "char" | "byte" | "short" | "int" | "long" | "float" | "double" ) |
| ResultType |
::= |
( "void" | Type ) |
| Name |
::= |
<IDENTIFIER> ( "." <IDENTIFIER> )* |
| NameList |
::= |
Name ( "," Name )* |
| Expression |
::= |
ConditionalExpression ( AssignmentOperator Expression )? |
| AssignmentOperator |
::= |
( "=" | "*=" | "/=" | "%=" | "+=" | "-=" | "<<=" | ">>=" | ">>>=" | "&=" | "^=" | "|=" ) |
| ConditionalExpression |
::= |
ConditionalOrExpression ( "?" Expression ":" ConditionalExpression )? |
| ConditionalOrExpression |
::= |
ConditionalAndExpression ( "||" ConditionalAndExpression )* |
| ConditionalAndExpression |
::= |
InclusiveOrExpression ( "&&" InclusiveOrExpression )* |
| InclusiveOrExpression |
::= |
ExclusiveOrExpression ( "|" ExclusiveOrExpression )* |
| ExclusiveOrExpression |
::= |
AndExpression ( "^" AndExpression )* |
| AndExpression |
::= |
EqualityExpression ( "&" EqualityExpression )* |
| EqualityExpression |
::= |
InstanceOfExpression ( ( "==" | "!=" ) InstanceOfExpression )* |
| InstanceOfExpression |
::= |
RelationalExpression ( "instanceof" Type )? |
| RelationalExpression |
::= |
ShiftExpression ( ( "<" | ">" | "<=" | ">=" ) ShiftExpression )* |
| ShiftExpression |
::= |
AdditiveExpression ( ( "<<" | ">>" | ">>>" ) AdditiveExpression )* |
| AdditiveExpression |
::= |
MultiplicativeExpression ( ( "+" | "-" ) MultiplicativeExpression )* |
| MultiplicativeExpression |
::= |
UnaryExpression ( ( "*" | "/" | "%" ) UnaryExpression )* |
| UnaryExpression |
::= |
( UnaryPlusMinusOperator UnaryExpression | PreIncrementExpression | PreDecrementExpression | UnaryExpressionNotPlusMinus ) |
| PreIncrementExpression |
::= |
"++" PrimaryExpression |
| PreDecrementExpression |
::= |
"--" PrimaryExpression |
| UnaryExpressionNotPlusMinus |
::= |
( UnaryNotPlusMinusOperator UnaryExpression | CastExpression | PostfixExpression ) |
| CastLookahead |
::= |
"(" PrimitiveType |
|
| |
"(" Name "[" "]" |
|
| |
"(" Name ")" ( "~" | "!" | "(" | <IDENTIFIER> | "this" | "super" | "new" | Literal ) |
| PostfixExpression |
::= |
PrimaryExpression ( PostfixOperator )? |
| PostfixOperator |
::= |
( "++" | "--" ) |
| CastExpression |
::= |
( "(" Type ")" UnaryExpression | "(" Type ")" UnaryExpressionNotPlusMinus ) |
| PrimaryExpression |
::= |
PrimaryPrefix ( PrimarySuffix )* |
| PrimaryPrefix |
::= |
( Literal | "this" | "super" "." <IDENTIFIER> | "(" Expression ")" | AllocationExpression | ResultType "." "class" | Name ) |
| PrimarySuffix |
::= |
( "." "this" | "." AllocationExpression | "[" Expression "]" | "." <IDENTIFIER> | Arguments ) |
| Literal |
::= |
( <INTEGER_LITERAL> | <FLOATING_POINT_LITERAL> | <CHARACTER_LITERAL> | <STRING_LITERAL> | BooleanLiteral | NullLiteral ) |
| BooleanLiteral |
::= |
( "true" | "false" ) |
| NullLiteral |
::= |
"null" |
| Arguments |
::= |
"(" ( ArgumentList )? ")" |
| ArgumentList |
::= |
Expression ( "," Expression )* |
| AllocationExpression |
::= |
( "new" PrimitiveType ArrayDimsAndInits | "new" Name ( ArrayDimsAndInits | Arguments ( ClassBody )? ) ) |
| ArrayDimsAndInits |
::= |
( ( "[" Expression "]" )+ ( "[" "]" )* | ( "[" "]" )+ ArrayInitializer ) |
| Statement |
::= |
( LabeledStatement | Block | EmptyStatement | AssertStatement | StatementExpression ";" | SwitchStatement | IfStatement | WhileStatement | DoStatement | ForStatement | BreakStatement | ContinueStatement | ReturnStatement | ThrowStatement | SynchronizedStatement | TryStatement | CheckClause | RetryStatement ) |
| LabeledStatement |
::= |
<IDENTIFIER> ":" Statement |
| Block |
::= |
"{" ( BlockStatement )* "}" |
| BlockStatement |
::= |
( LocalVariableDeclaration ";" | Statement | UnmodifiedClassDeclaration | UnmodifiedInterfaceDeclaration ) |
| LocalVariableDeclaration |
::= |
( "final" )? Type VariableDeclarator ( "," VariableDeclarator )* |
| EmptyStatement |
::= |
";" |
| StatementExpression |
::= |
( PreIncrementExpression | PreDecrementExpression | PrimaryExpression ( "++" | "--" | AssignmentOperator Expression )? ) |
| SwitchStatement |
::= |
"switch" "(" Expression ")" "{" ( SwitchLabel )* "}" |
| SwitchLabel |
::= |
( "case" Expression ":" ( BlockStatement )* | "default" ":" ( BlockStatement )* ) |
| IfStatement |
::= |
"if" "(" Expression ")" Statement ( "else" Statement )? |
| WhileStatement |
::= |
"while" "(" Expression ")" AssertionClause |
| DoStatement |
::= |
"do" AssertionClause "while" "(" Expression ")" ";" |
| ForStatement |
::= |
"for" "(" ( ForInit )? ";" ( Expression )? ";" ( ForUpdate )? ")" AssertionClause |
| ForInit |
::= |
( LocalVariableDeclaration | StatementExpressionList ) |
| StatementExpressionList |
::= |
StatementExpression ( "," StatementExpression )* |
| ForUpdate |
::= |
StatementExpressionList |
| BreakStatement |
::= |
"break" ( <IDENTIFIER> )? ";" |
| ContinueStatement |
::= |
"continue" ( <IDENTIFIER> )? ";" |
| ReturnStatement |
::= |
"return" ( Expression )? ";" |
| ThrowStatement |
::= |
"throw" Expression ";" |
| SynchronizedStatement |
::= |
"synchronized" "(" Expression ")" Block |
| TryStatement |
::= |
"try" Block ( "catch" "(" FormalParameter ")" Block )* ( "finally" Block )? |
| AssertStatement |
::= |
"assert" Expression ( ":" Expression )? ";" |
| MethodBodyBlock |
::= |
( RequireClause )? ( BlockStatement )* ( EnsureClause )? ( RescueClause )? |
| AssertionClause |
::= |
( InvariantClause )? ( VariantClause )? Statement |
| RequireClause |
::= |
<REQUIRE> ( BooleanAssertion ";" )+ <ASS_END> |
| EnsureClause |
::= |
<ENSURE> ( BooleanChangeAssertion ";" )+ <ASS_END> |
| BooleanAssertion |
::= |
( AssertionLabel )? AssertionExpression |
| BooleanChangeAssertion |
::= |
( <CHANGEONLY> "{" ( ChangeList )? "}" | BooleanAssertion ) |
| ChangeList |
::= |
FieldReference ( "," FieldReference )* |
| FieldReference |
::= |
( "this" "." )? <IDENTIFIER> |
| AssertionLabel |
::= |
"[" <IDENTIFIER> "]" |
| ClassInvariantClause |
::= |
<INVARIANT> ( InvariantAssertion ";" )+ <ASS_END> |
| InvariantAssertion |
::= |
( TraceAssertion | BooleanAssertion ) |
| InvariantClause |
::= |
<INVARIANT> ( BooleanAssertion ";" )+ <ASS_END> |
| CheckClause |
::= |
<CHECK> ( BooleanAssertion ";" )+ <ASS_END> |
| RescueClause |
::= |
<RESCUE> ( RescueCatch )+ ( ";" )? <ASS_END> |
| RescueCatch |
::= |
"catch" "(" FormalParameter ")" Block |
| VariantClause |
::= |
<VARIANT> AssertionExpression <ASS_END> |
| AssertionExpression |
::= |
( AssertionForAllExistsExpression | AssertionConditionalExpression ) |
| AssertionForAllExistsExpression |
::= |
( <FORALL> | <EXISTS> ) <IDENTIFIER> ":" ( AssertionFiniteEnumerationCreation | AssertionRangeExpression ) <FORALL_SEP> AssertionExpression |
| AssertionFiniteEnumerationCreation |
::= |
"new" Name AssertionArguments |
| AssertionRangeExpression |
::= |
"{" AssertionShiftExpression <RANGE> AssertionShiftExpression "}" |
| AssertionConditionalExpression |
::= |
AssertionConditionalOrExpression ( "?" AssertionExpression ":" AssertionExpression )? |
| AssertionConditionalOrExpression |
::= |
AssertionConditionalAndExpression ( "||" AssertionConditionalAndExpression )* |
| AssertionConditionalAndExpression |
::= |
AssertionInclusiveOrExpression ( "&&" AssertionInclusiveOrExpression )* |
| AssertionInclusiveOrExpression |
::= |
AssertionExclusiveOrExpression ( "|" AssertionExclusiveOrExpression )* |
| AssertionExclusiveOrExpression |
::= |
AssertionAndExpression ( "^" AssertionAndExpression )* |
| AssertionAndExpression |
::= |
AssertionEqualityExpression ( "&" AssertionEqualityExpression )* |
| AssertionEqualityExpression |
::= |
AssertionInstanceOfExpression ( ( "==" | "!=" ) AssertionInstanceOfExpression )* |
| AssertionInstanceOfExpression |
::= |
AssertionRelationalExpression ( "instanceof" Type )? |
| AssertionRelationalExpression |
::= |
AssertionShiftExpression ( ( "<" | ">" | "<=" | ">=" ) AssertionShiftExpression )* |
| AssertionShiftExpression |
::= |
AssertionAdditiveExpression ( ( "<<" | ">>" | ">>>" ) AssertionAdditiveExpression )* |
| AssertionAdditiveExpression |
::= |
AssertionMultiplicativeExpression ( ( "+" | "-" ) AssertionMultiplicativeExpression )* |
| AssertionMultiplicativeExpression |
::= |
AssertionUnaryExpression ( ( "*" | "/" | "%" ) AssertionUnaryExpression )* |
| AssertionUnaryExpression |
::= |
( UnaryPlusMinusOperator AssertionUnaryExpression | AssertionUnaryExpressionNotPlusMinus ) |
| AssertionUnaryExpressionNotPlusMinus |
::= |
( UnaryNotPlusMinusOperator AssertionUnaryExpression | AssertionCastExpression | AssertionPrimaryExpression ) |
| UnaryPlusMinusOperator |
::= |
( "+" | "-" ) |
| UnaryNotPlusMinusOperator |
::= |
( "!" | "~" ) |
| AssertionCastLookahead |
::= |
( "(" PrimitiveType | "(" Name "[" "]" | "(" Name ")" ( "~" | "!" | "(" | <IDENTIFIER> | "this" | "super" | Literal ) ) |
| AssertionCastExpression |
::= |
( "(" Type ")" AssertionUnaryExpression | "(" Type ")" AssertionUnaryExpressionNotPlusMinus ) |
| AssertionPrimaryExpression |
::= |
AssertionPrimaryPrefix ( AssertionPrimarySuffix )* |
| AssertionPrimaryPrefix |
::= |
( Literal | "this" | "super" "." <IDENTIFIER> | "(" AssertionExpression ")" | Name ) |
| AssertionPrimarySuffix |
::= |
( "." "this" | "[" AssertionExpression "]" | "." <IDENTIFIER> | AssertionArguments ) |
| AssertionArguments |
::= |
"(" ( AssertionArgumentList )? ")" |
| AssertionArgumentList |
::= |
AssertionExpression ( "," AssertionExpression )* |
| RetryStatement |
::= |
<RETRY> ";" |
| TraceAssertion |
::= |
( AssertionLabel )? TraceAssertionDeclaration |
| TraceAssertionDeclaration |
::= |
<TRACE> ( CommunicationExpressions )? <LPAREN> ( TraceConstant )* ( ProcessDeclaration )* <RPAREN> |
| TraceConstant |
::= |
FieldDeclaration |
| ProcessDeclaration |
::= |
( ( ProcessDeclarator <LBRACE> ( FieldDeclaration )* ProcessExpression <RBRACE> ) | ( FieldDeclaration )* ProcessExpression ) |
| ProcessDeclarator |
::= |
<IDENTIFIER> FormalParameters |
| ProcessExpression |
::= |
ProcessParallelExpression |
| ProcessParallelExpression |
::= |
ProcessChoiceExpression ( <TRACE_PARALLEL_OPERATOR> ProcessChoiceExpression )* |
| ProcessChoiceExpression |
::= |
ProcessPrefixExpression ( <TRACE_CHOICE_OPERATOR> ProcessPrefixExpression )* |
| ProcessPrefixExpression |
::= |
( ProcessPrimaryExpression ) ( <TRACE_PREFIX_OPERATOR> ( ProcessPrimaryExpression ) )* |
| ProcessPrimaryExpression |
::= |
( ConditionalCommunication | ProcessCall | ProcessJavaBlock | BasicProcess | ProcessIfElseExpression | ( <LPAREN> ProcessExpression <RPAREN> ) ) |
| ProcessCall |
::= |
<TRACE_CALL_OPERATOR> <IDENTIFIER> Arguments |
| ProcessJavaBlock |
::= |
<TRACE_EXECUTE_OPERATOR> <LPAREN> ( BlockStatement )* <RPAREN> |
| ConditionalCommunication |
::= |
( InputParameter | OutputParameter )? CommunicationExpressions ( <TRACE_CONDITION> <LPAREN> Expression <RPAREN> )? |
| BasicProcess |
::= |
( <TRACE_DEADLOCK_OPERATOR> | <TRACE_CHAOS_OPERATOR> | <TRACE_TERMINATION_OPERATOR> ) |
| ProcessIfElseExpression |
::= |
<TRACE_IF_OPERATOR> <LPAREN> Expression <RPAREN> <LBRACE> ProcessExpression <RBRACE> <TRACE_ELSE_OPERATOR> <LBRACE> ProcessExpression <RBRACE> |
| CommunicationExpressions |
::= |
( CommunicationExpression | <LBRACE> CommunicationExpression ( <COMMA> CommunicationExpression )* <RBRACE> ) ( <TRACE_COMPLEMENT_OPERATOR> CommunicationExpressions )? |
| CommunicationExpression |
::= |
( Communication | CommunicationWithWildcards ) |
| Communication |
::= |
( <THIS> "." )? Name CommunicationParameterList ( "." <IDENTIFIER> )? |
| CommunicationWithWildcards |
::= |
( <STAR> "." <IDENTIFIER> CommunicationParameterList ( "." <IDENTIFIER> )? | <STAR> | ( <PRIVATE> | <PACKAGE> | <PROTECTED> | <PUBLIC> )? ( <THIS> | Name ) "." <STAR> ) |
| CommunicationParameterList |
::= |
<LPAREN> ( CommunicationParameter ( <COMMA> CommunicationParameter )* )? <RPAREN> |
| CommunicationParameter |
::= |
( LayedDownParameter | TypedParameter | OutputParameter | InputParameter | <STAR> | <HOOK> ) |
| LayedDownParameter |
::= |
( <FLOATING_POINT_LITERAL> | <INTEGER_LITERAL> | <CHARACTER_LITERAL> | <STRING_LITERAL> ) |
| TypedParameter |
::= |
Type ( <IDENTIFIER> )? |
| InputParameter |
::= |
<HOOK> <IDENTIFIER> |
| OutputParameter |
::= |
<BANG> <IDENTIFIER> |
