The Static Analysis

  We outline in general terms the process of performing the dataflow analysis for the commuting/inverse structures. For the sake of brevity, we have one read and one write in the function - R reads from v.r and W writes to v.w, where v is the current path name parameter of the function. We could extend the analysis to any number of reads and writes by repeating this process for each pair. We would combine the results by taking the maximum of this set of sources. The approach is close to that found in [7].

1.

We start with a general control word V.R, that reads from some part of the structure. Any inverse directions in r or w can be used to restrict the structure of word V. The source can be ignored should Data(V.W) or Data(V.R) be illegal path names, as the statement will not be executed anyway.

2.

We form the path name v.r and convert it back into a control word V'.W, where V' satisfies Data$(V'.W) \equiv$ Data(V.R) and V' < V. We have the additional constraint that Data(V'.R) must be legal. V' is the potential source.

3.

We can now manipulate the control word V', using the analogous commutative properties from the data structure. We need to maximise it subject to V'.W < V.R. This last stage is strongly related to the minimisation of the path name in the normalisation algorithm.

The second step of finding the potential source is in general the most difficult. However, restricting the read and write words to simple directions simplifies this stage significantly, as will be shown in the worked example in section 5. During the analysis legality constraints are imposed on the tail of the control word. The lemmas in the appendix allow us to ignore the head of the word and find the sources of the relative control word, then extend this result to a general one, by prepending any control word.