A binary tree

Since we can simply define an inverse for each direction, finding the source of a read is simplified. For a pair of read/write statements with directions r and w, we apply r to the current path of the particular statement and then apply w^-1 to find the potential source. We can then check that it occurs before the read, and reject it otherwise. We take a simple example:-

F(w) = 		 {
		S: 		 Struct(w.m) =    ...
		T: 		    ...      = Struct(w.p)
		L: 		  F(w.l);
		R: 		  F(w.r);
		 }

Take a typical control word that reads in statement T, denoted X.T. For the purpose of applying direction p, X can have two formats, depending on whether it contains an R. These are X'.R.Lⁿ or Lⁿ, where X' is any control word and $n \geq 0$.

We take the Lⁿ form first, we now want to apply p to it to find the current word of the path name that it accesses. This gives Rⁿ. We now apply the inverse of the write word m to find the control word that accesses that part of the structure. There are two possible inverses - either append an L or a R. The two possible sources of Lⁿ.T are Rⁿ⁺¹.S and Rⁿ.L.S. Both of these control words are executed after the read, so this form has no source. If all the possible writes produce this result then this may indicate that the program is using an uninitialised value.

Now consider X'.R.Lⁿ.T. The current word of the path that it accesses is now X'.L.Rⁿ. Applying the inverse of the write word leaves us with possible sources of X'.L.Rⁿ.L.S and X'.L.Rⁿ⁺¹.S. Both of these occur earlier than the read. However the second is always executed after the first. Therefore it is the source.

It is possible to see how this analysis could be extended to cover read and write words rather than just single directions.