Download Automatic Test Data Generation From VDM

C
LR(1) GRAMMAR FOR VDM-SL
| function-definition-list “;” error
| function-definition-list error ;
function-definition = explicit-function-definition
| implicit-function-definition ;
explicit-function-definition = name “:” function-type name parameters-list “==” expression
maybe-precondition
| name “[” type-variable-list “]” “:” function-type name
parameters-list “==” expression maybe-precondition ;
implicit-function-definition = name parameter-type-list declName “:” type maybe-precondition
post expression
| name “[” type-variable-list “]” parameter-type-list declName “:”
type maybe-precondition post expression ;
type-variable-list = type-variable-identifier
| type-variable-list “,” type-variable-identifier ;
type-variable-identifier = “@” name ;
parameter-type-list = “(” “)”
| “(” pattern-type-pair-list “)” ;
pattern-type-pair-list = pattern-list “:” type
| pattern-type-pair-list “,” pattern-list “:” type ;
parameters-list = brack-maybe-pattern-list
| parameters-list brack-maybe-pattern-list ;
maybe-precondition = empty
| pre beginPreCond expression endPreCond ;
brack-maybe-pattern-list = “(” “)”
| “(” pattern-list “)” ;
operation-definition-list = operations openScope operation-definition closeScope
| operation-definition-list “;” openScope operation-definition
closeScope
| operation-definition-list “;” error
| operation-definition-list error ;
operation-definition = explicit-operation-definition
| implicit-operation-definition ;
explicit-operation-definition = name “:” discretionary-type “==>” discretionary-type name
brack-maybe-pattern-list “==” statement maybe-precondition ;
implicit-operation-definition = name parameter-type-list maybe-externals maybe-precondition
post expression
| name parameter-type-list maybe-externals maybe-precondition
post expression errs exception-list
62
Revision: 1.43