A Formal Semantics and an Interactive Environment for Java
by Isabelle Attali
Being both object-oriented and concurrent, the Java model features
interrelated aspects that are critical for the understanding of
an application: objects, static variables, threads, locks, etc.
We want to know how to visualize the various entities that participate
in the execution of a Java program.
These concepts are not easy to understand and to handle for a
programmer, nor easy to formally describe from a designer point
of view.
We address these questions using a formal description of the syntax
and the semantics of the Java language (useful for language designers
and implementers), and as well as an interactive development environment
(useful for programmers). We are using a powerful generic interactive
environment named Centaur (http://www.inria.fr/croap/centaur/centaur.html). Centaur produces a programming environment, dedicated to a
given language, from a formal description of the language.
This research started in spring 1997 with Denis Caromel (Professor
at University Nice - INRIA Sophia Antipolis - CNRS) and Marjorie
Russo, PhD Student), and is pursued at INRIA Sophia Antipolis.
The topology of instance variables within an object-oriented system
can be rather complex. Are they mainly trees? Are there DAGs?
Are there cycles, and where? Those are important questions for
understanding an application. How can a programming environment
provide that information to programmers in a simple and effective
manner, without requiring them to compare reference values within
a text-only debugger? Static variables raise special concerns,
as they can be accessed from objects without an explicit reference
to them.
When it comes to multi-threading and concurrent accesses, that
information becomes even more crucial. How can we effectively
visualize the objects shared by a given thread? Are there any
recursive calls, either directly or through cycles? Do several
threads access a single object at the same time?
We provide solutions to those problems and demonstrate them in
an interactive and graphical environment (shown in following Figure
and also at http://www.inria.fr/croap/java). It allows us to visualize
objects and thread activities at execution in both a textual and
a graphical manner, eg, the topology of the object graph (trees,
DAGs, cycles), thread activities and status, locks, and synchronizations.
Synthetic views give relevant information on status of objects
and interaction between objects and threads.
Using the Centaur system, this graphical environment is derived
from an executable operational semantics of Java: execution a
Java program is, in fact, an interpretation of the semantics with
the program source as data (there is no byte-code, and no virtual
machine is required). Animation of the various views is performed
by messages from the semantics interpreter to the visualization
engines (textual and graphical) in order to show, during execution,
the changes in the structures. No instrumentation is required
from the programmer.
We do not want to compete with commercial systems for Java development.
Instead, we propose two main concepts which can then be exploited
within any Java environment:
- graphical visualization of the object graph topology
- interactive symbolic debugging (no (re-)compilation is necessary).
Future activities include the following directions:
- allow user-control of the interleaving between all threads
- gain in scalability, with an abstract view of the object graph
- benefit from the formal definition the ability to perform formal
verification of Java programs.
Related Projects
With Denis Caromel and Carine Courbis (PhD Student), we recently
started a related research project. Our goal is to facilitate
smart card programming using Java Card, a Java subset that deals
with limited resources (http://www.inria.fr/croap/javacard).
Finally, with Denis Caromel and Romain Guider (PhD Student), we
are also investigating the use of static analysis, based on abstract
interpretation, for distributed and parallel programming in Java.
For this work, we utilize the product of another related research
project: the ProActive PDC Java Library (formerly Java//, Java
Parallel), a Java library for seamless sequential, multithreaded
and distributed programming using Java (http://www.inria.fr/sloop/javall). See also http://www.inria.fr/croap/java.
Please contact:
Isabelle Attali - INRIA
Tel: +33 4 92 38 79 10
E-mail: Isabelle.Attali@sophia.inria.fr
