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
)*