Property 6: no constructors called.

For all applets $A$ it is the case that no constructor method is called within a call to $\mathit{A.process}$. This can be a crucial property for applets due to the absence of garbage collection in standard JavaCards. Let $\mathsf{constructor}$ express the regular expression predicate .*\..*\.<init>_.* which tests whether the current location is in a constructor method.

$$\begin{array}{l} \phi_{6.1} \;\stackrel {\Delta}{=}\; \maths... ...\; loyaltyB.process\;\neg \mathsf{constructor}\\ \end{array}$$

This property holds of the loyalty applets, but not of the purse applet which can create a new object during a call to the process method (without bad consequences, due to conditions involving data).