FreePascal changes: programmer's documentation
Jochem Berndsen February 2007

Table of Contents
Introduction.............................................................................................................................1 Changes to scanner.................................................................................................................2 Changes to the parser.............................................................................................................2 Statement parser.................................................................................................................2 Expression parser................................................................................................................2 Declaration parser...............................................................................................................2 New and changed classes........................................................................................................3 New metatypes....................................................................................................................3 Postcondition.......................................................................................................................3 Other new classes...............................................................................................................3

Introduction
Comments are used in programming languages to explain the programmer's intent to the programmer self and for other programmers. These are necessary to maintain the program, but they are typically ignored by the compiler of interpreter for the programming language. There are programming languages in which it is possible to provide annotation that is parsed and used by the compiler for that language (for example, Eiffel). On the other hand, there are efforts to extend existing programming languages with possibilities to provide the compiler with information in formal annotation (for example, ESC/Java). There exists two possible routes for transforming the formal annotation in actual results: static and dynamic checking. Static checking is what happens in ESC/Java, in that case the compiler generates a number of proof obligations, which can be checked by a theorem prover. If this theorem prover succeeds, the annotation is correct, and this is verified in compile-time. (ESC/Java is imperfect in this respect) Dynamic checking, on the other hand, means that formal annotation is translated into run-time checks. In the Eiffel programming language, the amount of run-time checks generated can be controlled by switches. We implemented a form of dynamic and static checking in the FreePascal 2.0 compiler in order to see how difficult such a task would be. This document describes what changes are made to the FreePascal compiler. It is possible to insert assertions before, between or after any statement. These are compiled just like regular Assert()-statements. Furthermore, pre- and postconditions of functions, procedures and methods can be given. Class invariants are supported in a limited way. Before loops the programmer can insert an invariant and a variant function. Finally, there is support for propositions and definitions, that act as abbreviations. Missing are the abilities to use quantified expressions like 'for all', inheritance of class invariants, and giving pre- and postconditions of procedures and functions in the unit header instead of the unit implementation.


Changes to scanner
In scanner.pas, all comments are immediately filtered: they do not go to the parser. That means that {@, } are ignored, as well as anything in between. The scanner now recognizes comments that start with {@. A new token has been introduced representing '{@', called _OPEN_FORMAL. The matching } is called _CLOSE_FORMAL. The part between {@ and } is scanned as well. If parsing of formal annotation is switched off (the default), {@ is ignored, and the formal annotation does not enter the parser.

Changes to the parser
Statement parser
The changes to the state ent parser, which can be found in pstatmnt.pas, are more m extensive. What used to be a statement is called a pure_statement. Parsing of the formal annotation before and after statements is in the functions 'statement' and 'formal_annotation' in pstatmnt.pas. The following grammar is parsed: statement := ( assertion* pure_statement assertion* ) | ( (assertion | invariant | bound)* (while_statement | repeat_statement) assertion* ) assertion := '{@' expression? '}' invariant := '{@' 'INV' : expression '}' bound := '{@' 'BND' : expression '}'

Expression parser
The expression parser (pexpr.pas) must be able to recognize specification variables and definitions, but only inside formal annotation. For this purpose a new function is introduced, called comp_expr_in_formal_context, that parses an expression just like comp_expr, but it accepts specification variables and definitions. Specification variables act like regular local variables, they are initialized at the beginning of the function/procedure body.

Declaration parser
The declaration parser now contains a call to read_formal_decs if a _OPEN_FORMAL tok n is e encountered.


The function read_formal_decs can be found in pdecfor al.pas. This file is responsible for m parsing the pre- and postconditions of functions, specification variables and definitions. The following grammar is implemented by this file: declarations := (label_decs | const_decs | type_decs | var_decs | ... | formal_decs)* formal_decs := '{@' formal_dec (';' formal_decs)? '}' formal_dec := ('DEF' definitions) | ('SPECVAR' specvars) | ('PRE' '=' expression) | ('POST' '=' expression) | ('RET' '=' expression) definitions := identifier ( ':' type )? = expression ( ',' definitions )? specvars := identifier ( ':' type )? = expression ( ',' specvars )?

New and changed classes
New metatypes
Specification variables and definitions are both a new metatype. Specification variables are implemented by the class 'tspecvarsym', and definitions by 'tdefinitionsym'. Both classes are in the file 'symsym.pas'.

Statement nodes
The class 'tstatementnode' is extended with the fields 'postcondition' and 'proof_obligation' of type tnode. The field 'postcondition' is nil if no postcondition is supplied for this statement, or an expression if the user specified a postcondition. 'proof_obligation' is used when filling in the proof obligations during the static check. Also, 'synthesized_postcondition' is a new field of 'tstatementnode' (of type boolean). This field is true if the postcondition is calculated (using weakest precondition calculus).

Repetition nodes
The class 'twhilerepeatnode' is extended with the fields 'invariant', 'bound' and 'bound_variable' of type tnode. These hold the invariant, variant function and a load node for the bound variable respectively.


Other new classes
In order to support the proof obligations generated, a couple of new classes are introduced in the file 'proofobl.pas'. These are not exported.
●

twelldefinednode. Representing an expression of the form 'def.E'. A tunarynode, the field 'left' is the expression that should be well defined. The result type is Boolean. tsubstitutionnode. Representing an expression of the form 'E(x := F)'. A tbinarynode. The field 'left' is the expression in which something is substituded, 'right' is the variable to be substituted, and 'subst' is the expression that is substituted for the variable. tnamednode. A tunarynode, the field 'left' is the expression that is named. The field 'thename' is the name of the expression. TDefinition. Representing a definition that is created in order to abbreviate.

●

●

●