PALE syntax

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

## The basic language

### Identifiers

 p: pointer/data variable/field b: boolean variable/field s: set variable m: predicate T: type str: label (string enclosed in "..")

### Declarations

 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 ] )?

### Statements

 stm -> stm stm | ( assignment )@ ; | if ( condexp ) { stm } ( else { stm } )? | assert [ formula ( { ( pointerformula )& } )? ] | ;
 assignment -> lboolexp = condexp | lptrexp = ptrexp

### Formulas and expressions

 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 *

• Only types which are used (directly or indirectly) through some data variable declaration can be used for declaration of pointer or set variables; the remaining types are essentially weeded from the program.
• Pointer field formulas cannot select pointer fields (using 'ptrexp . p'), except the current field (using 'p').
• this can only be used in pointer field formulas (as a non-null pointer).
• pos can only be used in routing expression filter formulas (as a non-null pointer).
• null cannot be used as left side of . or in, as set element in {...}, or as ptrexp in ptrexp<routingexp>ptrexp.
• All expressions are type-checked in a standard way.
• Precedence and associativity of operators is standard.
• Declarations have standard lexical scope.
• The logicvars in a transduce declaration are called "logical variables".
• Formulas in pointerformulas cannot refer to logical variables.
• The formula can only be omitted from a pointerformula when used at assert.
• Expressions of the form formula?ptrexp:ptrexp or formula?setexp:setexp can only be used inside formulas.
• Usually the transduce construct is not used directly, but rather via automatic reduction of the extension constructs to the basic language.
• The [formula] form of condexp and the multi-assignment statement form usually only appears in automatically generated programs.
• The 'str' at transduce is a label that does not affect the processing.

## The extensions

### Identifiers

 n: procedure

### Declarations

 declaration -> proc n ( ( progvar )& ) : ( T | void ) ( logicvar ; )* [ formula ( { ( pointerformula )& } )? ] ( { ( progvar ; )* stm } )? [ formula ( { ( pointerformula )& } )? ]

### Statements

 stm -> while [ formula ( { ( pointerformula )& } )? ] ( condexp ) { stm } | return progexp ; | split [ formula ( { ( pointerformula )& } )? ] ( [ formula ( { ( pointerformula )& } )? ] )? ; | proccall ;
 assignment -> lprogexp = proccall

### Expressions

 proccall -> n ( ( progexp )& ) [ formula ]
 boolexp -> n . b | return
 ptrexp -> n . p | return
 setexp -> n . s
 progexp -> condexp | ptrexp
 lprogexp -> lboolexp | lptrexp

• The logicvars after the return type in a procedure declaration are called "logical variables", the formulas constitute the "pre-condition" and "post-condition" of the procedure, and the progvars in the procedure body are "local declarations".
• The formulas at procedure calls are called the "call invariants".
• A return statement can only occur as the last statement of a procedure.
• A return statement must occur if and only if the procedure return type is not void.
• A return expression can only occur in the post-condition of a procedure (as a boolean or a non-null pointer).
• The expression forms 'n . ...' can only be used in procedure call invariants. They refer to the logical variables of the called procedure.
• The scope of a formal procedure argument is the pre-condition and the body of the procedure.
• The scope of a locally declared variable is the body of the procedure.
• Procedure calls are not allowed in multi-assignment statements.
• Identifiers starting with an underscore '_' are reserved for the reduction of the extension constructs into the basic language.
• Every if statement which contains a while, split, or procedure call in one or both branches must be immediately followed by a while, split, or procedure call (unless nothing follows the if statement).
• The form of proc declaration without the procedure body is called a procedure prototype declaration.