We present the operational semantics of Carmel, a language that models the Java Card Virtual Machine Language. We define a small-step relation between program configurations, including rules for exception handling, array objects and subroutines. We also include the basic structures needed to model object ownership and the Java Card firewall.
展开▼
