Friedrich Schiller University Jena, Department of Mathematics & Computer Science
Programming Languages and Compilers

FPP-Syntax in EBNF

Nonterminals are in small letters (stmt), terminals are in capital letters (NULL) or included in single apostrophes (':=') .
program                 ::=  sequence_of_stmts
sequence_of_stmts       ::=  stmt { stmt }
stmt                    ::=  sim_stmt | compound_stmt
sim_stmt                ::=  null_stmt| assignment_stmt 
compound_stmt           ::=  if_stmt  | case_stmt | loop_stmt 

null_stmt               ::=  pre_assertion null_stmt_two | null_stmt_two 
null_stmt_two           ::=  NULL  ';' [ post_assertion ]
assignment_stmt         ::=  pre_assertion assignment_stmt_two 
                           | assignment_stmt_two
assignment_stmt_two     ::=  IDENTIFIER ':=' expr ';' [ post_assertion ] 

if_stmt                 ::=  pre_assertion if_stmt_two | if_stmt_two
if_stmt_two             ::=  if_stmt_body [ post_assertion ]
if_stmt_body            ::=  IF expr THEN seq_of_stmts elsif_or_else END IF ';' 
elsif_or_else           ::=  ELSIF expr THEN seq_of_stmts elsif_or_else 
                           | ELSE seq_of_stmts |   

case_stmt               ::=  case_stmt_body | pre_assertion case_stmt_body
case_stmt_body          ::=  CASE expr IS case_stmt_alt_2 END CASE ';' 
                               [ post_assertion ]        
case_stmt_alt_2         ::=  case_stmt_alt_when | case_stmt_alt_other
case_stmt_alt_other     ::=  WHEN OTHERS '=>' seq_of_stmts
case_stmt_alt_when      ::=  case_stmt_alt case_stmt_alt_iter
case_stmt_alt_iter      ::=  case_stmt_alt case_stmt_alt_iter 
                            | case_stmt_alt_other |
case_stmt_alt           ::=  WHEN choice { '|' choice } '=>' seq_of_stmts         
choice                  ::=  sim_expr | sim_expr '..' sim_expr

loop_stmt               ::=  loop_pre_assertion loop_post_assertion 
                               invariant_assertion loop_stmt_body
loop_stmt_body          ::=  for_loop ';' 
                           | termination_assertion while_loop ';'
for_loop                ::=  [ IDENTIFIER ':' ] for_iteration_scheme LOOP 
                               seq_of_stmts END LOOP [ IDENTIFIER ] 
while_loop              ::=  [ IDENTIFIER ':' ] while_iteration_scheme LOOP 
                               seq_of_stmts END LOOP [ IDENTIFIER ]
for_iteration_scheme    ::=  FOR for_loop_prm_spec                  
while_iteration_scheme  ::=  WHILE expr
for_loop_prm_spec       ::=  IDENTIFIER IN [ REVERSE ] loop_rng
loop_rng                ::=  sim_expr '..' sim_expr
loop_pre_assertion      ::=  precondition ':' expr ';'
loop_post_assertion     ::=  postcondition ':' expr ';'
invariant_assertion     ::=  invcondition ':' expr ';'         
termination_assertion   ::=  termcondition ':' expr ';'

pre_assertion           ::=  precondition ':' expr ';'             
post_assertion          ::=  postcondition ':' expr ';'

precondition            ::=  '--!'PRE         
postcondition           ::=  '--!'POST         
invcondition            ::=  '--!'INV         
termcondition           ::=  '--!'TERM         

expr                    ::=  rel_AND_rel | rel_AND_THEN_rel | rel_OR_rel 
                           | rel_OR_ELSE_rel | rel_XOR_rel | imp_expr  
rel_AND_rel             ::=  rel AND rel | rel_AND_rel AND rel    
rel_OR_rel              ::=  rel OR rel | rel_OR_rel OR rel    
rel_AND_THEN_rel        ::=  rel AND THEN rel | rel_AND_THEN_rel AND THEN rel    
rel_OR_ELSE_rel         ::=  rel OR ELSE rel | rel_OR_ELSE_rel OR ELSE rel    
rel_XOR_rel             ::=  rel | XOR_rel 
XOR_rel                 ::=  rel XOR rel | XOR_rel XOR rel      
imp_expr                ::=  expr '=>' expr                 
rel                     ::=  sim_expr [ relal_op sim_expr ]
relal_op                ::=  '=' | '/=' | '<' | '<=' | '>' | '>='

sim_expr                ::=  add_op_term | quantifier_expr          
add_op_term             ::=  term | unary_add_op term 
                           | add_op_term binary_add_op term  
term                    ::=  factor_mult_op_factor   
factor_mult_op_factor   ::=  factor | factor_mult_op_factor mult_op factor 
factor                  ::=  pri [ '**' pri ] | ABS pri | NOT pri
pri                     ::=  NUMERIC_LITERAL | IDENTIFIER [ '(' sim_exps ')' ] 
                           | '(' expr ')' 
sim_exps                ::=  sim_expr { ',' sim_expr } 
quantifier_expr         ::=  '(' quantifier idents ':' [ expr ] ':' expr ')'
idents                  ::=  IDENTIFIER { ',' IDENTIFIER } 
quantifier              ::=  FORALL | EXISTS
              
binary_add_op           ::=  '+' | '-' 
unary_add_op            ::=  '+' | '-' 
mult_op                 ::=  '*' | '/' | MOD | REM             

S. Kauer 1996  |  J. F. H. Winkler  2006.Sep.04