This declares that a BitList is a doubly linked list of records, each containing one boolean. The ' bool ' field contains the boolean value, ' data ' declares a successor pointer field, and ' pointer ' declares an auxiliary pointer field. The program heap is considered a finite set of finite trees of records reflecting the structure of the successor fields. A pointer either points to a record of the appropriate type or is 'null'. The formulas specified by the auxiliary pointer fields define where the auxiliary pointers are pointing to, deterministically from the tree structure.
Program variables are either of type data , pointer , or boolean .
The full source code for both PALE and MONA is freely available under the GNU Public Licence . The MONA tool provides the practical foundation for deciding Pointer Assertion Logic. It is an implementation of a decision procedure for weak monadic second-order logic on trees using guided tree automata and other sophisticated techniques. This paper describes the first tool based on transduction using monadic second-order logic on strings. Using that logic, only list-shaped data structures can be expressed.