Example Properties

Below we list a number of properties of the purse and loyalty applets, formulated using our judgement patterns. We introduce the following abbreviations of the applet class names:

$$\begin{array}{rcl} purse & \stackrel {\Delta}{=}& purse.Purs... ...\stackrel {\Delta}{=}& purse.LoyaltyB.LoyaltyB \\ \end{array}$$