Towards a Kool Future

Abstract

The K framework was successfully used for defining formal semantics for several practical languages, e.g. C, Java, Java Script, but no language with distributed concurrent objects was defined in K up to now. In this paper we investigate how the model of asynchronous method calls, using the so-called futures for handling the return values, can be added to an existing K definition using the ideas from the Complete Guide to the Future paper. As the running example we use the K definition of KOOL, a pedagogical and research language that captures the essence of the object-oriented programming paradigm. This is a first step toward a generic methodology for modularly adding future-based mechanisms to allow asynchronous method calls.