The event-driven programming style is pervasive as an efficient method for interacting with the environment. Unfortunately, the event-driven style severely complicates program maintenance and understanding, as it requires each logical flow of control to be fragmented across multiple independent callbacks.
We propose a backward-compatible extension to Java, called TaskJava, which supports lightweight, interleaved computations without foregoing standard control mechanisms like procedures and exceptions. At the same time, TaskJava programs can be automatically translated into efficient event-based code.
This technical report presents, in detail, a formalization of TaskJava. We formalize the operational semantics, typing rules, and modular compilation strategy for a core sublanguage. We then prove a number of properties of this core language, including type soundness, observational equivalence of translated programs, and freedom from certain classes of bugs.
UCLA CSD Technical Report TR060001, January 25, 2006, Revised July 3, 2006.
PDF PostScript © 2006.