--  $Id: java_throwable_api.ty,v 1.7 99/08/10 14:49:25 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                          */
-- /***************************************************************************/
--
-- /***************************************************************************/
-- /* This file contains the API specification for the Throwable class        */
-- /* (the superclass  of all errors and exceptions in the Java language)     */
-- /***************************************************************************/
program java_throwable_api is
use java;
use PSP;

   set ThrowableAPI is
   --SC: Performs methods and constructor for the Throwable class.
   --
   --SC: Specified constructors:
   --SC: Throwable()  
   --SC: Error()
   --SC: Exception()
   --SC: ClassNotFoundException()
   --SC: RuntimeException()
   --SC: ArithmeticException()
   --SC: IllegalArgumentException()
   --SC: IllegalThreadStateException()
   --SC: NumberFormatException()
   --SC: IllegalArgumentException()
   --SC: IllegalMonitorStateException()
   --SC: NullPointerException()
   --
   --JC: Object list, Class variable list, Current executing thread reference,
   --JC: Current object reference
   --JC: |- 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, java -> Objects, ClassVariablesL, Insts, ThreadStatus;

   Throwable:
      --RC: Constructs a new Throwable object with no detail message. The stack
      --RC: trace is automatically filled in.
      --
      --CS: new Throwable();
      ObjL, ClVarL, _, ObjId |-
       identifier "Throwable", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "Throwable", env(pairs[], locs[]),
                insts[constructorCall1(identifier "Object", arguments[], ObjId)])], runnable()  ; 

   Error:
      --RC: Constructs an Exception with no specified detail message to indicate      
      --RC: serious problem that a reasonable application should not try to 
      --RC: catch
      ObjL, ClVarL, _, ObjId |-
       identifier "Error", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "Error", env(pairs[], locs[]),
                insts[constructorCall1(identifier "Throwable", arguments[], ObjId)])], runnable()  ; 

   Exception:
      --RC: Constructs an Exception with no specified detail message to indicate      
      --RC: conditions that a reasonable application might want to catch. 
      ObjL, ClVarL, _, ObjId |-
       identifier "Exception", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "Exception", env(pairs[], locs[]),
                insts[constructorCall1(identifier "Throwable", arguments[], ObjId)])], runnable()  ; 

   ClassNotFoundException:
      --RC: Constructs an ClassNotFoundException with no specified detail 
      --RC: message. This exception is thrown when an application tries to load
      --RC: in a class through its string name but no definition for the class 
      --RC: with the specified name could be found. 
      ObjL, ClVarL, _, ObjId |-
       identifier "ClassNotFoundException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "ClassNotFoundException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "Exception", arguments[], ObjId)])], runnable()  ; 

   RuntimeException:
      --RC: Constructs an RuntimeException with no detail message (Thrown during
      --RC: the normal operation of the Java Virtual Machine)
      ObjL, ClVarL, _, ObjId |-
       identifier "RuntimeException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "RuntimeException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "Exception", arguments[], ObjId)])], runnable()  ; 

   ArithmeticException:
      --RC: Constructs an ArithmeticException with no detail message (Thrown 
      --RC: when an exceptional arithmetic condition has occurred. For example,
      --RC: an integer "divide by zero" throws an instance of this class). 
      ObjL, ClVarL, _, ObjId |-
       identifier "ArithmeticException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "ArithmeticException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "RuntimeException", arguments[], ObjId)])], runnable()  ; 

   IllegalArgumentException:
      --RC: Constructs an IllegalArgumentException with no detail message
      --RC: (Thrown to indicate that a method has been passed an illegal or 
      --RC: inappropriate argument).
      ObjL, ClVarL, _, ObjId |-
       identifier "IllegalArgumentException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "IllegalArgumentException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "RuntimeException", arguments[], ObjId)])], runnable()  ; 

   IllegalThreadStateException:
      --RC: Constructs an IllegalThreadStateException with no detail message
      --RC: (Thrown to indicate that a thread is not in an appropriate state for
      --RC: the requested operation). 
      ObjL, ClVarL, _, ObjId |-
       identifier "IllegalThreadStateException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "IllegalThreadStateException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "IllegalArgumentException", arguments[], ObjId)])], runnable()  ; 

   NumberFormatException:
      --RC: Constructs an NumberFormatException with no detail message
      --RC: (Thrown to indicate that the application has attempted to convert a
      --RC: string to one of the numeric types, but that the string does not 
      --RC: have the appropriate format).
      ObjL, ClVarL, _, ObjId |-
       identifier "NumberFormatException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "NumberFormatException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "IllegalArgumentException", arguments[], ObjId)])], runnable()  ; 

   IllegalMonitorStateException:
      --RC: Constructs an IllegalMonitorStateException with no detail message
      --RC: (Thrown to indicate that a thread has attempted to wait on an object
      --RC: monitor or to notify other threads waiting on an object's monitor 
      --RC: without owning the specified monitor).
      ObjL, ClVarL, _, ObjId |-
       identifier "IllegalMonitorStateException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "IllegalMonitorStateException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "RuntimeException", arguments[], ObjId)])], runnable()  ; 

   NullPointerException:
      --RC: Constructs a NullPointerException with no detail message
      --RC: (Thrown when an application attempts to use null in a case where an
      --RC: object is required).
      ObjL, ClVarL, _, ObjId |-
       identifier "NullPointerException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "NullPointerException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "RuntimeException", arguments[], ObjId)])], runnable()  ; 

   NegativeArraySizeException:
      --RC: Constructs a NegativeArraException with no detail message
      --RC: (Thrown when an application attempts to create an array with negative size.)
      ObjL, ClVarL, _, ObjId |-
       identifier "NegativeArraySizeException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "NegativeArraySizeException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "RuntimeException", arguments[], ObjId)])], runnable()  ; 

   IndexOutOfBoundsException:
      --RC: Constructs an IndexOutOfBoundsException with no detail message.
      --RC: (Thrown when an application attempts to access an element outside of the array.)
      ObjL, ClVarL, _, ObjId |-
       identifier "IndexOutOfBoundsException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "IndexOutOfBoundsException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "RuntimeException", arguments[], ObjId)])], runnable()  ; 

   ArrayStoreException:
      --RC: Constructs a ArrayStoreException with no detail message.
      --RC: (Thrown when an application attempts to store an element in an array whose
      --RC: dynamic type is incompatible with the type of the stored element.)
      ObjL, ClVarL, _, ObjId |-
       identifier "ArrayStoreException", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "ArrayStoreException", env(pairs[], locs[]),
                insts[constructorCall1(identifier "RuntimeException", arguments[], ObjId)])], runnable()  ; 
   end ThrowableAPI; 
end java_throwable_api