Formal Semantics
and Interactive Environment
for Parallel Object-Oriented Programming
The Jitan Environment


Isabelle Attali and Denis Caromel
Marjorie Russo

[Jitan Home Page] [Java Semantics] [Jitan Environment] [A Detailed Example] [To get the semantics] [Documentation] [Javacard] [Contacts]

Jitan Home Page

The Java language gathers two important concepts of the modern programming: object-orientation and concurrency.

A formal definition of the Java Semantics has been defined in an operational style using the Typol formalism. We use Natural Semantics to specify the object oriented and inheritance features of Java and a more traditional little step operational semantics to describe concurrency.
Here is an example of a Typol rule (translated in html by an automatic tool), which describes the semantics of the wait statement.

      --Concrete Syntax: ObjId.wait();
      --RC: Makes the current thread "dormant", adds it to the wait set of the current
      --RC: object and releases the locks on the current object. The current thread is 
      --RC: disabled for thread scheduling until another thread call the notifyAll method
      --RC: on the current object (or the notify method).
      --PC: Checks that the object 'ObjId' is locked by the current executing 
      --PC: thread 'OThId' and determines how many times the object is locked
      --PC: (nb times). 
      --PC: Adds the thread identifier 'OThId' to the wait set of the object 'ObjId'. 
      --PC: Releases the nb locks on the object 'ObjId'.
      getObjectLockInformation( ObjId |- ObjL1 -> OThId, nb )
      &  diff( nb, 0 )  &
      addThreadToTheObjectWaitSet( OThId, ObjId |- ObjL1 -> ObjL1_1 )  &
      releaseObjectLock( ObjId |- ObjL1_1 -> ObjL1_2 )
      ObjL1, ClVarL, OThId, ObjId |- identifier "wait", vals[]
        -> ObjL1_2, ClVarL, insts[synchroWaitEndRelock(ObjId, integer nb)], dormant(ObjId, integer nb)  ; 

                  ENVchangeObjectStatusInStatusList( ObjId );

Using the Centaur system, this semantics permits to generate a Development Environment called Jitan for parallel object-oriented programming and visualization; the specified semantics communicates with the environment thanks to notifications as in the above rule with the ENVchangeObjectStatusInStatusList predicate (in the do clause).
We provide features such as visualization of closure and semantic rules, and animation tools to show the concurrent activities of objects. Another interest of a formal approach is to provide tools to ensure safety properties of Java programs, at the byte code level.

This work is part of a larger project on formal transformation and parallelization for object-oriented languages.

Here is a view of the complete Jitan Environment; we can see:

To get the semantics

Click to get a complete version of the semantics and the environment.
Click to get directly the Typol files and their translation in html.


  • Graphical Visualization of Java Objects, Threads, and Locks
    Isabelle Attali, Denis Caromel, and Marjorie Russo,
    IEEE DS Online, Volume 2, Number 1, January 2001. Local and printable copy

  • From Executable Formal Specification to Java Property Verification
    Proceedings of Formal Techniques for Java Programs - An ECOOP'2000 Workshop, Cannes, June 2000.
    With I. Attali, D. Caromel and H. Nilsson

  • A Formal Executable Semantics for Java
    Proceedings of Formal Underpinnings of Java - An OOPSLA'98 Workshop, Vancouver, October 1998.

  • Vers une Sémantique Formelle de Java
    Actes des journées du PRC/GDR de Programmation , Novembre 1997.

  • Une sémantique formelle de Java
    Soutenance de DEA , Juin 1997.

  • Javacard



    Isabelle Attali
    INRIA Sophia Antipolis BP 93
    06902 Sophia Antipolis - France
    (33) 4 92 38 79 10
    Denis Caromel
    INRIA Sophia Antipolis BP 93
    06902 Sophia Antipolis - France
    (33) 4 92 38 76 31
    Marjorie Russo
    INRIA Sophia Antipolis BP 93
    06902 Sophia Antipolis - France
    (33) 4 92 38 75 58

    Since April, 16, 1998, you are our    th   visitor.
    Thanks for visiting!