The PALE syntax is defined in two levels: a basic language, and some convenient extensions making PALE look like ordinary programming languages. The grammar below is written in BNF extended with the following extra notation:
( X )^{@}: | a comma separated list of one or more X's | |
( X )^{&}: | a comma separated list of zero or more X's | |
( X )^{*}: | a list of zero or more X's | |
( X )^{?}: | zero or one X |
p: | pointer/data variable/field |
b: | boolean variable/field |
s: | set variable |
m: | predicate |
T: | type |
str: | label (string enclosed in "..") |
pale | -> | ( declaration )^{*} |
declaration | -> | transducedecl | | | typedecl | | | progvar; | | | preddecl; |
typedecl | -> | type T = { ( field ; )^{*} } |
field | -> | data ( d )^{@} : T |
| | pointer ( p )^{@} : T [ formula ] | |
| | bool ( b )^{@} |
progvar | -> | data ( p )^{@} : T |
| | pointer ( p )^{@} : T | |
| | bool ( b )^{@} |
logicvar | -> | pointer ( p )^{@} : T |
| | bool ( b )^{@} | |
| | set ( s )^{@} : T |
preddecl | -> | pred m ( ( logicvar )^{&} ) = formula |
transducedecl | -> | transduce ( str )^{?} ( logicvar ; )^{*} [ formula ( { ( pointerformula )^{&} } )^{?} ] stm |
pointerformula | -> | T . p ( [ formula ] )^{?} |
stm | -> | stm stm |
| | ( assignment )^{@} ; | |
| | if ( condexp ) { stm } ( else { stm } )^{?} | |
| | assert [ formula ( { ( pointerformula )^{&} } )^{?} ] | |
| | ; |
assignment | -> | lboolexp = condexp | | | lptrexp = ptrexp |
formula | -> | existpos ( p )^{@} of T : formula | | | allpos ( p )^{@} of T : formula |
| | existset ( s )^{@} of T : formula | | | allset ( s )^{@} of T : formula | |
| | existptr ( p )^{@} of T : formula | | | allptr ( p )^{@} of T : formula | |
| | existbool ( s )^{@} : formula | | | allbool ( s )^{@} : formula | |
| | ( formula ) | | | ! formula | |
| | formula & formula | | | formula | formula | |
| | formula => formula | | | formula <=> formula | |
| | ptrexp in setexp | | | setexp sub setexp | |
| | setexp = setexp | | | setexp != setexp | |
| | empty ( setexp ) | | | ptrexp < routingexp > ptrexp | |
| | formula ? formula : formula | | | ptrexp < routingexp > setexp | |
| | m ( ( predarg )^{&} ) | | | boolexp |
predarg | -> | formula | | | ptrexp | | | setexp |
condexp | -> | ? | | | boolexp | | | [ formula ] |
boolexp | -> | ( boolexp ) | | | ! boolexp |
| | boolexp & boolexp | | | boolexp | boolexp | |
| | boolexp => boolexp | | | boolexp <=> boolexp | |
| | boolexp = boolexp | | | ptrexp = ptrexp | |
| | boolexp != boolexp | | | ptrexp != ptrexp | |
| | true | | | false | |
| | lboolexp | | | boolexp ? boolexp : boolexp |
lboolexp | -> | b | | | ptrexp . b |
ptrexp | -> | null | | | this | | | pos | | | lptrexp | | | formula ? ptrexp : ptrexp |
lptrexp | -> | p | | | ptrexp . p |
setexp | -> | s | | | ptrexp ^ T . p | | | { ( ptrexp )^{@} } | | | formula ? setexp : setexp |
| | setexp union setexp | | | setexp inter setexp | | | setexp minus setexp |
routingexp | -> | p | | | ^ T . p | | | [ formula ] |
| | routingexp . routingexp | | | ( routingexp ) | |||
| | routingexp + routingexp | | | routingexp * |
n: | procedure |
declaration | -> | proc n ( ( progvar )^{&} ) : ( T | void ) ( logicvar ; )^{*} [ formula ( { ( pointerformula )^{&} } )^{?} ] ( { ( progvar ; )^{*} stm } )^{?} [ formula ( { ( pointerformula )^{&} } )^{?} ] |
stm | -> | while [ formula ( { ( pointerformula )^{&} } )^{?} ] ( condexp ) { stm } |
| | return progexp ; | |
| | split [ formula ( { ( pointerformula )^{&} } )^{?} ] ( [ formula ( { ( pointerformula )^{&} } )^{?} ] )^{?} ; | |
| | proccall ; |
assignment | -> | lprogexp = proccall |
proccall | -> | n ( ( progexp )^{&} ) [ formula ] |
boolexp | -> | n . b | | | return |
ptrexp | -> | n . p | | | return |
setexp | -> | n . s |
progexp | -> | condexp | | | ptrexp |
lprogexp | -> | lboolexp | | | lptrexp |
Copyright © 2000 Anders Møller |