--  $Id: java_api.ty,v 1.7 99/08/10 14:49:13 hnilsson Exp $
-- /***************************************************************************/
-- /*               Copyright (C) 1997-1999 INRIA Sophia-Antipolis            */
-- /*                     I. Attali, D. Caromel and M. Russo                  */
-- /*                                Projet OASIS                             */
-- /*                         Rt. des Lucioles, BP 93,                        */
-- /*                         F-06902 Sophia Antipolis cedex                  */
-- /*                             (+33) 4 92 38 76 31                         */
-- /*                             All rights reserved                         */
-- /***************************************************************************/
--
-- /***************************************************************************/
-- /* Rules for the Java language APIs                                        */
-- /***************************************************************************/
program java_api is
use java;
use PSP;

import
   getDirectAncestor (
      |- OptTypeName -> OptTypeName )
   from java_inheritance;

import
   ObjectAPI (
      Objects, ClassVariablesL, Ref, Ref |-
       Identifier, java -> Objects, ClassVariablesL, Insts, ThreadStatus )
   from java_object_api;

import
   getObjectType ( ObjectId |- Objects -> Identifier )
   from java_object_list;

import
   ThreadAPI (
      Objects, ClassVariablesL, Ref, Ref |-
       Identifier, java -> Objects, ClassVariablesL, Insts, ThreadStatus )
   from java_thread_api;

import
   ThrowableAPI (
      Objects, ClassVariablesL, Ref, Ref |-
       Identifier, java -> Objects, ClassVariablesL, Insts, ThreadStatus )
   from java_throwable_api;

   set APIMethodOrConstructorCall is
   --SC: Performs an API method or constructor call.
   --
   --JC: Object list, Class variable list,
   --JC: Current executing thread reference, Current object reference
   --JC: |- Method or Constructor name, Arguments value list (maybe empty)
   --JC: -> modified object list, modified class variable list, 
   --JC: Continuation instruction list (maybe empty), New current thread status
   judgement
      Objects, ClassVariablesL, Ref, Ref |-
       Identifier, java -> Objects, ClassVariablesL, Insts, ThreadStatus;

   MethodOrConstructorCallTreatment:
      --RC: Gets the object type and dispatches the method
      --RC: or constructor call to the right class.
      getObjectType( ObjId |- ObjL1 -> ClName )
      &
      APIDispatch(
         ObjL1, ClVarL1, OThId, ObjId |-
          ClName, MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus )
      --------------------------------
      ObjL1, ClVarL1, OThId, ObjId |- MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus  ; 
   end APIMethodOrConstructorCall; 

   set APIDispatch is
   --SC: Dispatches the API according to the type of the object that has 
   --SC: called this API. If the API does not belong to the given
   --SC: object type, tries with the direct ancestor of the object 
   --SC: class. Goes up in the hierarchy until the API can be
   --SC: performed (ie the right class has been found) or until the 
   --SC: hierarchy root (ie Object class). In this latter case, that
   --SC: means that the given method or constructor is not an API.
   --
   --JC: Object list, Class variable list, 
   --JC: Current executing thread reference, Current object reference
   --JC: |- Class name, Method or Constructor name, Argument list (maybe empty)
   --JC: -> Modified object list, Modified class variable list, 
   --JC: Continuation instruction list (maybe empty), New current thread status
   judgement
      Objects, ClassVariablesL, Ref, Ref |-
       Identifier, Identifier, java -> Objects, ClassVariablesL, Insts, ThreadStatus;

   ObjectAPI:
      ObjectAPI(
         ObjL1, ClVarL1, OThId, ObjId |- MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus )
      --------------------------------
      ObjL1, ClVarL1, OThId, ObjId |-
       identifier "Object", MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus  ; 

   ThrowableAPI:
      ThrowableAPI(
         ObjL1, ClVarL1, OThId, ObjId |- MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus )
      --------------------------------
      ObjL1, ClVarL1, OThId, ObjId |-
       identifier "Throwable", MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus  ; 

   ThreadAPI:
      ThreadAPI(
         ObjL1, ClVarL1, OThId, ObjId |- MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus )
      --------------------------------
      ObjL1, ClVarL1, OThId, ObjId |-
       identifier "Thread", MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus  ; 

   InheritedMethodLookingForTheDirectAPIAncestor:
      --RC: The given method does not belong to the current class
      --RC: 'ClName1'. So we try to perform the given API on 
      --RC: the direct ancestor 'ClName2' of the given class
      getDirectAncestor(
         |- ClName1 -> ClName2 )  &
      ObjL1, ClVarL1, OThId, ObjId |-
       ClName2, MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus
      --------------------------------
      ObjL1, ClVarL1, OThId, ObjId |-
       ClName1, MethName, ArgL -> ObjL1_1, ClVarL1_1, InstL, ThStatus  ; 
   end APIDispatch; 

   set getAPIObjectAttributes is
   --SC: Gives the attribute names and default values that belong to a 
   --SC: new object for the given class.
   --
   --JC: |- Class name of the new object 
   --JC: -> attribute List (name/default value) 
   judgement |- Identifier -> Pairs;

   Object:
      |- identifier "Object" -> pairs[]  ; 

   Thread:
      |- identifier "Thread" -> pairs[]  ; 

   NullPointerException:
      |- identifier "NullPointerException" -> pairs[]  ; 

   IllegalThreadStateException:
      |- identifier "IllegalThreadStateException" -> pairs[]  ; 

   IllegalMonitorStateException:
      |- identifier "IllegalMonitorStateException" -> pairs[]  ; 

   RuntimeException:
      |- identifier "RuntimeException" -> pairs[]  ; 

   Throwable:
      |- identifier "Throwable" -> pairs[]  ; 

   Exception:
      |- identifier "Exception" -> pairs[]  ; 

   ArithmeticException:
      |- identifier "ArithmeticException" -> pairs[]  ; 

   NegativeArraySizeException:
      |- identifier "NegativeArraySizeException" -> pairs[]  ; 

   IndexOutOfBoundsException:
      |- identifier "IndexOutOfBoundsException" -> pairs[]  ; 

   ArrayStoreException:
      |- identifier "ArrayStoreException" -> pairs[]  ; 
   end getAPIObjectAttributes; 

   set getClassAPIDirectAncestor is
   --SC: Gets the direct API ancestor of the given class.
   --
   --JC: |- Class name 
   --JC: -> Direct ancestor class name
   judgement |- OptTypeName -> OptTypeName;

   Thread_Object:
      |- identifier "Thread" -> identifier "Object"  ; 

   Throwable_Object:
      |- identifier "Throwable" -> identifier "Object"  ; 

   Error_Throwable:
      |- identifier "Error" -> identifier "Throwable"  ; 

   LinkageError_Error:
      |- identifier "LinkageError" -> identifier "Error"  ; 

   VirtualMachineError_Error:
      |- identifier "VirtualMachineError" -> identifier "Error"  ; 

   Exception_Throwable:
      |- identifier "Exception" -> identifier "Throwable"  ; 

   ClassNotFoundException_Exception:
      |- identifier "ClassNotFoundException" -> identifier "Exception"  ; 

   CloneNotSupportedException_Exception:
      |- identifier "CloneNotSupportedException" -> identifier "Exception"  ; 

   IllegalAccessException_Exception:
      |- identifier "IllegalAccessException" -> identifier "Exception"  ; 

   InstantiationException_Exception:
      |- identifier "InstantiationException" -> identifier "Exception"  ; 

   InterruptedException_Exception:
      |- identifier "InterruptedException" -> identifier "Exception"  ; 

   RuntimeException_Exception:
      |- identifier "RuntimeException" -> identifier "Exception"  ; 

   ArithmeticException_RuntimeException:
      |- identifier "ArithmeticException" -> identifier "RuntimeException"  ; 

   ArrayStoreException_RuntimeException:
      |- identifier "ArrayStoreException" -> identifier "RuntimeException"  ; 

   ClassCastException_RuntimeException:
      |- identifier "ClassCastException" -> identifier "RuntimeException"  ; 

   IllegalArgumentException_RuntimeException:
      |- identifier "IllegalArgumentException" -> identifier "RuntimeException"  ; 

   IllegalThreadStateException_IllegalArgumentException:
      |- identifier "IllegalThreadStateException" -> identifier "IllegalArgumentException"  ; 

   NumberFormatException_IllegalArgumentException:
      |- identifier "NumberFormatException" -> identifier "IllegalArgumentException"  ; 

   IllegalMonitorStateException_RuntimeException:
      |- identifier "IllegalMonitorStateException" -> identifier "RuntimeException"  ; 

   IndexOutOfBoundsException_RuntimeException:
      |- identifier "IndexOutOfBoundsException" -> identifier "RuntimeException"  ; 

   NegativeArraySizeException_RuntimeException:
      |- identifier "NegativeArraySizeException" -> identifier "RuntimeException"  ; 

   NullPointerException_RuntimeException:
      |- identifier "NullPointerException" -> identifier "RuntimeException"  ; 

   SecurityException_RuntimeException:
      |- identifier "SecurityException" -> identifier "RuntimeException"  ; 
   end getClassAPIDirectAncestor; 
end java_api