-- $Id: java_environment.ty,v 1.8 99/08/10 10:43:24 mrusso Exp $
-- /***************************************************************************/
-- /* Copyright (C) 1997-1999 INRIA Sophia-Antipolis */
-- /* I. Attali, D. Caromel and M. Russo */
-- /* Projet OASIS */
-- /* 2004, route des Lucioles, BP 93 */
-- /* F-06902 Sophia Antipolis Cedex */
-- /* (+33) 4 92 38 76 31 */
-- /* All rights reserved */
-- /***************************************************************************/
program java_environment is
use java;
use PSP;
import
getNumberOfDormantAndBlockedThreadsOnTheGivenObject (
ObjectId |- Objects -> integer, integer ) ,
getObject ( ObjectId |- Objects -> Object )
from java_object_list;
import isAThread ( Object -> Bool )
from java_inheritance;
import
getExceptionList ( _ ) , getStackList ( _ ) ,
getStatusList ( _ ) , myAbort ( ) ,
setFirstExceptionList ( _ ) ,
setFirstStackList ( _ ) ,
setFirstStatusList ( _ ) ,
setNewExceptionList ( _ ) ,
setNewStackList ( _ ) , setNewStatusList ( _ ) ,
freeStatusList ( ) , freeStackList ( ) ,
freeExceptionList ( ) ,
freeCompilationUnit ( ) ,
freeExecutingThread ( ) ,
freeAbstractionThreadList ( ) ,
setNewAbstractionThreadList ( _ ) ,
getAbstractionThread ( _ ) ,
getAbstraction ( _ ) ,
getAbstractionThreadList ( _ ) ,
setFirstAbstractionThreadList ( _ )
from jfunctions;
import emit_tree ( _, _ ) , appendtree ( _, _, _ ) , diff ( _, _ ) , receive ( _, _ ) , sup ( _, _ ) , minus ( _, _, _ )
from prolog() ;
import sub ( _, _, _ ) from arith;
var TVObjId: ObjectId;
set ENVgetUserAction is
--SC: Checks if the user has not selected an action on the menu of the
--SC: interpreter. For example, if the "stop" action has been chosen, the
--SC: interpretation of the given program should be stopped immediately.
--SC: This action should be called after each semantics step to the user
--SC: action in consideration.
--
--JC: No action
judgement ();
judgement (Statuss);
SendAWaitingSignal_WaitForAnAnswer:
(StatL) ;
do
emit_tree( "exec", StatL ) & receive( "wait", Message ) &
testMessage( Message );
DoNothing: () ;
end ENVgetUserAction;
set testMessage is
--SC: Tests the received message to see which action is wanted by the user.
--
--JC: String (the received message)
judgement (string);
ContinueMessage_GoOn: ("continue") ;
AbortMessage_Abort:
--c: to prevent from a bug !
myAbort( )
--------------------------------
("abort") ;
(Else) ;
provided diff( Else, "abort" );
end testMessage;
set ENVupdateEnvIfNonDormantOrBlockedThreadOnObject is
--SC: This set communicates with the graphical environment only if there is
--SC: no more blocked or dormant thread on the given object. The lock on the
--SC: object should be removed.
--
--JC: Object reference, Object list, Number of accepted blocked threads
judgement (ObjectId, Objects, integer);
--iJC: Number of dormant thread, Number of blocked threads
--iJC: |- Object reference
judgement integer, integer |- ObjectId;
GetNbOfDormantAndBlockedThreads:
getNumberOfDormantAndBlockedThreadsOnTheGivenObject(
ObjId |- ObjL -> nbDormantThreads, nbBlockedThreads1 ) &
sub( nbBlockedThreads1, nbAcceptedBlockedThreads, nbBlockedThreads1_1 ) &
nbDormantThreads, nbBlockedThreads1_1 |- ObjId
--------------------------------
(ObjId, ObjL, nbAcceptedBlockedThreads) ;
NoDormantOrBlockedThread_CommunicateToTheEnv:
0, 0 |- ObjId ;
do ENVsendRemoveLockOnObject( ObjId );
AtLeastOneDormantThread:
nbDormantThread, _ |- _ ;
provided diff( nbDormantThread, 0 );
AtLeastOneBlockedThread:
_, nbBlockedThread |- _ ;
provided diff( nbBlockedThread, 0 );
end ENVupdateEnvIfNonDormantOrBlockedThreadOnObject;
set ENVsendException is
--SC: Sends a message to the interpretation environment in order to
--SC: visualize the given exception.
--
--JC: New exception.
judgement (Exception);
getExceptionList( ExceptionL )
--------------------------------
(Exception) ;
do
setNewExceptionList( exceptions[Exception.ExceptionL] )
& emit_tree( "exception", exceptions[Exception.ExceptionL] );
end ENVsendException;
set ENVsendRemoveLockOnObject is
--SC: Sends a message to the graphic interpretation environment in order to
--SC: delete the lock node associated with the object specified by the
--SC: given reference.
--
--JC: Object reference
judgement (ObjectId);
(ObjId) ;
do emit_tree( "aLockMustBeRemoved", ObjId );
end ENVsendRemoveLockOnObject;
set ENVsendObjectAndClassVariableLists is
--SC: Sends the objects and the static variable list to the graphic
--SC: interpretation environment.
--SC: Warning : only the classes with static variables are sent to the
--SC: environment. Also sends the object list to the textual interpretation
--SC: environment.
--
--JC1: Objects, Class variable list
judgement (Objects, ClassVariablesL);
--iJC: Class variable list
--iJC: -> Class variable list (only classes with static variable(s))
judgement (ClassVariablesL -> ClassVariablesL);
MainRule_SendMessagesToTheEnvironment:
(ClVarL1 -> ClVarL1_1) &
getObjectsForGraphic( ObjL1, ClVarL1_1 -> ObjL1_1, ClVarL1_2 )
--------------------------------
(ObjL1, ClVarL1) ;
do
emit_tree( "displayMainStructure", mainStruct(ClVarL1_2, ObjL1_1) ) & emit_tree( "objl", ObjL1 )
& emit_tree( "t_objl", ObjL1 );
EmptyClassVariableList:
(classVariablesL[] -> classVariablesL[]) ;
RecursiveRule_EmptyFirstList:
(ClVarL1 -> ClVarL1_1)
--------------------------------
(classVariablesL[classVariables(_, pairs[]).ClVarL1] -> ClVarL1_1) ;
RecursiveRule_TheFirstListIsKeptBecauseNotEmpty:
(ClVarL1 -> ClVarL1_1)
--------------------------------
(classVariablesL[classVariables(ClName, pairs[Pair.PairL]).ClVarL1] ->
classVariablesL[classVariables(ClName, pairs[Pair.PairL]).ClVarL1_1]) ;
end ENVsendObjectAndClassVariableLists;
set getObjectsForGraphic is
--SC: determines the object list for the graphic window dealing with the
--SC: possible abstraction, that is to say, selecting only the objects
--SC: wanted by the user.
--
--JC: Complete object list, Complete variable list
--JC: -> Selected object list, correspondent class variable list.
judgement (Objects, ClassVariablesL -> Objects, ClassVariablesL);
--iJC: Global object list, Abstract object list, Threads interaction list
--iJC: |- Threads to display -> Updated Abstract object list.
judgement
Objects, Objects, ThreadStacks |- AbstractionThreads -> Objects;
NoAbstraction_ReturnsTheGivenLists:
(ObjL, ClVarL -> ObjL, ClVarL) ;
provided getAbstraction( objectNumber 0 );
NewAbstractionToDealWith_ReturnsTheObtainedLists:
getAbstractionThread( OThNumber )
--C: New abstraction on this thread. &
getStackList( stacks(ThreadStacks, _) ) &
ObjL1, objects[], ThreadStacks |- abstractionThreads[OThNumber] -> ObjL2
&
addObjectsCorrespondingToAttributesAndLocalVariables(
ObjL1, ObjL2 |- ObjL2 -> ObjL2_1 ) &
getGoodObjectsOrder( ObjL2_1 -> ObjL2_2 )
&
checkGlobalView( ObjL1, ObjL2_2 -> ObjL3 )
--------------------------------
(ObjL1, ClVarL1 -> ObjL3, ClVarL1) ;
provided getAbstraction( objectNumber 1 )
--C: There is an abstraction on a new thread;
do
setNewAbstractionThreadList( abstractionThreads[OThNumber] );
AnOldAbstractionToDealWith:
getAbstractionThreadList( OThNumbers ) &
getStackList( stacks(ThreadStacks, _) ) &
ObjL1, objects[], ThreadStacks |- OThNumbers -> ObjL2 &
addObjectsCorrespondingToAttributesAndLocalVariables(
ObjL1, ObjL2 |- ObjL2 -> ObjL2_1 ) &
getGoodObjectsOrder( ObjL2_1 -> ObjL2_2 )
&
checkGlobalView( ObjL1, ObjL2_2 -> ObjL3 )
--------------------------------
(ObjL1, ClVarL1 -> ObjL3, ClVarL1) ;
provided getAbstraction( objectNumber 5 );
AddAThreadToAbstraction_ReturnsTheObtainedLists:
getAbstractionThread( OThNumber )
--C: New abstraction on this thread. &
getAbstractionThreadList( OThNumbers1 ) &
getStackList( stacks(ThreadStacks, _) ) &
getAbstractionList( OThNumber |- OThNumbers1 -> OThNumbers1_1
) & ObjL1, objects[], ThreadStacks |- OThNumbers1_1 -> ObjL2
&
addObjectsCorrespondingToAttributesAndLocalVariables(
ObjL1, ObjL2 |- ObjL2 -> ObjL2_1 ) &
getGoodObjectsOrder( ObjL2_1 -> ObjL2_2 )
&
checkGlobalView( ObjL1, ObjL2_2 -> ObjL3 )
--------------------------------
(ObjL1, ClVarL1 -> ObjL3, ClVarL1) ;
provided getAbstraction( objectNumber 2 );
do setNewAbstractionThreadList( OThNumbers1_1 );
ThreadRemovedFromAbstraction_ReturnsTheObtainedLists:
getAbstractionThread( OThNumber )
--C: New abstraction on this thread. &
getAbstractionThreadList( OThNumbers1 ) &
getStackList( stacks(ThreadStacks, _) ) &
getAbstractionThreads(
OThNumber |- OThNumbers1 -> OThNumbers1_1 ) &
ObjL1, objects[], ThreadStacks |- OThNumbers1_1 -> ObjL2 &
addObjectsCorrespondingToAttributesAndLocalVariables(
ObjL1, ObjL2 |- ObjL2 -> ObjL2_1 ) &
getGoodObjectsOrder( ObjL2_1 -> ObjL2_2 )
&
checkGlobalView( ObjL1, ObjL2_2 -> ObjL3 )
--------------------------------
(ObjL1, ClVarL1 -> ObjL3, ClVarL1) ;
provided getAbstraction( objectNumber 3 )
--C: The user wants to remove one thread from the abstraction;
do setNewAbstractionThreadList( OThNumbers1_1 );
ReturnToGlobalView_ReturnsTheGivenLists:
(ObjL, ClVarL -> ObjL, ClVarL) ;
provided getAbstraction( objectNumber 4 );
--C: The user chooses to return to global view.
do
setNewAbstractionThreadList( abstractionThreads[] );
NoMoreThreadToDisplay:
_, ObjL, _ |- abstractionThreads[] -> ObjL ;
OneMoreThreadToDisplay_DetermineTheCorrespondingObjectList:
getObject( objectId(true(), OThNumber) |- ObjL1 -> Thread )
&
addObjectsLinkedToThread(
ObjL1, objects[Thread.ObjL2], objectId(true(), OThNumber) |- ThreadStacks -> ObjL2_1 )
& ObjL1, ObjL2_1, ThreadStacks |- OThNumbers -> ObjL2_2
--------------------------------
ObjL1, ObjL2, ThreadStacks |- abstractionThreads[OThNumber.OThNumbers] -> ObjL2_2 ;
set getAbstractionThreads is
--SC: Remove the given thread number from the list of the threads to
--SC: represent on the abstraction graph.
--
--JC: Thread number |- Thread numbers -> New thread numbers without the given one.
judgement ObjectNumber |- AbstractionThreads -> AbstractionThreads;
ThreadNumberFound_RemovedFromTheList:
OThNumber |- abstractionThreads[OThNumber.OThNumbers] -> OThNumbers ;
RecursiveRule:
OThNumber1 |- OThNumbers1 -> OThNumbers1_1
--------------------------------
OThNumber1 |- abstractionThreads[OThNumber2.OThNumbers1] -> abstractionThreads[OThNumber2.OThNumbers1_1] ;
provided diff( OThNumber1, OThNumber2 );
ThreadNumberNotFound_NotRemovedFromTheList:
_ |- abstractionThreads[] -> abstractionThreads[] ;
end getAbstractionThreads ;
set checkGlobalView is
--SC: Check if the user has clicked on global view.
--
--JC: Global object list, abstracted object list
--JC: -> object list to visualize on the graphic view.
judgement (Objects, Objects -> Objects);
AbstractedViewSelected:
(_, ObjL -> ObjL) ;
provided
getAbstraction( objectNumber i ) & diff( i, 4 );
GlobalViewSelected:
(ObjL, _ -> ObjL) ;
provided getAbstraction( objectNumber 4 );
do
setNewAbstractionThreadList( abstractionThreads[] );
end checkGlobalView ;
set getAbstractionList is
--SC: Check if the given thread number is already in the given
--SC: thread number list
--
--JC: Thread number |- Abstraction thread list -> New abstraction list.
judgement ObjectNumber |- AbstractionThreads -> AbstractionThreads;
ThreadNumberNotFound_AddIt:
OThNumber |- abstractionThreads[] -> abstractionThreads[OThNumber] ;
RecursiveRule_threadNotFound:
OThNumber1 |- OThNumbers1 -> OThNumbers1_1
--------------------------------
OThNumber1 |- abstractionThreads[OThNumber2.OThNumbers1] -> abstractionThreads[OThNumber2.OThNumbers1_1] ;
provided diff( OThNumber1, OThNumber2 );
ThreadNumberFound:
OThNumber |- abstractionThreads[OThNumber.OThNumbers] -> abstractionThreads[OThNumber.OThNumbers] ;
end getAbstractionList ;
set getGoodObjectsOrder is
--SC: Put the threads on top of the abstracted object list
--SC: in order to ease the graphical representation.
--
--JC: Initial object list -> Ordered object list
judgement (Objects -> Objects);
--iJC: Threads, Simple objects |- Abstraction objects
--iJC: -> Updated thread list, Updated simple object list
judgement Objects, Objects |- Objects -> Objects, Objects;
GlobalRule:
objects[], objects[] |- ObjL1 -> Threads, SimpleObjects &
appendtree( Threads, SimpleObjects, ObjL2 )
--------------------------------
(ObjL1 -> ObjL2) ;
EndRule:
Threads, SimpleObjects |- objects[] -> Threads, SimpleObjects ;
RecursiveRuleWithThread:
isAThread( Thread -> true() ) &
Threads1, SimpleObjects1 |- ObjL -> Threads1_1, SimpleObjects1_1
--------------------------------
Threads1, SimpleObjects1 |-
objects[Thread.ObjL] -> objects[Thread.Threads1_1], SimpleObjects1_1 ;
RecursiveRuleWithSimpleObject:
isAThread( Object -> false() ) &
Threads1, SimpleObjects1 |- ObjL -> Threads1_1, SimpleObjects1_1
--------------------------------
Threads1, SimpleObjects1 |-
objects[Object.ObjL] -> Threads1_1, objects[Object.SimpleObjects1_1] ;
end getGoodObjectsOrder ;
end getObjectsForGraphic;
set addLockingThreads is
--SC: Adds the threads which are locking objects of the abstracted
--SC: object list in this list.
--
--JC: Global object list, Abstract object list
--JC: |- Objects to check -> New abstract object list
judgement Objects, Objects |- Objects -> Objects;
NoMoreObjectsToCheck_EmptyList:
_, ObjL |- objects[] -> ObjL ;
RecursiveRuleWithThread:
isAThread( Thread -> true() ) &
ObjL1, ObjL2 |- ObjL3 -> ObjL2_1
--------------------------------
ObjL1, ObjL2 |- objects[Thread.ObjL3] -> ObjL2_1 ;
RecursiveRuleWithSimpleObject_UnlockedObject:
ObjL1, ObjL2 |- ObjL3 -> ObjL2_1
--------------------------------
ObjL1, ObjL2 |-
objects[object(objectId(false(), _), _, _, unlocked(), _, _).ObjL3] -> ObjL2_1 ;
RecursiveRuleWithSimpleObject_LockedObject_ThreadInList:
--RC: If the considered object is a simple one, checks if this object
--RC: is locked and in this case, add the locking thread to the
--RC: abstracted object list.
getObject( OThId |- ObjL2 -> Thread ) &
ObjL1, ObjL2 |- ObjL3 -> ObjL2_1
--------------------------------
ObjL1, ObjL2 |-
objects[object(objectId(false(), _), _, _, locked(OThId, integer nb), _, _).ObjL3] -> ObjL2_1 ;
provided diff( nb, 0 );
RecursiveRuleWithSimpleObject_LockedObject_ThreadNotInList:
--RC: If the considered object is a simple one, checks if this object
--RC: is locked and in this case, add the locking thread to the
--RC: abstracted object list.
getObject( OThId |- ObjL1 -> Thread ) &
ObjL1, objects[Thread.ObjL2] |- ObjL3 -> ObjL4
--------------------------------
ObjL1, ObjL2 |-
objects[object(objectId(false(), _), _, _, locked(OThId, integer nb), _, _).ObjL3] -> ObjL4 ;
provided diff( nb, 0 );
end addLockingThreads;
set addObjectsCorrespondingToAttributesAndLocalVariables is
--SC: Adds in the abstraction object list the objects which are
--SC: the attribute values and local variables of objects that are
--SC: already in the list.
--
--JC: Global object list, Abstract object list
--JC: |- Objects to check -> New abstract object list
judgement Objects, Objects |- Objects -> Objects;
NoMoreObjectsToCheck_EmptyList:
_, ObjL |- objects[] -> ObjL ;
RecursiveRuleWithThread_SeeksForAttributesAndLocalVariables:
isAThread( Thread -> true() ) &
checkForAttributeObjects(
ObjL1, ObjL2, ObjL3 |- Thread -> ObjL2_1, ObjL3_1 ) &
checkForLocalVariablesObjects(
ObjL1, ObjL2_1, ObjL3_1 |- Thread -> ObjL2_2, ObjL3_2 ) &
ObjL1, ObjL2_2 |- ObjL3_2 -> ObjL2_3
--------------------------------
ObjL1, ObjL2 |- objects[Thread.ObjL3] -> ObjL2_3 ;
RecursiveRuleWithSimpleObject_SeeksForAttributes:
isAThread( Object -> false() ) &
checkForAttributeObjects(
ObjL1, ObjL2, ObjL3 |- Object -> ObjL2_1, ObjL3_1 ) &
ObjL1, ObjL2_1 |- ObjL3_1 -> ObjL2_2
--------------------------------
ObjL1, ObjL2 |- objects[Object.ObjL3] -> ObjL2_2 ;
end addObjectsCorrespondingToAttributesAndLocalVariables;
set checkForAttributeObjects is
--SC: Checks the attributes of the given object and adds
--SC: the corresponding objects to the abstraction object list
--SC: and to the list of objects which have not yet been checked.
--
--JC: Global object list, Abstraction object list, Objects to check later
--JC: |- Given object -> New abstraction object list, New list of objects
--JC: to check later
judgement Objects, Objects, Objects |- Object -> Objects, Objects;
GetAttributes_SeekTheCorrespondingObjects_AddThemToTheLists:
getObjectsInPairs(
ObjL1, ObjL2, ObjL3 |- Attributes -> ObjL2_1, ObjL3_1 )
--------------------------------
ObjL1, ObjL2, ObjL3 |- object(_, _, Attributes, _, _, _) -> ObjL2_1, ObjL3_1 ;
end checkForAttributeObjects;
set checkForLocalVariablesObjects is
--SC: Checks the local variables of the given thread and adds
--SC: the corresponding objects to the abstraction object list
--SC: and to the list of objects which have not yet been checked.
--
--JC: Global object list, Abstraction object list, Objects to check later
--JC: |- Given thread -> New abstraction object list, New list of objects
--JC: to check later
judgement Objects, Objects, Objects |- Object -> Objects, Objects;
GetContinuation_SeekTheCorrespondingObjects_AddThemToTheLists:
analyseClosure(
ObjL1, ObjL2, ObjL3 |- Cont -> ObjL2_1, ObjL3_1 )
--------------------------------
ObjL1, ObjL2, ObjL3 |- object(_, _, _, _, _, activity(_, Cont)) -> ObjL2_1, ObjL3_1 ;
set analyseClosure is
--SC: Checks recursively the local variables of the given closure and adds
--SC: the corresponding objects to the abstraction object list
--SC: and to the list of objects which have not yet been checked.
--
--JC: Global object list, Abstraction object list, Objects to check later
--JC: |- Given closure -> New abstraction object list, New list of objects
--JC: to check later
judgement Objects, Objects, Objects |- Clr -> Objects, Objects;
MainRule_CheckTheEnvironmentAndTheInstructionList:
analyseEnv( ObjL1, ObjL2, ObjL3 |- Env -> ObjL2_1, ObjL3_1 )
&
analyseInsts(
ObjL1, ObjL2_1, ObjL3_1 |- Insts -> ObjL2_2, ObjL3_2 )
--------------------------------
ObjL1, ObjL2, ObjL3 |- clr(_, _, _, Env, Insts) -> ObjL2_2, ObjL3_2 ;
set analyseEnv is
--SC: Checks the local variable and parameters and adds
--SC: the corresponding objects to the abstraction object list
--SC: and to the list of objects which have not yet been checked.
--
--JC: Global object list, Abstraction object list, Objects to check later
--JC: |- Environment -> New abstraction object list, New list of objects
--JC: to check later
judgement Objects, Objects, Objects |- Env -> Objects, Objects;
MainRule_CheckTheParametersAndLocalVariables:
getObjectsInPairs(
ObjL1, ObjL2, ObjL3 |- Params -> ObjL2_1, ObjL3_1 ) &
getObjectsInPairs(
ObjL1, ObjL2_1, ObjL3_1 |- Pairs -> ObjL2_2, ObjL3_2 )
--------------------------------
ObjL1, ObjL2, ObjL3 |- env(Params, locs[Pairs._]) -> ObjL2_2, ObjL3_2 ;
end analyseEnv ;
set analyseInsts is
--SC: Checks recursively the given instruction list and adds
--SC: the corresponding objects to the abstraction object list
--SC: and to the list of objects which have not yet been checked.
--
--JC: Global object list, Abstraction object list, Objects to check later
--JC: |- Instruction list -> New abstraction object list, New list of objects
--JC: to check later
judgement
Objects, Objects, Objects |- Insts -> Objects, Objects;
EmptyInstructionList_NoObjectToAdd:
_, ObjL1, ObjL2 |- insts[] -> ObjL1, ObjL2 ;
ClosureAsFirstInstruction_AnalyseIt:
analyseClosure(
ObjL1, ObjL2, ObjL3 |- clr(_, _, _, Env, Insts) -> ObjL2_1, ObjL3_1 )
--------------------------------
ObjL1, ObjL2, ObjL3 |- insts[clr(_, _, _, Env, Insts)._] -> ObjL2_1, ObjL3_1 ;
SemBlockAsFirstInstruction_AnalyseIt:
getObjectsInPairs(
ObjL1, ObjL2, ObjL3 |- Pairs -> ObjL2_1, ObjL3_1 ) &
analyseInsts(
ObjL1, ObjL2_1, ObjL3_1 |- Insts -> ObjL2_2, ObjL3_2 )
--------------------------------
ObjL1, ObjL2, ObjL3 |-
insts[semBlock(Insts, blockEnv(_, _, Pairs))._] -> ObjL2_2, ObjL3_2 ;
TryBlockExecutionAsFirstInstruction_AnalyseIt:
ObjL1, ObjL2, ObjL3 |-
insts[semBlock(Insts, blockEnv(_, _, Pairs))._] -> ObjL2_1, ObjL3_1
--------------------------------
ObjL1, ObjL2, ObjL3 |-
insts[tryBlockExecution(semBlock(Insts, blockEnv(_, _, Pairs)), _, _)._] -> ObjL2_1, ObjL3_1 ;
TryCatchBlockExecutionAsFirstInstruction_AnalyseIt:
ObjL1, ObjL2, ObjL3 |-
insts[semBlock(Insts, blockEnv(_, _, Pairs))._] -> ObjL2_1, ObjL3_1
--------------------------------
ObjL1, ObjL2, ObjL3 |-
insts[tryCatchBlockExecution(_, semBlock(Insts, blockEnv(_, _, Pairs)), _)._] -> ObjL2_1, ObjL3_1 ;
TryFinallyExecutionAsFirstInstruction_AnalyseIt:
ObjL1, ObjL2, ObjL3 |-
insts[semBlock(Insts, blockEnv(_, _, Pairs))._] -> ObjL2_1, ObjL3_1
--------------------------------
ObjL1, ObjL2, ObjL3 |-
insts[tryFinallyExecution(semBlock(Insts, blockEnv(_, _, Pairs)))._] -> ObjL2_1, ObjL3_1 ;
OtherFirstInstruction_NoObjectToAdd:
_, ObjL1, ObjL2 |- insts[_._] -> ObjL1, ObjL2 ;
end analyseInsts ;
end analyseClosure ;
end checkForLocalVariablesObjects;
set getObjectsInPairs is
--SC: Selects the objects which are referenced in the given
--SC: attribute list.
--
--JC: Global object list, Abstraction object list, Objects to check later
--JC: |- Attribute list -> New Abstraction object list, New list of
--JC: objects to check later
judgement Objects, Objects, Objects |- Pairs -> Objects, Objects;
NoMoreAttributes:
_, ObjL1, ObjL2 |- pairs[] -> ObjL1, ObjL2 ;
ObjectAttribute_AlreadyInAbstractionObjectList:
getObject( TVObjId |- ObjL2 -> Object ) &
ObjL1, ObjL2, ObjL3 |- Pairs -> ObjL2_1, ObjL3_1
--------------------------------
ObjL1, ObjL2, ObjL3 |- pairs[pair(_, TVObjId).Pairs] -> ObjL2_1, ObjL3_1 ;
ObjectAttribute_NotAlreadyInAbstractionObjectList:
getObject( TVObjId |- ObjL1 -> Object ) &
appendtree( ObjL2, objects[Object], ObjL2_1 ) & appendtree( ObjL3, objects[Object], ObjL3_1 )
& ObjL1, ObjL2_1, ObjL3_1 |- Pairs -> ObjL2_2, ObjL3_2
--------------------------------
ObjL1, ObjL2, ObjL3 |- pairs[pair(_, TVObjId).Pairs] -> ObjL2_2, ObjL3_2 ;
NotAnObjectAttribute:
ObjL1, ObjL2, ObjL3 |- Pairs -> ObjL2_1, ObjL3_1
--------------------------------
ObjL1, ObjL2, ObjL3 |- pairs[_.Pairs] -> ObjL2_1, ObjL3_1 ;
end getObjectsInPairs;
set addObjectsLinkedToThread is
--SC: Determines the objects which must be displayed in the graph
--SC: corresponding to the given thread reference.
--
--JC: Global object list, Abstract object list, Considered thread reference
--JC: |- Threads interaction list -> Updated Abstract object list.
judgement Objects, Objects, ObjectId |- ThreadStacks -> Objects;
--iJC: Global object list, Abstract object list |- List of objects to add
--iJC: -> Updated abstract object list
judgement Objects, Objects |- ObjectIds -> Objects;
DeterminesTheObjectsLinkedToTheThreadByAMethodCall:
getThreadStack( OThId |- ThreadStacks -> threadStack(OThId, ObjectIds) )
& ObjL1, ObjL2 |- ObjectIds -> ObjL2_1
--------------------------------
ObjL1, ObjL2, OThId |- ThreadStacks -> ObjL2_1 ;
EmptyObjectsReferenceList:
_, ObjL |- objectIds[] -> ObjL ;
RecursiveRule_TheObjectToAddIsAlreadyInTheAbstractObjectList:
getObject( ObjId |- ObjL2 -> Object ) &
ObjL1, ObjL2 |- ObjIds -> ObjL2_1
--------------------------------
ObjL1, ObjL2 |- objectIds[ObjId.ObjIds] -> ObjL2_1 ;
RecursiveRule_TheObjectToAddIsNotInTheList_AddsIt:
getObject( ObjId |- ObjL1 -> Object ) &
appendtree( ObjL2, objects[Object], ObjL2_1 ) &
ObjL1, ObjL2_1 |- ObjIds -> ObjL2_2
--------------------------------
ObjL1, ObjL2 |- objectIds[ObjId.ObjIds] -> ObjL2_2 ;
end addObjectsLinkedToThread;
set getThreadStack is
judgement ObjectId |- ThreadStacks -> ThreadStack;
SoughtThreadStack_ReturnsIt:
OThId |- threadStacks[threadStack(OthId, ObjIds)._] -> threadStack(OthId, ObjIds) ;
RecursiveRule_NotTheSoughtThread:
OThId1 |- ThreadStacks -> ThreadStack
--------------------------------
OThId1 |- threadStacks[threadStack(OThId2, _).ThreadStacks] -> ThreadStack ;
provided diff( OThId1, OThId2 );
end getThreadStack;
set ENVsendNewObject is
--SC: When an object is created, sends it to the textual and graphic
--SC: interpretation environment.
--
--JC: Object
judgement (Object);
(Obj) ;
do emit_tree( "newCreatedObject", Obj );
end ENVsendNewObject;
set ENVsendStackList is
--SC: Sends the list of cross references between objects and threads to the
--SC: interpretation environment.
--
--JC: Stack list
judgement (Stacks);
(StackL) ;
do emit_tree( "stack", StackL );
end ENVsendStackList;
set ENVsendStatusList is
--SC: In case of the creation of an object, sends it to the textual and
--SC: graphic interpretation environment.
--
--JC: Status list
judgement (Statuss);
(StatL) ;
do emit_tree( "stats", StatL );
end ENVsendStatusList;
set ENVsendObjectList is
--SC: Sends the object list to the textual interpretation environment.
--
--JC: Objects
judgement (Objects);
(ObjL) ;
do emit_tree( "objl", ObjL ) & emit_tree( "t_objl", ObjL );
end ENVsendObjectList;
set ENVsendCurrentExecutingThread is
--SC: Communicates to the graphic interpretation environment the thread
--SC: which is going to be "executing".
--
--JC: Objects, New executing thread reference
judgement (Objects, ObjectId);
GetTheCorrespondingObject_SendIt:
getObject( ObjId |- ObjL -> Obj )
--------------------------------
(ObjL, ObjId) ;
do emit_tree( "currentExecutingThread", Obj );
end ENVsendCurrentExecutingThread;
set ENVsendDeadThread is
--SC: Communicates to the graphic interpretation environment the new "dead"
--SC: thread.
--
--JC: Objects, Dead thread reference
judgement (Objects, ObjectId);
GetTheCorrespondingThread_SendIt:
getObject( OThId |- ObjL -> Thr )
--------------------------------
(ObjL, OThId) ;
do emit_tree( "aThreadIsDead", Thr );
end ENVsendDeadThread;
set ENVinitializeStatusAndStackAndExceptionLists is
--SC: Initializes the lists in order to save them as Prolog global variables.
--
--JC: nothing
judgement ();
() ;
do
ENVsendStatusList(
statuss(
objectIds[], objectIds[objectId(true(), objectNumber 0)], objectIds[], objectIds[], objectIds[], objectIds[], objectIds[],
objectIds[], objectIds[]) ) &
setFirstStatusList(
statuss(
objectIds[], objectIds[objectId(true(), objectNumber 0)], objectIds[], objectIds[], objectIds[], objectIds[], objectIds[],
objectIds[], objectIds[]) ) &
setNewStatusList(
statuss(
objectIds[], objectIds[objectId(true(), objectNumber 0)], objectIds[], objectIds[], objectIds[], objectIds[], objectIds[],
objectIds[], objectIds[]) ) &
ENVsendStackList(
stacks(
threadStacks[threadStack(objectId(true(), objectNumber 0), objectIds[])],
objectStacks[objectStack(objectId(true(), objectNumber 0), objectIds[])]) ) &
setFirstStackList(
stacks(
threadStacks[threadStack(objectId(true(), objectNumber 0), objectIds[])],
objectStacks[objectStack(objectId(true(), objectNumber 0), objectIds[])]) ) &
setNewStackList(
stacks(
threadStacks[threadStack(objectId(true(), objectNumber 0), objectIds[])],
objectStacks[objectStack(objectId(true(), objectNumber 0), objectIds[])]) ) &
setFirstExceptionList( exceptions[] ) &
setFirstAbstractionThreadList( abstractionThreads[] )
&
setNewAbstractionThreadList( abstractionThreads[] );
end ENVinitializeStatusAndStackAndExceptionLists;
set ENVfreeEnvironment is
--SC: Free the Prolog global variables.
--
--JC: nothing
judgement ();
() ;
do
freeStatusList( ) &
freeStackList( ) &
freeExceptionList( ) &
freeAbstractionThreadList( ) &
freeCompilationUnit( ) &
freeExecutingThread( );
end ENVfreeEnvironment;
set ENVdeleteAThreadFromStackList is
--SC: Takes the new executing thread reference and deletes it from the stack
--SC: list in order to add it incrementally during the closures imbrication
--SC: analysis.
--
--JC: Thread reference
judgement (ObjectId);
--iJC: Thread reference
--iJC: |- Stack list
--iJC: -> Updated stack list
judgement ObjectId |- Stacks -> Stacks;
EntryRule_GetTheCurrentStackList:
OThId |- StackL1 -> StackL1_1
--------------------------------
(OThId) ;
provided getStackList( StackL1 );
do setNewStackList( StackL1_1 );
UpdateTheStackList:
ENVdeleteAThreadStackFromList( OThId |- ThrStackL1 -> ThrStackL1_1 )
&
ENVdeleteAThreadFromStacks( OThId |- ObjStackL1 -> ObjStackL1_1 )
--------------------------------
OThId |- stacks(ThrStackL1, ObjStackL1) -> stacks(ThrStackL1_1, ObjStackL1_1) ;
end ENVdeleteAThreadFromStackList;
set ENVdeleteAThreadStackFromList is
--SC: Erases a thread stack from the threads stack list.
--
--JC: Thread reference
--JC: |- Threads stack list
--JC: -> updated threads stack list
judgement ObjectId |- ThreadStacks -> ThreadStacks;
FoundTheThreadStack_EraseIt:
OThId |- threadStacks[threadStack(OThId, _).ThStackL] -> threadStacks[threadStack(OThId, objectIds[]).ThStackL] ;
RecursiveRule_NotTheGoodThread:
OThId1 |- ThStackL1 -> ThStackL1_1
--------------------------------
OThId1 |- threadStacks[threadStack(OThId2, ThStack).ThStackL1] ->
threadStacks[threadStack(OThId2, ThStack).ThStackL1_1] ;
provided diff( OThId1, OThId2 );
end ENVdeleteAThreadStackFromList;
set ENVdeleteAThreadFromStacks is
--SC: Erases a thread reference from all the different object stacks.
--
--JC: Thread reference
--JC: |- Objects stack list
--JC: -> Updated objects stack list
judgement ObjectId |- ObjectStacks -> ObjectStacks;
RecursiveRule_EraseTheThreadReferenceFromOneObjectStack:
ENVeraseThreadFromObjectsReferenceList(
OThId |- ObjStack1 -> ObjStack1_1 ) &
OThId |- ObjStackL1 -> ObjStackL1_1
--------------------------------
OThId |- objectStacks[objectStack(ObjId, ObjStack1).ObjStackL1] ->
objectStacks[objectStack(ObjId, ObjStack1_1).ObjStackL1_1] ;
EmptyObjectsStackList_EndOfRecursion:
_ |- objectStacks[] -> objectStacks[] ;
end ENVdeleteAThreadFromStacks;
set ENVeraseThreadFromObjectsReferenceList is
--SC: Erases a thread reference from an objects reference list.
--
--JC: Thread reference
--JC: |- References
--JC: -> Updated reference list
judgement ObjectId |- ObjectIds -> ObjectIds;
RecursiveRule_EraseTheThreadReference:
OThId |- ObjIdL1 -> ObjIdL1_1
--------------------------------
OThId |- objectIds[OThId.ObjIdL1] -> ObjIdL1_1 ;
RecursiveRule_NotTheSoughtThreadReference:
OThId1 |- ObjIdL1 -> ObjIdL1_1
--------------------------------
OThId1 |- objectIds[OThId2.ObjIdL1] -> objectIds[OThId2.ObjIdL1_1] ;
provided diff( OThId1, OThId2 );
EmptyList_EndOfRecursion: _ |- objectIds[] -> objectIds[] ;
end ENVeraseThreadFromObjectsReferenceList;
set ENVaddTheCrossedReferencesToTheInteractionStacks is
--SC: When entering in a method call, adds the reference of the object on
--SC: which the method was called in the visiting object list of the current
--SC: executing thread. Adds the current executing thread reference in the
--SC: stack of the object on which the method was called.
--
--JC: Thread reference, Object reference
judgement (ObjectId, ObjectId);
--iJC: Thread reference, Object reference
--iJC: |- Stacks
--iJC: -> Updated stack list
judgement ObjectId, ObjectId |- Stacks -> Stacks;
GetTheStacks_UpdateThem:
OThId, ObjId |- StackL1 -> StackL1_1
--------------------------------
(OThId, ObjId) ;
provided getStackList( StackL1 );
do
ENVsendStackList( StackL1_1 ) &
setNewStackList( StackL1_1 );
UpdateTheStacks:
ENVaddObjectReferenceInThreadStack(
OThId, ObjId |- ThrStackL1 -> ThrStackL1_1 ) &
ENVaddThreadReferenceInObjectStack(
OThId, ObjId |- ObjStackL1 -> ObjStackL1_1 )
--------------------------------
OThId, ObjId |- stacks(ThrStackL1, ObjStackL1) -> stacks(ThrStackL1_1, ObjStackL1_1) ;
end ENVaddTheCrossedReferencesToTheInteractionStacks;
set ENVaddObjectReferenceInThreadStack is
--SC: When entering in a method call, adds the reference of the object on
--SC: which the method was called in the visiting object list of the current
--SC: executing thread.
--
--JC: Thread reference, Object reference
--JC: |- Threads stack list
--JC: -> Updated threads stack list
judgement ObjectId, ObjectId |- ThreadStacks -> ThreadStacks;
FindTheGoodThread_AddTheObjectReferenceToTheStack:
ENVaddObjectReferenceToAGivenList(
ObjId |- ThrStack1 -> ThrStack1_1 )
--------------------------------
OThId, ObjId |-
threadStacks[threadStack(OThId, ThrStack1).ThrStackL] -> threadStacks[threadStack(OThId, ThrStack1_1).ThrStackL] ;
RecursiveRule_NotTheGoodThread:
OThId1, ObjId |- ThrStackL1 -> ThrStackL1_1
--------------------------------
OThId1, ObjId |-
threadStacks[threadStack(OThId2, ThrStack).ThrStackL1] -> threadStacks[threadStack(OThId2, ThrStack).ThrStackL1_1] ;
provided diff( OThId1, OThId2 );
end ENVaddObjectReferenceInThreadStack;
set ENVaddThreadReferenceInObjectStack is
--SC: When entering in a method call, adds the current executing thread
--SC: reference in the stack of the object on which the method was called.
--
--JC: Thread reference, Object reference
--JC: |- Objects stack list
--JC: -> Updated objects stack list
judgement ObjectId, ObjectId |- ObjectStacks -> ObjectStacks;
FindTheGoodObject_AddTheThreadReferenceToTheStack:
ENVaddObjectReferenceToAGivenList(
OThId |- ObjStack1 -> ObjStack1_1 )
--------------------------------
OThId, ObjId |-
objectStacks[objectStack(ObjId, ObjStack1).ObjStackL] -> objectStacks[objectStack(ObjId, ObjStack1_1).ObjStackL] ;
RecursiveRule_NotTheGoodObject:
OThId, ObjId1 |- ObjStackL1 -> ObjStackL1_1
--------------------------------
OThId, ObjId1 |-
objectStacks[objectStack(ObjId2, ObjStack).ObjStackL1] -> objectStacks[objectStack(ObjId2, ObjStack).ObjStackL1_1] ;
provided diff( ObjId1, ObjId2 );
end ENVaddThreadReferenceInObjectStack;
set ENVupdateThreadStatusList is
--SC: Updates the thread part of the status list and communicates it to the
--SC: environment.
--
--JC: Thread reference, Old status, New status
judgement (ObjectId, ThreadStatus, ThreadStatus);
--iJC: Thread reference, Old status, New status
--iJC: |- Status list
--iJC: -> Updated status list
judgement ObjectId, ThreadStatus, ThreadStatus |- Statuss -> Statuss;
GetStatusList_UpdateIt:
OThId, OldThrStatus, NewThrStatus |- StatL1 -> StatL1_1
--------------------------------
(OThId, OldThrStatus, NewThrStatus) ;
provided getStatusList( StatL1 );
do
ENVsendStatusList( StatL1_1 ) &
setNewStatusList( StatL1_1 );
RemoveThreadReferenceFromOldStatus_AddItToNewStatus:
ENVremoveThreadReferenceFromStatusList(
OThId, OldThrStatus |- StatL1 -> StatL1_1 ) &
ENVaddThreadReferenceToStatusList(
OThId, NewThrStatus |- StatL1_1 -> StatL1_2 )
--------------------------------
OThId, OldThrStatus, NewThrStatus |- StatL1 -> StatL1_2 ;
end ENVupdateThreadStatusList;
set ENVchangeObjectStatusInStatusList is
--SC: Updates the thread part of the status list and communicates it to the
--SC: environment. An object can be unlocked or locked. So if the given
--SC: object was unlocked it becomes locked.
--
--JC: Object reference
judgement (ObjectId);
--iJC: Object reference
--iJC: |- Status list
--iJC: -> Updated status list
judgement ObjectId |- Statuss -> Statuss;
GetStatusList_UpdateIt:
ObjId |- StatL1 -> StatL1_1
--------------------------------
(ObjId) ;
provided getStatusList( StatL1 );
do
ENVsendStatusList( StatL1_1 ) &
setNewStatusList( StatL1_1 );
ChangeTheObjectStatus:
ENVremoveObjectReferenceFromReferenceList(
ObjId1 |- unlocked1 -> unlocked1_1 ) &
ENVaddObjectReferenceToAGivenList( ObjId1 |- locked1 -> locked1_1 )
--------------------------------
ObjId1 |- statuss(created, runnable, executing, blocked, dormant, suspended, dead, unlocked1, locked1) ->
statuss(created, runnable, executing, blocked, dormant, suspended, dead, unlocked1_1, locked1_1) ;
ENVremoveObjectReferenceFromReferenceList(
ObjId |- locked1 -> locked1_1 ) &
ENVaddObjectReferenceToAGivenList( ObjId |- unlocked1 -> unlocked1_1 )
--------------------------------
ObjId |- statuss(created, runnable, executing, blocked, dormant, suspended, dead, unlocked1, locked1) ->
statuss(created, runnable, executing, blocked, dormant, suspended, dead, unlocked1_1, locked1_1) ;
end ENVchangeObjectStatusInStatusList;
set ENVremoveThreadReferenceFromStatusList is
--SC: Removes a thread reference from the status list, more precisely it
--SC: removes it from the threads reference list attached to the given
--SC: status.
--
--JC: Thread reference, Thread status
--JC: |- Status list
--JC: -> Updated status list
judgement ObjectId, ThreadStatus |- Statuss -> Statuss;
RemoveFromCreatedThreadList:
ENVremoveObjectReferenceFromReferenceList(
OThId |- created1 -> created1_1 )
--------------------------------
OThId, created(_) |-
statuss(created1, runnable, executing, blocked, dormant, suspended, dead, unlocked, locked) ->
statuss(created1_1, runnable, executing, blocked, dormant, suspended, dead, unlocked, locked) ;
RemoveFromRunnableThreadList:
ENVremoveObjectReferenceFromReferenceList(
OThId |- runnable1 -> runnable1_1 )
--------------------------------
OThId, runnable() |-
statuss(created, runnable1, executing, blocked, dormant, suspended, dead, unlocked, locked) ->
statuss(created, runnable1_1, executing, blocked, dormant, suspended, dead, unlocked, locked) ;
ENVremoveObjectReferenceFromReferenceList(
OThId |- executing1 -> executing1_1 )
--------------------------------
OThId, executing() |-
statuss(created, runnable, executing1, blocked, dormant, suspended, dead, unlocked, locked) ->
statuss(created, runnable, executing1_1, blocked, dormant, suspended, dead, unlocked, locked) ;
ENVremoveObjectReferenceFromReferenceList(
OThId |- blocked1 -> blocked1_1 )
--------------------------------
OThId, blocked(_) |-
statuss(created, runnable, executing, blocked1, dormant, suspended, dead, unlocked, locked) ->
statuss(created, runnable, executing, blocked1_1, dormant, suspended, dead, unlocked, locked) ;
ENVremoveObjectReferenceFromReferenceList(
OThId |- dormant1 -> dormant1_1 )
--------------------------------
OThId, dormant(_, _) |-
statuss(created, runnable, executing, blocked, dormant1, suspended, dead, unlocked, locked) ->
statuss(created, runnable, executing, blocked, dormant1_1, suspended, dead, unlocked, locked) ;
ENVremoveObjectReferenceFromReferenceList(
OThId |- suspended1 -> suspended1_1 )
--------------------------------
OThId, suspended(_) |-
statuss(created, runnable, executing, blocked, dormant, suspended1, dead, unlocked, locked) ->
statuss(created, runnable, executing, blocked, dormant, suspended1_1, dead, unlocked, locked) ;
end ENVremoveThreadReferenceFromStatusList;
set ENVaddThreadReferenceToStatusList is
--SC: Adds a thread identifier to the status list.
--
--JC: Thread reference, New status
--JC: |- Status list
--JC: -> Updated status list
judgement ObjectId, ThreadStatus |- Statuss -> Statuss;
ENVaddObjectReferenceToAGivenList( OThId |- created1 -> created1_1 )
--------------------------------
OThId, created(_) |-
statuss(created1, runnable, executing, blocked, dormant, suspended, dead, unlocked, locked) ->
statuss(created1_1, runnable, executing, blocked, dormant, suspended, dead, unlocked, locked) ;
ENVaddObjectReferenceToAGivenList( OThId |- runnable1 -> runnable1_1 )
--------------------------------
OThId, runnable() |-
statuss(created, runnable1, executing, blocked, dormant, suspended, dead, unlocked, locked) ->
statuss(created, runnable1_1, executing, blocked, dormant, suspended, dead, unlocked, locked) ;
ENVaddObjectReferenceToAGivenList( OThId |- executing1 -> executing1_1
)
--------------------------------
OThId, executing() |-
statuss(created, runnable, executing1, blocked, dormant, suspended, dead, unlocked, locked) ->
statuss(created, runnable, executing1_1, blocked, dormant, suspended, dead, unlocked, locked) ;
ENVaddObjectReferenceToAGivenList( OThId |- blocked1 -> blocked1_1 )
--------------------------------
OThId, blocked(_) |-
statuss(created, runnable, executing, blocked1, dormant, suspended, dead, unlocked, locked) ->
statuss(created, runnable, executing, blocked1_1, dormant, suspended, dead, unlocked, locked) ;
ENVaddObjectReferenceToAGivenList( OThId |- dormant1 -> dormant1_1 )
--------------------------------
OThId, dormant(_, _) |-
statuss(created, runnable, executing, blocked, dormant1, suspended, dead, unlocked, locked) ->
statuss(created, runnable, executing, blocked, dormant1_1, suspended, dead, unlocked, locked) ;
ENVaddObjectReferenceToAGivenList( OThId |- suspended1 -> suspended1_1
)
--------------------------------
OThId, suspended(_) |-
statuss(created, runnable, executing, blocked, dormant, suspended1, dead, unlocked, locked) ->
statuss(created, runnable, executing, blocked, dormant, suspended1_1, dead, unlocked, locked) ;
ENVaddObjectReferenceToAGivenList( OThId |- dead1 -> dead1_1 )
--------------------------------
OThId, dead() |-
statuss(created, runnable, executing, blocked, dormant, suspended, dead1, unlocked, locked) ->
statuss(created, runnable, executing, blocked, dormant, suspended, dead1_1, unlocked, locked) ;
end ENVaddThreadReferenceToStatusList;
set ENVremoveObjectReferenceFromReferenceList is
--SC: Removes an object identifier from an object identifier list.
--
--JC: Object reference
--JC: |- Objects reference list
--JC: -> Updated objects reference list
judgement ObjectId |- ObjectIds -> ObjectIds;
GoodObjectReference_ReferenceDeletedFromTheList:
ObjId |- objectIds[ObjId.ObjIdL] -> ObjIdL ;
RecursiveRule_NotTheGoodObjectReference:
ObjId1 |- ObjIdL1 -> ObjIdL1_1
--------------------------------
ObjId1 |- objectIds[ObjId2.ObjIdL1] -> objectIds[ObjId2.ObjIdL1_1] ;
provided diff( ObjId1, ObjId2 );
end ENVremoveObjectReferenceFromReferenceList;
set ENVaddObjectReferenceToAGivenList is
--SC: Adds an object identifier in an object identifier list.
--
--JC: Object reference
--JC: |- Objects reference list
--JC: -> Updated objects reference list
judgement ObjectId |- ObjectIds -> ObjectIds;
EmptyReferenceList_ObjectReferenceAddedAtTheEndOfTheList:
ObjId |- objectIds[] -> objectIds[ObjId] ;
RecursiveRule_NotTheEndOfTheList:
ObjId1 |- ObjIdL1 -> ObjIdL1_1
--------------------------------
ObjId1 |- objectIds[ObjId2.ObjIdL1] -> objectIds[ObjId2.ObjIdL1_1] ;
end ENVaddObjectReferenceToAGivenList;
set ENVaddCreatedThreadToStatusList is
--SC: Adds a new created thread in the status list and communicates it
--SC: to the environment.
--
--JC: Thread reference
judgement (ObjectId);
--iJC: Thread reference
--iJC: |- Status list
--iJC: -> Updated status list
judgement ObjectId |- Statuss -> Statuss;
GetTheStatusList_AddThreadReferenceToThisList:
OThId |- StatL1 -> StatL1_1 &
addThreadToStackList( OThId )
--------------------------------
(OThId) ;
provided getStatusList( StatL1 );
do
ENVsendStatusList( StatL1_1 ) &
setNewStatusList( StatL1_1 );
AddThreadReferenceToTheCreatedThreadList:
ENVaddObjectReferenceToAGivenList( OThId |- created1 -> created1_1
)
--------------------------------
OThId |- statuss(created1, runnable, executing, blocked, dormant, suspended, dead, unlocked, locked) ->
statuss(created1_1, runnable, executing, blocked, dormant, suspended, dead, unlocked, locked) ;
end ENVaddCreatedThreadToStatusList;
set ENVaddCreatedSimpleObjectToStatusList is
--SC: Adds a new created object in the status list and communicates it
--SC: to the environment.
--
--JC: Created object reference
judgement (ObjectId);
--iJC: Created object reference
--iJC: |- Status list
--iJC: -> Updated status list
judgement ObjectId |- Statuss -> Statuss;
GetStatusList_AddObjectReferenceToThisList:
ObjId |- StatL1 -> StatL1_1 &
addObjectToStackList( ObjId )
--------------------------------
(ObjId) ;
provided getStatusList( StatL1 );
do
ENVsendStatusList( StatL1_1 ) &
setNewStatusList( StatL1_1 );
AddObjectReferenceToTheUnlockedObjectsReferenceList:
ENVaddObjectReferenceToAGivenList(
ObjId |- unlocked1 -> unlocked1_1 )
--------------------------------
ObjId |- statuss(created, runnable, executing, blocked, dormant, suspended, dead, unlocked1, locked) ->
statuss(created, runnable, executing, blocked, dormant, suspended, dead, unlocked1_1, locked) ;
end ENVaddCreatedSimpleObjectToStatusList;
set addThreadToStackList is
--SC: Adds a new thread in the stack list. Communicates to the environment.
--
--JC: Thread reference
judgement (ObjectId);
--iJC1: Thread reference
--iJC1: |- Objects and threads interaction list
--iJC1: -> Updated objects and threads interaction list.
judgement ObjectId |- Stacks -> Stacks;
--iJC2: Thread reference
--iJC2: |- Threads interaction list
--iJC2: => Updated threads interaction list.
judgement ObjectId |- ThreadStacks => ThreadStacks;
GetTheObjectsAndThreadsInteractionList_AddTheThreadReference:
OThId |- StackL1 -> StackL1_1
--------------------------------
(OThId) ;
provided getStackList( StackL1 );
do
ENVsendStackList( StackL1_1 ) &
setNewStackList( StackL1_1 );
AddTheCreatedThreadToTheThreadsAndObjectsInteractionLists:
OThId |- ThStackL1 => ThStackL1_1 &
addObjectToStackList( OThId |- ObjStackL1 => ObjStackL1_1 )
--------------------------------
OThId |- stacks(ThStackL1, ObjStackL1) -> stacks(ThStackL1_1, ObjStackL1_1) ;
EndOfTheThreadsInteractionList_AddTheThreadReference:
OThId |- threadStacks[] => threadStacks[threadStack(OThId, objectIds[])] ;
RecursiveRule_NotTheEndOfTheList:
OThId |- ThStackL1 => ThStackL1_1
--------------------------------
OThId |- threadStacks[ThStack.ThStackL1] => threadStacks[ThStack.ThStackL1_1] ;
end addThreadToStackList;
set addObjectToStackList is
--SC: Adds a new object in the stack list. Communicates to the environment.
--
--JC1: Object reference
judgement (ObjectId);
--JC2: Object reference
--JC2: |- Objects interaction list
--JC2: => Updated objects interaction list
judgement ObjectId |- ObjectStacks => ObjectStacks;
--iJC: Object reference
--iJC: |- Objects and threads interaction list
--iJC: -> Updated objects and threads interaction list
judgement ObjectId |- Stacks -> Stacks;
GetTheObjectsAndThreadsInteractionList_AddTheObjectReference:
ObjId |- StackL1 -> StackL1_1
--------------------------------
(ObjId) ;
provided getStackList( StackL1 );
do
ENVsendStackList( StackL1_1 ) &
setNewStackList( StackL1_1 );
AddTheCreatedObjectToTheObjectsInteractionList:
ObjId |- ObjStackL1 => ObjStackL1_1
--------------------------------
ObjId |- stacks(ThStackL, ObjStackL1) -> stacks(ThStackL, ObjStackL1_1) ;
EndOfTheObjectsInteractionList_AddTheObjectReference:
ObjId |- objectStacks[] => objectStacks[objectStack(ObjId, objectIds[])] ;
RecursiveRule_NotTheEndOfTheList:
ObjId |- ObjStackL1 => ObjStackL1_1
--------------------------------
ObjId |- objectStacks[ObjStack.ObjStackL1] => objectStacks[ObjStack.ObjStackL1_1] ;
end addObjectToStackList;
end java_environment