JPV - Input Language

parseVerifier ::= Prog
Prog ::= Condition Statements Condition
Block ::= "{" ( Statements )? "}"
Condition ::= "##" BoolExpr "##"
Statements ::= ( Statement | Block ) ( Statements )?
Statement ::= EmptyStatement
| AssignStatement
| WhileStatement
| IfStatement
EmptyStatement ::= ";"
AssignExpr ::= Id ( "=" ArithExpr | ( "+=" ArithExpr ) | ( "-=" ArithExpr ) | ( "/=" ArithExpr ) | ( "*=" ArithExpr ) | ( "++" ) | ( "--" ) )
AssignStatement ::= AssignExpr ";"
WhileStatement ::= "while" "(" BoolExpr ")" "##" BoolExpr "##" ( Statement | ( Block ) )
IfStatement ::= "if" "(" BoolExpr ")" ( Statement | Block ) ( "else" ( Statement | Block ) )?
DoStatement ::= "do" ( Statement | Block ) "while" "(" BoolExpr ")"
ForStatement ::= "for" "(" AssignExpr ";" BoolExpr ";" AssignExpr ")" ( Statement | Block )
ArithExpr ::= Product ( "+" Product | "-" Product )*
Product ::= Term ( "*" Term | "%" Term | "/" Term )*
Term ::= "+" Term
| "-" Term
| "(" ArithExpr ")"
| intFunc
| Num
| Id
| Const
BoolExpr ::= BoolTerm ( ( "&" | "&&" ) BoolTerm | ( "|" | "||" ) BoolTerm )*
BoolProduct ::= BoolTerm ( "==" BoolTerm )*
CompareExpr ::= ArithExpr ( ">" ArithExpr | "<" ArithExpr | "==" ArithExpr | "<=" ArithExpr | ">=" ArithExpr | "!=" ArithExpr )
BoolTerm ::= "!" BoolTerm
| boolFunc
| "(" BoolExpr ")"
| ( "true" )
| ( "false" )
| CompareExpr
intFunc ::= Id "(" ( ArithExpr ( "," ArithExpr )* )? ")"
boolFunc ::= Const "(" ( ArithExpr ( "," ArithExpr )* )? ")"
Num ::= ["0" - "9"] ( ["0" - "9"] )*
Letter ::= ["a" - "z", "A" - "Z"]
Const ::= ["A" - "Z"] ( "_" | Letter | Num )*
Id ::= ["a" - "z"] ( "_" | Letter | Num )*