Description of syntax:

"|" :

or 

"(expression)?" :

optional 

"(expression)+" :

1 or more 

"(expression)*" :

0 or more 

"boolean" :

true or false

"ID" :

ID tag 

"fop" :

First Order Predicate

"EOF" :

End Of File

compilationUnit :

( face | body )+ EOF

face :

"face" faceID ( faceParameters )? "is" ( requirementClause )? 
  ( importClause )* ( declaration )+ "end" "face" 
           

body :

"body" bodyID ":" ( faceID )+ 
  ( faceParameters )? 
"is" 
  ( requirementClause )? 
  ( importClause )* 
  ( implementation )+ 
"end" "body"
             

faceParameters :

"[" ( ID )+ "]" 

requirementClause :

"required" 
  ( declaration | 
  ( "face" faceID "in" faceName ) | 
  ( "body" bodyID ":" faceName ) )+ 
"end" "required" 
           

importClause :

"import" ( ID )+ "from" ( bodyID ":" )? faceID

implementation :

procedureBody | variableBody | functionBody | typeDeclaration

declaration :

( variableDeclaration ( assertion )*
  | typeDeclaration              
  | procedureDeclaration 
  | functionDeclaration 
  | typeOperator ) 
              

variableDeclaration : 

"variable" ( variableID )+ ":" 
  ( "constant" 
  | "shared" 
  | "protected" 
  | "remote" 
  | "spread" | ) 
  type
           

typeDeclaration :

"type" typeID "is" type ( assertion )*

typeOperator : 

"type" typeID "(" ( typeID )+ ")" "is" type ( assertion )*

type : 

( bodyorfaceID ".")? typeID 
  | "integer" 
  | "boolean" 
  | "rational" 
  | "floating" 
  | "character" 
  | "string" ( "[" integerExpression "]" )? 
  | "range" discreteRange 
  | enumeration 
  | "array" "[" discreteRangeList "]" "of" type 
  | "record" ID ":" type ( "," ID ":" type )* "end" "record" 
  | "access" typeID 
  | "apply" typeOperatorID "(" typeList ")" 
  | "private" 

discreteRange : 

( ID | INTEGER | STRINGLITERAL ) ".." ( ID | INTEGER | STRINGLITERAL ) 

enumeration :

"(" ( ( STRINGLITERAL )+ | ( ID )+ | ( INTEGER )+ ) ")" 

typeList : 

type ( "," type )* 

name : 

partialName ( "." partialName )*

partialName : 

ID ( "[" parameterList "]" )? 

parameterList : 

parameter ( "," parameter )+ | expression 

parameter : 

name | STRINGLITERAL | INTEGER | FLOATING | RATIONAL | parenthesizedExpression

aggregate : 

"(" ID "=>" expression ( "," ID "=>" expression )* ")"

expression : 

( "-" )? subExpression ( aop subExpression )*

subExpression : 

functionCall 
  | parenthesizedExpression
  | variableName 
  | STRINGLITERAL 
  | INTEGER 
  | FLOATING 
  | RATIONAL 
           

aop : 

"/" | "*" | "**" | "+" | "-" | "mod" 

booleanExpression : 

( "not" )? 
  ( functionCall 
  | ( variableName | parenthesizedBoolean ) ( lop booleanExpression )?              
  | expression rop expression 
  | expression "in" discreteRange 
  | "true" 
  | "false" 
  ) 
           

lop : 

"and" | "or" | "not" | "xor"| "cand" | "cor"

rop : 

"=" | "<>" | "<=" | "<" | ">=" | ">"

allocator : 

"new" accessTypeID 

formula : 

  "skip" 
  | procedureCall 
  | temporalExistentialQuantification 
  | variableName ":=" ( aggregate | allocator | expression ) 
  | variableName "==" booleanExpression 
  | "if" ( assertion )* guardedFormula ( "[ ]" guardedFormula )+ ( assertion )* "fi"! 
  | "do" ( assertion )* guardedFormula ( assertion )* "od" 
  | "forall" ID ":" type "in" discreteRange 
     temporalExistentialQuantification              
  | "return" expression 
  | ( "fetchadd" | "swap" ) "(" variableName "," expression "," ID ")"
  | ( "fetchand" | "fetchor" | "fetchxor" ) "(" variableName "," booleanExpression "," expression "," ID ")"

guardedFormula :

booleanExpression "=>" formula

fetchop :

"fetchadd" | "fetchand" | "fetchor" | "fetchxor" | "swap"

temporalExistentialQuantification :

( temporalExistentialQuantifier )? block

temporalExistentialQuantifier :

"declare" ( implementation )+ 

block : 

"begin" compositeFormula "end"            

compositeFormula : 

sequentialComposition | concurrentComposition            

sequentialComposition : 

concurrentComposition ";" compositeFormula            

concurrentComposition : 

( assertion )* 
formula ( "&" formula )* 
( assertion )*

procedureDeclaration : 

"procedure" ID "(" ( formalParameterList )? ")" ( assertion )* 

functionDeclaration : 

"function" ( ID | STRINGLITERAL ) 
  "(" ( formalParameterList )? ")" "return" type ( assertion )*
           

formalParameterList : 

ID ":" ( modifier )? type 
( "," ID ":" ( modifier )? type )* 

modifier : 

"constant" | "shared" | "protected" | "remote" | "spread" 

procedureBody : 

"procedure" ID "(" ( formalParameterList )? ")" 
( assertion )* 
"is" temporalExistentialQuantification 
           

variableBody : 

variableDeclaration ( ":=" ( aggregate | allocator | expression ) ";"
  | "==" booleanExpression ";" )? 
( assertion )* 

functionBody : 

"function" ( ID | STRINGLITERAL ) 
  "(" ( formalParameterList )? ")" "return" type 
  ( assertion )* 
  "is" temporalExistentialQuantification 
           

assertion : 

"{" ( ID ":" ( logicVariableList )? ":" )? 
  foPredicate ( "by" reason )? "}" 
           

logicVariableList : 

( ID )+ 

foPredicate : 

( "not" )? 
  ( "all" logicVariables "are" foPredicate 
  | "exists" logicVariables "that" foPredicate 
  | "sum" logicVariables ":" expression "equals" expression 
  | "product" logicVariables ":" expression "equals" expression 
  | "numberof" logicVariables ":" booleanExpression "equals" expression 
  | ( variableName | parenthesizedPredicate | predicateInvocation ) 
    ( fop 
       ( variableName | parenthesizedPredicate | predicateInvocation ) )*
  | expression rop expression 
  | expression "in" discreteRange
  | variableName 
  | "true" 
  | "false" 
  | predicateInvocation 
  ) 
           

logicVariables : 

ID ( "," ID)* ":" type "in" ( discreteRange | booleanExpression )
  ( fop booleanExpression )*

parenthesizedPredicate : 

"(" foPredicate ")"

predicateInvocation : 

ID "(" ( parameterList )? ")"

reason : 

ID

fop : 

"and" | "or" | "xor" | "implies" | "iff" 

faceID : 

ID

faceName : 

name

bodyID : 

ID

typeID : 

ID

bodyorfaceID : 

bodyID | faceID

reason : 

ID

accessTypeID : 

ID