PALE syntax

PALE syntax

The basic language
The extensions

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

Restrictions and comments

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

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

Restrictions and comments

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.