We now turn to the problem of performing static analysis of programs written over these general structures. We will be considering recursive functions, and the style will be imperative, rather than functional.
[5] deals with the analysis of array structures, when the program is of the form of a recursive procedure. The procedures consist of sequences of read/write statements or recursive calls. Each call has a recursion guard, a predicate that decides whether the call occurs. Each call is labelled from an alphabet C, so that words over C (control words ) identify each run-time instance of the function body. The predicates must be computable at compile-time and consist of closed form expressions over the number of occurrences of particular labels in the current control word. Restricting the set of recursion guards in a specific way allows exact predicates for the execution of each statement to be derived.
In [4], some of these restrictions are lifted, and the analysis does the best it can under the assumption that there is no knowledge of whether particular recursive calls are followed.
The data flow analysis aims to find, for a particular statement that reads from a point in the data structure, the last statement that wrote to that particular point. They aim to summarise all the data flow information in closed form formulas, independent of the size of the computation. For this they use numbered occurrence languages.
[3] extends this approach to recursively defined structures. The data structure is defined by describing a language over some alphabet, and then associating each distinct word with an item of data. In this context they consider trees, multidimensional arrays and almost free shapes , which are the same as our commuting structures. The recursive program structures that they use are simpler than in [5]. A procedure consists of explore constructs that specify a recursion direction and a predicate over the control word. This has the advantage that the body of the procedure is executed if, and only if, the predicates in the recurse statements hold. The sources are described using the numbered occurrence languages; for the fully commutative structures the formulas obtained are exact. The free and almost free shapes, however, yield approximate solutions; a set of possible sources amongst which the actual source must lie.
For the ASAP structures [10] discusses a system that automatically constructs proofs about whether two paths are possible aliases of each other, e.g given p,q,RE1,RE2, does p.RE1 = q.RE2. This method is suited to general imperative programs where the information obtained about the accesses that each statement makes are of this form. The approach is more appropriate for detecting independent sections of code, rather than tracing the flow of data throughout a section of code.