Property 5: Bonus point are awarded at most once within a transaction.

Transfer of bonus points from a loyalty to the purse does not cause further bonus points to be awarded.

$$\begin{array}{l} \phi_{5} \;\stackrel {\Delta}{=}\; \\ \qu... ...ckage } \mathit{purse.Purse} \vee \mathsf{api} \\ \end{array}$$

That is, calls to the $\mathit{bonusPointsToPurse}$ method does not cause a context switch to any other applet package (but possibly to the JavaCard Runtime Environment - JCRE).

The previous correctness properties were specific to certain applications whereas the following express properties that can be beneficial for any JavaCard applet.