Java Formal Semantics


[Java Semantics Home Page] [Java Semantics] [Java Development Environment] [A Detailed Example] [Documentation] [Contacts]


Java is an object-oriented programming language. This implies that the execution of a Java program creates objects, modifies them and updates object references. The program behavior during the execution is therefore described by the evolution of its object list.

The Semantics

The semantic specification is composed of 400 inference rules describing an operational semantics of Java. Some modules are expressed in a Natural Semantics style (especially object-oriented features). Some others are expressed in a Structural Operational Semantics style (especially concurrency features).

The semantics of inheritance and dynamic binding is expressed in Natural Semantics (200 rules). For example this next rule is dealing with the obtainment of the attribute list of a given type and of the associated static variables.




The Operational Semantics simulates parallelism with a deterministic interleaving of (activities of) concurrent threads (this will change later).
So, the modules describing the actual execution of statements (loops, assignments, ...) are expressed in Structural Operational Semantics (200 rules).
We present here the two main Typol rules defining the evaluation of the assignment expression.



This first rule concerns the case "Var = Value1" where Var is a simple variable. In this case, the "assign" predicate deals with the assigment.



This second rule deals with the case "Name = Expr1". Here "Expr1" is evaluated in "Expr1_1" and, in the next step of execution the instruction to execute will be the first instruction of "InstL1". When this instruction list will be executed, the next instruction to execute will be the evaluation of the expression "Name = Expr1_1".
We need these two rules in order to simulate interleaving between several threads. The assignment is not an atomic statement so we need to foresee a possibility of interleaving during its execution.


[Java Semantics Home Page] [Java Semantics] [Java Development Environment] [A Detailed Example] [Documentation] [Contacts]

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