A structural operational semantics of a non trivial sublanguage of Java is presented. This language includes dynamic creation of objects, blocks, and synchronization of threads. First we introduce a simple operational description of the sequential part of the language, where the memory is treated as an algebra with suitably axiomatized operations. Then, the interaction between threads via a shared memory is described in terms of structures, called "event spaces," whose well-formedness conditions formalize directly the rules given in the Java language specification. Event spaces are included in the operational judgements to develop the semantics of the full multi-threaded sublanguage, which is shown to extend the one for sequential Java conservatively. The result allows sequential programs to be reasoned about in a simplified computational framework without loss of generality.
展开▼
