Property 7: recursion freeness.

For all non-API methods $m$ it is the case that a call to $m$ never triggers another call to $m$.

$$\begin{array}{l} \phi_{7} \;\stackrel {\Delta}{=}\; m \;\mathsf{never}\;\mathsf{triggers}\; m \end{array}$$

The elapsed time to construct the set of call graphs from the example classes was approximately 16 seconds on a Linux workstation with a Pentium III 1.9 GHz CPU and 256 MB of memory. The resulting call graphs, which includes API program points, consists of 2034 nodes and 3747 edges. The pushdown system generated from these call graphs has approximately 1200 production rules. To check the pushdown system against each of the formulas above, given an initial configuration, took less than one second on the same computer hardware as used for call graph generation.