A dynamic operational semantics for JVML

Abstract

In this papera, we present a dynamic semantics for the Java Virtual Machine Language (JVML). The semantics is specified in an operational style according to the syntactic structure of JVML programs. In order to ascribe meanings to threading, the semantics is made small-step and is structured in two layers: The first layer consists of judgements that capture the semantics of sequential JVML programs in isolation. The second layer consists of judgements that capture the parallel execution of JVML threads. The semantics presented in this paper is a faithful and formal transcription of JVML specification as described in [1]. Besides, we provide full account details for the most technical and tricky aspects of JVML such as multi-threading, synchronization, method invocations, exception handling, object creation, object's fields manipulation, stack manipulation, local variable access, modifiers, etc. The presented semantics is, to the best of our knowledge, the first dynamic semantics of JVML that provides semantics for that many features within the same framework.