--  $Id: java_thread_api.ty,v 1.7 99/08/10 14:49:17 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 specifications for the Thread class          */
-- /* Specified APIs: Thread(), resume(), start(), suspend()                  */
-- /***************************************************************************/ 
program java_thread_api is
use java;
use PSP;

import
   getObject ( ObjectId |- Objects -> Object ) ,
   createExceptionObject (
      Objects, ObjectId |- Identifier, ExceptText -> ObjectId, Objects, Insts ) ,
   setNewThreadStatus (
      ObjectId, ThreadStatus, ClassVariablesL |- Objects -> Objects )
   from java_object_list;

import diff ( _, _ ) , not_eq ( _, _ ) from  prolog() ;

   set ThreadAPI is
   --SC: Performs all the Thread constructors and methods.
   --
   --SC: Specified constructor and methods:
   --SC: Thread()
   --SC: resume()
   --SC: start()
   --SC: suspend()
   --
   --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;

   Thread:
      --RC: Allocates a new Thread object.
      --
      --CS: new Thread();
      ObjL, ClVarL, _, ObjId |-
       identifier "Thread", vals[]
          ->
          ObjL, ClVarL,
          insts[
             clr(
                ObjId, identifier "none", identifier "Thread", env(pairs[], locs[]),
                insts[constructorCall1(identifier "Object", arguments[], ObjId)])], runnable()  ; 

   Resume:
      --RC: Resumes a suspended Thread.
      --
      --CS : OThId.resume();
      getThreadStatus( OThId |- ObjL1 -> suspended(ThStatus) )
      &
      setNewThreadStatus(
         OThId, ThStatus, ClVarL |- ObjL1 -> ObjL1_1 )
      --------------------------------
      ObjL1, ClVarL, _, OThId |-
       identifier "resume", vals[] -> ObjL1_1, ClVarL, insts[], runnable()  ; 

   Start:
      --RC: Causes the thread to pass from the created status into the runnable
      --RC: status to begin its execution (the JVM calls the "run" method).
      --
      --CS: OThId2.start();
      getThreadStatus( OThId |- ObjL1 -> created(_) )  &
      setNewThreadStatus(
         OThId, runnable(), ClVarL |- ObjL1 -> ObjL1_1 )
      --------------------------------
      ObjL1, ClVarL, _, OThId |- identifier "start", vals[] -> ObjL1_1, ClVarL, insts[], runnable()  ; 

   Start_ThreadAlreadyDead_DoNothing:
      --
      --CS: OthId2.start();
      getThreadStatus( OThId |- ObjL1 -> dead() )
      --------------------------------
      ObjL, ClVarL, _, OThId |- identifier "start", vals[] -> ObjL, ClVarL, insts[], runnable()  ; 

   Start_ThreadAlreadyStarted_ExceptionThrown:
      --RC: The IllegalThreadStateException is thrown because the given thread 
      --RC: was already started.
      --
      --CS: OthId2.start();
      getThreadStatus( OThId2 |- ObjL1 -> ThStatus )  &
      not_eq( ThStatus, created(_) )  &  not_eq( ThStatus, dead() )  &
      createExceptionObject(
         ObjL1, OThId1 |-
          identifier "IllegalThreadStateException", exceptText "Method 'start' called on an already started thread."
             ->
             _, ObjL1_1, InstL )
      --------------------------------
      ObjL1, ClVarL, OThId1, OThId2 |-
       identifier "start", vals[] -> ObjL1_1, ClVarL, InstL, runnable()  ; 

   Suspend_ExecutingThread:
      --RC: suspends the current executing thread.
      --
      --CS: OThId.suspend();
      setNewThreadStatus(
         OThId, suspended(runnable()), ClVarL |- ObjL1 -> ObjL1_1 )
      --------------------------------
      ObjL1, ClVarL, OThId, OThId |-
       identifier "suspend", vals[] -> ObjL1_1, ClVarL, insts[], suspended(runnable())  ; 

   Suspend_NotTheExecutingThread:
      --RC: suspends another thread than the current executing thread
      --
      --CS: OThId2.suspend();
      getThreadStatus( OThId2 |- ObjL1 -> ThStatus )  &
      setNewThreadStatus(
         OThId2, suspended(ThStatus), ClVarL |- ObjL1 -> ObjL1_1 )
      --------------------------------
      ObjL1, ClVarL, OThId1, OThId2 |-
       identifier "suspend", vals[] -> ObjL1_1, ClVarL, insts[], runnable()  ; 
               provided diff( OThId1, OThId2 );

      set getThreadStatus is
      --SC : Returns the status for the given thread.
      judgement ObjectId |- Objects -> ThreadStatus;

      GetStatus:
         getObject(
            OThId |- ObjL -> object(OThId, _, _, _, _, activity(ThStatus, _)) )
         --------------------------------
         OThId |- ObjL -> ThStatus  ; 
      end getThreadStatus ;
   end ThreadAPI; 
end java_thread_api