Formal Semantics
and Interactive Environment
for Parallel Object-Oriented Programming
The Jitan Environment

   Wait:
      --Concrete Syntax: ObjId.wait();
      --
      --RC: Makes the current thread "dormant", adds it to the wait set of the current
      --RC: object and releases the locks on the current object. The current thread is 
      --RC: disabled for thread scheduling until another thread call the notifyAll method
      --RC: on the current object (or the notify method).
      --
      --PC: Checks that the object 'ObjId' is locked by the current executing 
      --PC: thread 'OThId' and determines how many times the object is locked
      --PC: (nb times). 
      --PC: Adds the thread identifier 'OThId' to the wait set of the object 'ObjId'. 
      --PC: Releases the nb locks on the object 'ObjId'.
      getObjectLockInformation( ObjId |- ObjL1 -> OThId, nb )
      &  diff( nb, 0 )  &
      addThreadToTheObjectWaitSet( OThId, ObjId |- ObjL1 -> ObjL1_1 )  &
      releaseObjectLock( ObjId |- ObjL1_1 -> ObjL1_2 )
      --------------------------------
      ObjL1, ClVarL, OThId, ObjId |- identifier "wait", vals[]
        -> ObjL1_2, ClVarL, insts[synchroWaitEndRelock(ObjId, integer nb)], dormant(ObjId, integer nb)  ; 

               do
                  ENVchangeObjectStatusInStatusList( ObjId );