Java Formal Semantics

[Jitan Home Page] [Java Semantics] [Jitan Environment] [A Detailed Example] [To get the semantics] [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 of our subset of Java is composed of about 850 inference rules. Some modules are expressed in a Natural Semantics style (especially object-orientation and inheritance features). Some others are expressed in a Structural Operational Semantics style (especially concurrency features).
This semantics is specified using the Typol formalism. This formalism enables to get a modular specification. The figure below presents the different modules which composed our semantic specification of Java and the relations which exist between them. Click on the file names to directly access them...

Program interpretation Concurrency Statements Expressions API Evaluation Inheritance Object list Environment



The semantics of inheritance and dynamic binding is expressed in Natural Semantics (350 rules). For example this next set is dealing with the obtainment of the attribute list of a given type. The second rule is for API types. 

   set makeAttributeList is
   --SC: Determines the attribute list correponding to a given type (useful for
   --SC: an object creation).
   --
   --JC: |- Class name of the new instance 
   --JC: -> Initialized Attribute list 
   judgement |- OptTypeName -> Pairs;

   DeclarationObject_InProgramClasses:
      getClassDeclaration( ClName1 -> ClDec )  &
      getLocalAttributeList( |- ClDec -> LocAttrL )
      &
      getDirectAncestor( |- ClName1 -> ClName2 )
      &
      makeInheritedAttributeList( LocAttrL |- ClName2 -> AttrL )
      --------------------------------
      |- ClName1 -> AttrL  ; 

   DeclarationObject_inAPI:
      getAPIObjectAttributes( |- ClName -> AttrL )
      --------------------------------
      |- ClName -> AttrL  ; 
   end makeAttributeList;


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 (500 rules).
We present here the two main Typol rules defining the evaluation of the assignment expression. 

   ComplexAssignValueToASimpleVariable:
      --RC: Assigns a value to a variable (parameter or local variable).
      --
      --CS: var1 = 10;
      assign(
         ObjL1, ClVarL1, Env1, ObjId |- Ident, TVValue -> ObjL1_1, ClVarL1_1, Env1_1 )
      --------------------------------
      ObjL1, ClVarL1, Env1, _, ObjId, _ |-
       semAssign(empty(), Ident, assignment(), TVValue) -> ObjL1_1, ClVarL1_1, Env1_1, TVValue, insts[], runnable()  ;


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

   ComplexAssignExpressionToASimpleVariable:
      --RC: Evaluates the right member of the assignment before assigning the 
      --RC: variable.
      --
      --CS: var1 = 25 + var2;
      evaluateExpression(
         ObjL, ClVarL, Env, OThId, ObjId, Mode |-
          Expr -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
      --------------------------------
      ObjL, ClVarL, Env, OThId, ObjId, Mode |-
       semAssign(empty(), Ident, AOp, Expr) ->
          ObjL_1, ClVarL_1, Env_1, semAssign(empty(), Ident, AOp, Expr_1), InstL, ThStatus  ;


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.

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

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