-- $Id: java_object_list.ty,v 1.12 10/.0/.2 .1:.1:.3 mrusso 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 */
-- /***************************************************************************/
program java_object_list is
use java;
use PSP;
use messargs;
import
ENVaddCreatedSimpleObjectToStatusList ( ObjectId ) ,
ENVaddCreatedThreadToStatusList ( ObjectId ) ,
ENVchangeObjectStatusInStatusList ( ObjectId ) ,
ENVinitializeStatusAndStackAndExceptionLists ( ) ,
ENVsendNewObject ( Object ) ,
ENVsendObjectAndClassVariableLists ( Objects, ClassVariablesL ) ,
ENVsendObjectList ( Objects ) ,
ENVupdateThreadStatusList ( ObjectId, ThreadStatus, ThreadStatus )
from java_environment;
import
getFieldDeclaration (
Objects, OptTypeName, Vals, Bool |- Identifier -> FieldDeclaration, Identifier, Bool ) ,
getInitialValueForAGivenType ( Type -> Val ) ,
isAThread ( Object -> Bool ) ,
isAThread ( OptTypeName => Bool ) ,
isThisModifierInTheList ( Modifier |- Modifiers -> Bool ) ,
makeAttributeList (
|- OptTypeName -> Pairs )
from java_inheritance;
import appendtree ( _, _, _ ) , diff ( _, _ ) , not_eq ( _, _ ) , succ ( _, _ )
from prolog() ;
var TVValue: Val;
var TVArrayInit: ArrayInitializer;
var TVLocVarDec: LocalVariableDeclaration;
var TVStatement: Statement;
var TVMethodDecl: MethodDeclarator;
set loadClasses is
--SC: Retrieves all the class names and their associated class variables
--SC: (name/value) contained in the program. Even if a class does
--SC: not contain any class variable, it is set in the class variable list.
--
--JC: Type declarations contained in the program
--JC: -> List containing all the classes and their variables
judgement (TypeDeclarations -> ClassVariablesL);
--iJC: Type declaration (interface or class)
--iJC: => Class variable list
judgement (TypeDeclaration => ClassVariablesL);
NoMoreTypeDeclaration_EndOfTheLoad:
(typeDeclarations[] -> classVariablesL[]) ;
RecursiveRuleOnTypeDeclaration:
(TDec => ClVarL1) & (TDecL -> ClVarL2) &
appendtree( ClVarL1, ClVarL2, ClVarL3 )
--------------------------------
(typeDeclarations[TDec.TDecL] -> ClVarL3) ;
InterfaceDeclaration_NotAClass:
(interfaceDeclaration(_, _, _, _) => classVariablesL[]) ;
ClassDeclaration_GetItsStaticVariables:
getStaticVariableList( FDeclL -> ClVarL )
--------------------------------
(classDeclaration(_, ClName, _, _, FDeclL) => classVariablesL[classVariables(ClName, ClVarL)]) ;
end loadClasses;
set getStaticVariables is
--SC: Get the static variables of the given class (this list can be empty)
--
--JC: Sought class
--JC: |- Class variable list
--JC: -> Class variables of the given class
judgement OptTypeName |- ClassVariablesL -> Pairs;
NoMoreClassVariableInTheList:
--RC: This case is normally impossible because each class should be
--RC: referenced in this list
_ |- classVariablesL[] -> pairs[] ;
RecursiveRuleOnClassVariableList:
ClName1 |- StaticVarsL -> StaticVarL
--------------------------------
ClName1 |- classVariablesL[classVariables(ClName2, _).StaticVarsL] -> StaticVarL ;
provided diff( ClName1, ClName2 );
HasFoundTheClassVariablesInTheList:
ClName |- classVariablesL[classVariables(ClName, StaticVarL)._] -> StaticVarL ;
end getStaticVariables;
set getStaticVariableList is
--SC: Retrieves all the static variables and their values (if a variable is
--SC: not initialized, a default value depending on the variable type is
--SC: assigned) contained in a class.
--
--JC: Fields contained in a class declaration
--JC: -> List of static variable names and their values
judgement (FieldDeclarations -> Pairs);
--iJC1: Field declaration
--iJC1: -> static variable list corresponding to the field declaration
judgement (FieldDeclaration => Pairs);
--iJC2: The common (part of) the type
--iJC2: |- variables declaration
--iJC2: => static variable list corresponding to the given variables declara
judgement Type |- VariableDeclarators => Pairs;
NoMoreFieldDeclarations: (fieldDeclarations[] -> pairs[]) ;
RecursiveRuleOnFieldDeclarations:
(FDec => ClVarL1) & (FDecL -> ClVarL2) &
appendtree( ClVarL1, ClVarL2, ClVarL3 )
--------------------------------
(fieldDeclarations[FDec.FDecL] -> ClVarL3) ;
MethodDeclaration_NotAStaticVariable:
(methodDeclaration(_, _, _, _, _) => pairs[]) ;
ConstructorDeclaration_NotAStaticVariable:
(constructorDeclaration(_, _, _, _) => pairs[]) ;
StaticVariables:
isThisModifierInTheList( static() |- ModL -> true() )
& Type |- StaticVarDecL => StaticPairL
--------------------------------
(fieldVariableDeclaration(ModL, Type, StaticVarDecL) => StaticPairL) ;
NotStaticVariables:
isThisModifierInTheList( static() |- ModL -> false() )
--------------------------------
(fieldVariableDeclaration(ModL, _, _) => pairs[]) ;
InitializedStaticVariable:
getRealTypeAndName( Type, StaticVarName -> _, RealName )
--------------------------------
Type |- variableDeclarators[initializedVariable(StaticVarName, TVValue)] => pairs[pair(RealName, TVValue)] ;
NotInitializedStaticVariable:
getRealTypeAndName( Type, StaticVarName -> RealType, RealName )
&
getInitialValueForAGivenType( RealType -> Value )
--------------------------------
Type |- variableDeclarators[StaticVarName] => pairs[pair(RealName, Value)] ;
InitializedStaticVariable_OtherStaticVariablesToRetrieve:
getRealTypeAndName( Type, StaticVarName -> _, RealName ) &
Type |- StaticVarDecL => ClVarL
--------------------------------
Type |- variableDeclarators[initializedVariable(StaticVarName, TVValue).StaticVarDecL] =>
pairs[pair(RealName, TVValue).ClVarL] ;
NotInitializedStaticVariable_OtherStaticVariablesToRetrieve:
getRealTypeAndName( Type, StaticVarName -> RealType, RealName )
&
getInitialValueForAGivenType( RealType -> Value )
& Type |- StaticVarDecL => ClVarL
--------------------------------
Type |- variableDeclarators[StaticVarName.StaticVarDecL] => pairs[pair(RealName, Value).ClVarL] ;
end getStaticVariableList;
set getMainThread is
--SC: Creates the thread that will execute the main() method (by default, its
--SC: class declaration is the first type declaration).
--SC: **********************************************************************
--SC: Be careful, the main() method must always be implemented in the first
--SC: class of the program
--SC: **********************************************************************
--
--JC: |- Program Type Declarations
--JC: -> New thread that will execute the main() method
judgement |- TypeDeclarations -> Object;
CreateTheMainThread:
--RC: The main thread has the number zero as reference.
createObject( objectId(true(), objectNumber 0) |- objectNumber 0, ClName -> Obj, _ )
--------------------------------
|- typeDeclarations[classDeclaration(_, ClName, _, _, _)._] -> Obj ;
do
ENVinitializeStatusAndStackAndExceptionLists(
);
end getMainThread;
set generateANumberForTheNewObject is
--SC: Determines the reference of the created object. This reference is the
--SC: number of objects in the list before this new object addition.
--
--JC: object list
--JC: -> object number
judgement |- Objects -> ObjectNumber;
--iJC: intermediate object number
--iJC: |- object list
--iJC: => object number
judgement integer |- Objects => integer;
CountsTheObjects:
0 |- ObjL => ObjectsNumber
--------------------------------
|- ObjL -> objectNumber ObjectsNumber ;
NoMoreObjectInTheList:
ObjectsNumber |- objects[] => ObjectsNumber ;
RecursiveRule_CountsTheObjects:
n |- ObjL => k & succ( k, m )
--------------------------------
n |- objects[_.ObjL] => m ;
end generateANumberForTheNewObject;
set createObject is
--SC: Create an object depending on its nature (i.e. a simple object or a
--SC: thread).
--
--JC: Reference of the thread that creates this new object (this reference is
--JC: useful in case of thread creation)
--JC: |- Generated reference for this new object, Object type
--JC: -> new created object, its identifier
judgement ObjectId |- ObjectNumber, OptTypeName -> Object, ObjectId;
SimpleObjectCreation:
isAThread( ClName => false() ) &
createSimpleObject( objectId(false(), ObjNb), ClName -> Obj )
--------------------------------
_ |- ObjNb, ClName -> Obj, objectId(false(), ObjNb) ;
provided diff( ObjNb, objectNumber 0 );
do
ENVsendNewObject( Obj ) &
ENVaddCreatedSimpleObjectToStatusList(
objectId(false(), ObjNb) );
ThreadCreation:
isAThread( ClName => true() ) &
createThreadObject( objectId(true(), ObjNb), ClName, OThId -> Obj )
--------------------------------
OThId |- ObjNb, ClName -> Obj, objectId(true(), ObjNb) ;
provided diff( ObjNb, objectNumber 0 );
do
ENVsendNewObject( Obj ) &
ENVaddCreatedThreadToStatusList( objectId(true(), ObjNb) );
MainThreadCreation:
--RC: This thread has 0 as number and owns the main() method
createThreadObject( objectId(true(), objectNumber 0), ClName -> Obj )
--------------------------------
_ |- objectNumber 0, ClName -> Obj, objectId(true(), objectNumber 0) ;
do ENVsendNewObject( Obj );
end createObject;
set createSimpleObject is
--SC: Creates a simple object (i.e. not a thread) with its attributes.
--
--JC: Object identifier, its type
--JC: -> created object
judgement (ObjectId, OptTypeName -> Object);
SimpleObjectCreation_GetAttributeList:
makeAttributeList( |- ClName -> AttrL )
--------------------------------
(ObjId, ClName -> object(ObjId, ClName, AttrL, unlocked(), waits[], empty())) ;
end createSimpleObject;
set createThreadObject is
--SC: Creates a thread with its attributes and its closure (if it is the main
--SC: thread, this closure is the main() method code, otherwise it is the
--SC: run() method code). The new thread status is runnable for the main
--SC: thread, otherwise it is created by the given thread.
--
--JC1: Identifier for this thread, Its type, Identifier of the thread that
--JC1: creates this new thread
--JC1: -> New thread
judgement (ObjectId, Type, ObjectId -> Object);
--JC2: This judgement must only be used for the main thread (that is the
--JC2: thread that will execute the main() method) creation.
--JC2: Identifier for this thread, Its type
--JC2: -> The new main thread
judgement (ObjectId, Type -> Object);
ThreadCreation:
makeAttributeList( |- ClName1 -> AttrL
) &
getFieldDeclaration(
objects[], ClName1, vals[], false() |- identifier "run" -> FieldDecl, ClName2, true() )
&
makeClosure( ClName2, vals[], OThId1 |- FieldDecl -> Clr )
--------------------------------
(OThId1, ClName1, OThId2 -> object(OThId1, ClName1, AttrL, unlocked(), waits[], activity(created(OThId2), Clr))) ;
provided diff( OThId1, objectId(true(), objectNumber 0) );
MainThreadCreation:
makeAttributeList( |- ClName1 -> AttrL
) &
getFieldDeclaration(
objects[], ClName1, vals[], false() |- identifier "main" -> FieldDecl, ClName2, true() )
&
makeClosure(
ClName2, vals[], objectId(true(), objectNumber 0) |-
FieldDecl -> clr(_, _, MethName, Env, InstL) )
--------------------------------
(objectId(true(), objectNumber 0), ClName1
->
object(
objectId(true(), objectNumber 0), ClName1, AttrL, unlocked(), waits[],
activity(runnable(), clr(objectId(true(), objectNumber 0), identifier "none", MethName, Env, InstL)))) ;
end createThreadObject;
set createExceptionObject is
--SC: Creates an instance of an exception and adds it to the object list.
--
--JC: Object list (this list contains all the objects created by the program
--JC: interpretation), current executing thread id
--JC: |- exception class name, exception text
--JC: -> new exception object id, modified object list (the new
--JC: exception object has been appended), next instructions to execute
--JC: (constructor call of the exception + except statment)
judgement
Objects, ObjectId |- Identifier, ExceptText -> ObjectId, Objects, Insts;
--JC: ^, ^ |- ^, ^, id of the object that has thrown this exception,
--JC: name of the method where the exception occured -> ^, ^, ^
--JC: (ie constructor call of the exception + exception statement)
judgement
Objects, ObjectId |- Identifier, ExceptText, ObjectId, Identifier -> ObjectId, Objects, Insts;
--JC: ^ (only useful to generate the exception object id), ^
--JC: |- ^, ^ => ^, exception object, ^ (ie constructor call of the exception
--JC: + except statement)
judgement
Objects, ObjectId |- Identifier, ExceptText => ObjectId, Object, Insts;
--JC: ^, ^ |- ^, ^, ^, ^ => ^, ^, ^
--JC: (ie constructor call of the exception + exception statement)
judgement
Objects, ObjectId |- Identifier, ExceptText, ObjectId, Identifier => ObjectId, Object, Insts;
CreateAnExceptionObject_AddItToObjectList:
ObjL1, OThId |- ExceptName, Text => ExObjId, ExObj, Insts &
appendtree( ObjL1, objects[ExObj], ObjL1_1 )
--------------------------------
ObjL1, OThId |- ExceptName, Text -> ExObjId, ObjL1_1, Insts ;
CreateExceptionObject_ReturnItAndExcept:
generateANumberForTheNewObject( |- ObjL1 -> i )
& createObject( OThId |- i, ExceptName -> ExObj, ExObjId )
--------------------------------
ObjL1, OThId |-
ExceptName, Text
=>
ExObjId, ExObj, insts[constructorCall1(ExceptName, arguments[], ExObjId), except(ExceptName, ExObjId, Text)] ;
CreateAnExceptionObject_AddItToObjectList:
ObjL1, OThId |- ExceptName, Text, ObjId, MethodName => ExObjId, ExObj, Insts
& appendtree( ObjL1, objects[ExObj], ObjL1_1 )
--------------------------------
ObjL1, OThId |- ExceptName, Text, ObjId, MethodName -> ExObjId, ObjL1_1, Insts ;
CreateExceptionObject_ReturnItAndExcept:
generateANumberForTheNewObject( |- ObjL1 -> i )
& createObject( OThId |- i, ExceptName -> ExObj, ExObjId )
--------------------------------
ObjL1, OThId |-
ExceptName, Text, ObjId, MethodName
=>
ExObjId, ExObj,
insts[constructorCall1(ExceptName, arguments[], ExObjId), exception(OThId, ObjId, MethodName, except(ExceptName, ExObjId, Text))] ;
end createExceptionObject;
set getObjectLockInformation is
--SC: Returns how many times the given object is locked and by which thread.
--
--JC: The object reference for which the lock information is required
--JC: |- objects
--JC: -> The reference of the thread that has locked the object,
--JC: lock(s) number
judgement ObjectId |- Objects -> ObjectId, integer;
LockedObject:
getObject( ObjId |- ObjL -> object(ObjId, _, _, locked(OThId, integer nbLocks), _, _) )
--------------------------------
ObjId |- ObjL -> OThId, nbLocks ;
UnlockedObject:
getObject( ObjId |- ObjL -> object(ObjId, _, _, unlocked(), _, _) )
--------------------------------
ObjId |- ObjL -> _, 0 ;
end getObjectLockInformation;
set getThreadCurrentMethod is
--SC: Returns the given thread current method name (gets the continuation
--SC: and passes through all the closures to find the most inner one (only
--SC: the first instruction is checked)).
--
--JC1: Thread reference
--JC1: |- Objects
--JC1: -> Current method name
judgement ObjectId |- Objects -> Identifier;
--JC2: Thread reference
--JC2: |- Objects
--JC2: => first instruction
judgement ObjectId |- Objects => Inst;
--iJC1: |- Closure
--iJC1: -> Current method name, current instruction
judgement |- Clr -> Identifier, Inst;
--iJC2: |- Instruction
--iJC2: => Current method name or undefined, current instruction, True if the instruction contains
--iJC2: a closure/ False otherwise
judgement |- Inst => Identifier, Inst, Bool;
GetTheThreadContinuation:
|- Cont -> MethName, Inst
--------------------------------
OThId |- objects[object(OThId, _, _, _, _, activity(_, Cont))._] -> MethName ;
SeekTheGivenThread:
OThId |- ObjL -> MethName
--------------------------------
OThId |- objects[object(ObjId, _, _, _, _, _).ObjL] -> MethName ;
provided diff( ObjId, OThId );
GetTheThreadContinuation:
|- Cont -> _, Inst
--------------------------------
OThId |- objects[object(OThId, _, _, _, _, activity(_, Cont))._] => Inst ;
SeekTheGivenThread:
OThId |- ObjL -> Inst
--------------------------------
OThId |- objects[object(ObjId, _, _, _, _, _).ObjL] => Inst ;
provided diff( ObjId, OThId );
BlockIntoAClosure_FindTheMethodNameInTheBlockInstL:
|- semBlock(insts[Inst1.InstL], Env) => MethName, Inst2, true()
--------------------------------
|- clr(_, _, _, _, insts[semBlock(insts[Inst1.InstL], Env)._]) -> MethName, Inst2 ;
BlockIntoAClosure_NoMoreMethod_SoTheCurrentMethodIsThisOne:
--RC: No more closure => no more method. So the current method is the one
--RC: we are looking for.
|- semBlock(insts[Inst.InstL], Env) => _, _, false()
--------------------------------
|- clr(_, _, MethName, _, insts[semBlock(insts[Inst.InstL], Env)._]) -> MethName, Inst ;
ClosureIntoAClosure_FindTheMethodNameInTheClosure:
|- clr(ObjId, Mode, MethName1, Env, InstL) -> MethName2, Inst
--------------------------------
|- clr(_, _, _, _, insts[clr(ObjId, Mode, MethName1, Env, InstL)._]) -> MethName2, Inst ;
NoMoreInstructionInTheCurrentClosure_TheCurrentMethodIsThisOne:
|- clr(_, _, MethName, _, insts[]) -> MethName, _ ;
NoMoreClosureInTheCurrentClosure_TheCurrentMethodIsThisOne:
|- clr(_, _, MethName, _, insts[Inst._]) -> MethName, Inst ;
provided not_eq( Inst, clr(_, _, _, _, _) ) & not_eq( Inst, semBlock(_, _) );
NoMoreInstructionInTheCurrentBlock_NoMoreMethod:
|- semBlock(insts[], _) => _, _, false() ;
BlockIntoTheCurrentBlock_LookForTheMethodName:
|- semBlock(InstL, Env) => MethName, Inst, TF
--------------------------------
|- semBlock(insts[semBlock(InstL, Env)._], _) => MethName, Inst, TF ;
ClosureIntoTheBlock_FindTheMethodNameInTheClosure:
|- clr(ObjId, Mode, MethName1, Env, InstL) -> MethName2, Inst
--------------------------------
|- semBlock(insts[clr(ObjId, Mode, MethName1, Env, InstL)._], _) => MethName2, Inst, true() ;
NoMoreClosureInTheCurrentBlock_NoMoreMethod:
|- semBlock(insts[Inst._], _) => _, Inst, false() ;
provided not_eq( Inst, clr(_, _, _, _, _) ) & not_eq( Inst, semBlock(_, _) );
end getThreadCurrentMethod;
set getObjectType is
--SC: Returns the given object type.
--
--JC: Object reference
--JC: |- Objects
--JC: -> Type of the given object
judgement ObjectId |- Objects -> Type;
GetObjectType:
getObject( ObjId |- ObjL -> object(ObjId, Type, _, _, _, _) )
--------------------------------
ObjId |- ObjL -> Type ;
end getObjectType;
set isTheObjectLocked is
--SC: Checks if the given object is locked or not.
--
--JC: Object reference
--JC: |- Objects
--JC: -> True/False
judgement ObjectId |- Objects -> Bool;
--iJC: Locks number
--iJC: -> True/False
judgement (integer -> Bool);
getObjectLockInfo:
getObjectLockInformation( ObjId |- ObjL -> _, NbLocks )
& (NbLocks -> TF)
--------------------------------
ObjId |- ObjL -> TF ;
NoLock: (0 -> false()) ;
Lock:
(NbLocks -> true()) ;
provided diff( NbLocks, 0 );
end isTheObjectLocked;
set areAllThreadsDead is
--SC: Checks that all threads are "dead".
--
--JC: Objects
--JC: -> True if all the threads are dead/False otherwise
judgement (Objects -> Bool);
NoAliveThread: (objects[] -> true()) ;
AtLeastOneAliveThread:
isAThread( Obj -> true() ) &
isTheThreadDead( Obj -> false() )
--------------------------------
(objects[Obj._] -> false()) ;
NotAThread_RecursiveRule:
isAThread( Obj -> false() ) &
(ObjL -> TF)
--------------------------------
(objects[Obj.ObjL] -> TF) ;
NotAnAliveThread_RecursiveRule:
isAThread( Obj -> true() ) &
isTheThreadDead( Obj -> true() ) &
(ObjL -> TF)
--------------------------------
(objects[Obj.ObjL] -> TF) ;
end areAllThreadsDead;
set isTheThreadDead is
--SC: Determines if the given thread is "dead" or not.
--
--JC: Thread
--JC: -> True if dead/ False if alive
judgement (Object -> Bool);
AliveThread:
(object(_, _, _, _, _, activity(ThStatus, _)) -> false()) ;
provided diff( ThStatus, dead() );
DeadThread:
(object(_, _, _, _, _, activity(dead(), _)) -> true()) ;
end isTheThreadDead;
set releaseObjectLock is
--SC : Removes a lock on an object.
--
--JC: Locked object reference
--JC: |- Objects
--JC: -> Updated object list
judgement ObjectId |- Objects -> Objects;
FindTheObject_RemoveTheLock:
ObjId |- objects[object(ObjId, ClName, AttrL, locked(_, integer 1), Wait_L, Activity).ObjL] ->
objects[object(ObjId, ClName, AttrL, unlocked(), Wait_L, Activity).ObjL] ;
LookForTheObject:
ObjId1 |- ObjL1 -> ObjL1_1
--------------------------------
ObjId1 |- objects[object(ObjId2, ClName2, AttrL2, Locked2, Wait_L2, Activity2).ObjL1] ->
objects[object(ObjId2, ClName2, AttrL2, Locked2, Wait_L2, Activity2).ObjL1_1] ;
provided diff( ObjId1, ObjId2 );
end releaseObjectLock;
set getNumberOfDormantAndBlockedThreadsOnTheGivenObject is
--SC: Computes the number of threads "blocked" and "dormant", waiting for a
--SC: lock on the given object.
--
--JC: Object reference
--JC: |- Objects
--JC: -> number of threads dormant and blocked on the given object
judgement ObjectId |- Objects -> integer, integer;
--iJC: intermediate number of threads dormant or blocked on the given object
--iJC: |- Objects, Sought object reference
--iJC: -> Number of dormant and blocked threads on the given object
judgement integer, integer |- Objects, ObjectId -> integer, integer;
EntryPoint:
0, 0 |- ObjL, OjbId -> nbDormantThread, nbBlockedThread
--------------------------------
OjbId |- ObjL -> nbDormantThread, nbBlockedThread ;
NoMoreObject:
nbDormantThread, nbBlockedThread |- objects[], _ -> nbDormantThread, nbBlockedThread ;
BlockedThreadOnTheGivenObject_RecursiveRule:
succ( nbBlockedThread1, nbBlockedThread1_1 ) &
nbDormantThread1, nbBlockedThread1_1 |- ObjL, OjbId -> nbDormantThread1_1, nbBlockedThread1_2
--------------------------------
nbDormantThread1, nbBlockedThread1 |-
objects[object(_, _, _, _, _, activity(blocked(OjbId), _)).ObjL], OjbId -> nbDormantThread1_1, nbBlockedThread1_2 ;
DormantThreadOnTheGivenObject_RecursiveRule:
succ( nbDormantThread1, nbDormantThread1_1 ) &
nbDormantThread1_1, nbBlockedThread1 |- ObjL, OjbId -> nbDormantThread1_2, nbBlockedThread1_1
--------------------------------
nbDormantThread1, nbBlockedThread1 |-
objects[object(_, _, _, _, _, activity(dormant(OjbId, _), _)).ObjL], OjbId
->
nbDormantThread1_2, nbBlockedThread1_1 ;
NotADormantOrBlockedThread_RecursiveRule:
nbDormantThread1, nbBlockedThread1 |- ObjL, OjbId -> nbDormantThread1_1, nbBlockedThread1_1
--------------------------------
nbDormantThread1, nbBlockedThread1 |-
objects[object(_, _, _, _, _, activity(ThStatus, _)).ObjL], OjbId -> nbDormantThread1_1, nbBlockedThread1_1 ;
provided
not_eq( ThStatus, blocked(OjbId) ) & not_eq( ThStatus, dormant(OjbId, _) );
SimpleObject_CanNotBeBlockedOrDormant:
nbDormantThread1, nbBlockedThread1 |- ObjL, OjbId -> nbDormantThread1_1, nbBlockedThread1_1
--------------------------------
nbDormantThread1, nbBlockedThread1 |-
objects[object(_, _, _, _, _, empty()).ObjL], OjbId -> nbDormantThread1_1, nbBlockedThread1_1 ;
end getNumberOfDormantAndBlockedThreadsOnTheGivenObject;
set setLock is
--SC: Sets a lock on the given object. (this set should be used only if the
--SC: object does not have any lock or if it is already locked by the given
--SC: thread (in this case the lock value is higher than 1))
--
--JC: Object reference on which the lock must be set,
--JC: Thread reference (i.e. the owner of the lock),
--JC: the number of times that the thread locked this object
--JC: |- Objects
--JC: -> modified object list
judgement ObjectId, ObjectId, Val |- Objects -> Objects;
--iJC: (same judgements. The first one is used for the env)
judgement ObjectId, ObjectId, Val |- Objects => Objects;
EntryPoint_SendInfoToEnv:
ObjId, OThId, LocValue |- ObjL1 => ObjL1_1
--------------------------------
ObjId, OThId, LocValue |- ObjL1 -> ObjL1_1 ;
do ENVsendObjectList( ObjL1_1 );
setLock:
ObjId, OThId, LocValue |-
objects[object(ObjId, ClName, AttrL, unlocked(), WaitSet, Act).ObjL] =>
objects[object(ObjId, ClName, AttrL, locked(OThId, LocValue), WaitSet, Act).ObjL] ;
do
ENVchangeObjectStatusInStatusList( ObjId );
setNewLockValue_WhenItIsAlreadyLockedByThisSameObject:
ObjId, OThId, LocValue |-
objects[object(ObjId, ClName, AttrL, locked(OThId, _), WaitSet, Act).ObjL] =>
objects[object(ObjId, ClName, AttrL, locked(OThId, LocValue), WaitSet, Act).ObjL] ;
LookForTheObject:
ObjId1, OThId, LocValue |- ObjL1 => ObjL1_1
--------------------------------
ObjId1, OThId, LocValue |-
objects[object(ObjId2, ClName, AttrL, Lock, WaitSet, Act).ObjL1] =>
objects[object(ObjId2, ClName, AttrL, Lock, WaitSet, Act).ObjL1_1] ;
provided diff( ObjId1, ObjId2 );
end setLock;
set setNewClosure is
--SC: sets the new closure in the activity of the given thread.
--
--JC: Thread reference that will have this new closure, the new closure,
--JC: class variables (only used for the environment)
--JC: |- objects
--JC: -> modified object list
judgement ObjectId, Clr, ClassVariablesL |- Objects -> Objects;
--JC: (same as the previous one without the class variables)
judgement ObjectId, Clr |- Objects -> Objects;
EntryPoint_SendInfoToEnv:
OThId, Clr |- ObjL1 -> ObjL1_1
--------------------------------
OThId, Clr, ClVarL |- ObjL1 -> ObjL1_1 ;
do
ENVsendObjectAndClassVariableLists( ObjL1_1, ClVarL );
SetTheNewClosureToTheGivenThread:
OThId, Clr |-
objects[object(OThId, ClName, AttrL, Lock, WaitSet, activity(ThStatus, _)).ObjL] ->
objects[object(OThId, ClName, AttrL, Lock, WaitSet, activity(ThStatus, Clr)).ObjL] ;
LookForTheGivenThread:
OThId, Clr1 |- ObjL1 -> ObjL1_1
--------------------------------
OThId, Clr1 |-
objects[object(ObjId, ClName, AttrL, Lock, WaitSet, Act).ObjL1] ->
objects[object(ObjId, ClName, AttrL, Lock, WaitSet, Act).ObjL1_1] ;
provided diff( OThId, ObjId );
end setNewClosure;
set setNewThreadStatus is
--SC: sets the new status to the given thread.
--
--JC: Thread reference that will have the new status, the new status,
--JC: class variables (only used for the environment)
--JC: |- objects
--JC: -> modified object list
judgement
ObjectId, ThreadStatus, ClassVariablesL |- Objects -> Objects;
--iJC: (same as above without the class variables)
judgement ObjectId, ThreadStatus, Objects |- Objects => Objects;
EntryPoint_SendInfoToEnv:
OThId, ThStatus, ObjL1 |- ObjL1 => ObjL1_1
--------------------------------
OThId, ThStatus, ClVarL |- ObjL1 -> ObjL1_1 ;
do
ENVsendObjectList( ObjL1_1 ) &
ENVsendObjectAndClassVariableLists( ObjL1_1, ClVarL );
SetNewStatusToTheGivenThread:
OThId, NewThStatus, _ |-
objects[object(OThId, ClName, AttrL, Lock, WaitSet, activity(OldThStatus, Clr)).ObjL] =>
objects[object(OThId, ClName, AttrL, Lock, WaitSet, activity(NewThStatus, Clr)).ObjL] ;
do
ENVupdateThreadStatusList( OThId, OldThStatus, NewThStatus );
LookForTheGivenThread:
OThId, ThStatus, ObjL |- ObjL1 => ObjL1_1
--------------------------------
OThId, ThStatus, ObjL |-
objects[object(ObjId, ClName, AttrL, Lock, WaitSet, Act).ObjL1] =>
objects[object(ObjId, ClName, AttrL, Lock, WaitSet, Act).ObjL1_1] ;
provided diff( OThId, ObjId );
end setNewThreadStatus;
set getObject is
--SC: gets the object specified by its reference
--
--JC: Sought object reference
--JC: |- Objects
--JC: -> the wanted object
judgement ObjectId |- Objects -> Object;
HasFoundTheObject:
ObjId |- objects[object(ObjId, ClName, AttrL, Lock, WaitSet, Act)._] ->
object(ObjId, ClName, AttrL, Lock, WaitSet, Act) ;
LookForTheObject:
ObjId1 |- ObjL -> Obj
--------------------------------
ObjId1 |- objects[object(ObjId2, _, _, _, _, _).ObjL] -> Obj ;
provided diff( ObjId1, ObjId2 );
end getObject;
set makeClosure is
--SC: Makes the closure corresponding to the method call. A synchronized
--SC: instruction is added if the method has the "synchronized" modifier in
--SC: its declaration. A Closure is composed of the reference of the object
--SC: on which the method is executed, the method name, if it is a static or
--SC: non static method, the parameters name and value list, the environment
--SC: (i.e. the parameters and the local variables of the method body) and
--SC: the method instructions
--
--JC: Class name of the object that has called this method, Parameter values,
--JC: Reference of the object that has invoked this method
--JC: |- Method declaration
--JC: -> Closure for this method
judgement OptTypeName, Vals, ObjectId |- FieldDeclaration -> Clr;
SynchronizedMethod:
--RC: Gets the closure for this synchronized method (the instruction list
--RC: contains a synchro_ref instruction as first instruction followed by
--RC: the instructions of the method body)
isThisModifierInTheList(
synchronized() |- ModL -> true() ) &
getMethodNameAndParameters( TVMethodDecl -> MethName, ParamL )
&
makeBindedParamList( ParamValueL |- ParamL -> BindParamL )
&
getModeAndTargetClass( ClName |- ModL -> _, TargetClName )
&
getInstructionsAndLocalVariables(
insts[], locs[pairs[]] |- MBlock => InstL, LocVarL )
--------------------------------
ClName, ParamValueL, ObjId |-
methodDeclaration(ModL, _, TVMethodDecl, _, MBlock) ->
clr(
ObjId, TargetClName, MethName, env(BindParamL, LocVarL),
insts[synchroLock(ObjId, semBlock(InstL, blockEnv(BindParamL, LocVarL, pairs[])))]) ;
NonSynchronizedMethod:
--RC: Gets the closure for this non synchronized method
isThisModifierInTheList(
synchronized() |- ModL -> false() ) &
getMethodNameAndParameters( TVMethodDecl -> MethName, ParamL )
&
makeBindedParamList( ParamValueL |- ParamL -> BindParamL )
&
getModeAndTargetClass( ClName |- ModL -> _, TargetClName )
&
getInstructionsAndLocalVariables(
insts[], locs[pairs[]] |- MBlock => InstL, LocVarL )
--------------------------------
ClName, ParamValueL, ObjId |-
methodDeclaration(ModL, _, TVMethodDecl, _, MBlock) ->
clr(ObjId, TargetClName, MethName, env(BindParamL, LocVarL), InstL) ;
end makeClosure;
set getInstructionsAndLocalVariables is
--SC: Gets all the instructions and local variables contained in the given
--SC: block.
--
--JC1: Instructions, Local variables
--JC1: |- Block to analyse
--JC1: => Increased instruction list, Increased local
--JC1: variable list
judgement Insts, Locs |- Block => Insts, Locs;
--JC2: Instructions, Local variables
--JC2: |- Block Statement (i.e. a statement or a local variable declaration)
--JC2: => Increased instruction list, Increased local variable list
judgement Insts, Locs |- BlockStatement -> Insts, Locs;
NoMoreElementInTheBlock:
InstL, LocVarL |- block[] => InstL, LocVarL ;
BlockWithABlockAsFirstInstruction:
--RC: Treats the next elements of the block
--RC: (the first block is not analyse)
InstL1, LocVarL1 |- BlElemL2 => InstL1_1, LocVarL1_1 &
appendtree( insts[block[BlElem1.BlElemL1]], InstL1_1, InstL1_2 )
--------------------------------
InstL1, LocVarL1 |- block[block[BlElem1.BlElemL1].BlElemL2] => InstL1_2, LocVarL1_1 ;
BlockWithoutABlockAsFirstInstruction:
--RC: Treats the first statement and goes on
--RC: with the next elements of the block
InstL1, LocVarL1 |- BlElem -> InstL1_1, LocVarL1_1 &
InstL1_1, LocVarL1_1 |- BlElemL => InstL1_2, LocVarL1_2
--------------------------------
InstL1, LocVarL1 |- block[BlElem.BlElemL] => InstL1_2, LocVarL1_2 ;
provided not_eq( BlElem, block[_] );
LocalVariableDeclaration_AddLocalVariableAndInstruction:
addToLocalVariableList( LocVarL1 |- TVLocVarDec -> LocVarL1_1, InstL2 )
& appendtree( InstL1, InstL2, InstL3 )
--------------------------------
InstL1, locs[LocVarL1.LocVarLL] |- TVLocVarDec -> InstL3, locs[LocVarL1_1.LocVarLL] ;
Statement_AddItToTheInstructionList:
appendtree( InstL1, insts[TVStatement], InstL1_1 )
--------------------------------
InstL1, LocVarL |- TVStatement -> InstL1_1, LocVarL ;
end getInstructionsAndLocalVariables;
set getModeAndTargetClass is
--SC: Gets the mode ("static", "nonvirtual" or "virtual") and the target
--SC: (the given class name if it is a static method or "none" otherwise)
--
--JC: Class Name
--JC: |- Method modifiers
--JC: -> Mode ("static", "nonvirtual" or "virtual"), the target
judgement OptTypeName |- Modifiers -> Identifier, Identifier;
Static:
isThisModifierInTheList( static() |- ModL -> true() )
--------------------------------
ClName |- ModL -> identifier "static", ClName ;
Private:
isThisModifierInTheList( private() |- ModL -> true() )
--------------------------------
_ |- ModL -> identifier "nonvirtual", identifier "none" ;
Other: _ |- _ -> identifier "virtual", identifier "none" ;
end getModeAndTargetClass;
set makeBindedParamList is
--SC: Build a list that contains all the parameter names and their associated
--SC: values.
--
--JC: Parameter values
--JC: |- Parameter declaration
--JC: -> parameter (name/value) list
judgement Vals |- Parameters -> Pairs;
NoMoreValue: vals[] |- _ -> pairs[] ;
RecursiveRule:
getRealTypeAndName( Type, VarDeclId -> _, RealName ) &
ValueL |- ParamDecL -> ParamL
--------------------------------
vals[Value.ValueL] |- parameters[parameter(_, Type, VarDeclId).ParamDecL] -> pairs[pair(RealName, Value).ParamL] ;
end makeBindedParamList;
set addToLocalVariableList is
--SC: Adds a/many new local variables to the local variable list. A local
--SC: variable has no value (i.e. "empty()") if it is not initialized or it
--SC: has been initialized with an expression that needs to be evaluated
--SC: before the assignment (in this case, an instruction needs to be added
--SC: at the top of the instruction list).
--
--JC: Existing local variables
--JC: |- a local variable declaration
--JC: -> Increased local variable list, Instruction that needs to be executed
--JC: to evaluate an expression
judgement Pairs |- LocalVariableDeclaration -> Pairs, Insts;
--iJC: type, initial Value |- variable declarator
--iJC: => local variable list, Instruction that needs to be executed to
--iJC: evaluate an expression
judgement Type, Val |- VariableDeclarators => Pairs, Insts;
EntryPoint_LocalVariablesDeclaration_PrimitiveType:
Type, empty() |- LocVarNameL => LocVarL2, InstL &
appendtree( LocVarL1, LocVarL2, LocVarL3 )
--------------------------------
LocVarL1 |- localVariableDeclaration(_, Type, LocVarNameL) -> LocVarL3, InstL ;
InitializedVariableWithAValue_AddToLocalVariableList:
getRealTypeAndName( Type, VarDeclId -> _, Name )
--------------------------------
Type, _ |-
variableDeclarators[initializedVariable(VarDeclId, TVValue)] => pairs[pair(Name, TVValue)], insts[] ;
InitializedVariableWithAnArrayInitializer_AddToInstrAndLocalVariableLists:
--RC: Local variables do not have default values
getRealTypeAndName( Type, VarDeclId -> RealType, Name ) &
getElementTypeAndNDims( RealType -> ElementType, NDims )
--------------------------------
Type, Value |-
variableDeclarators[initializedVariable(VarDeclId, TVArrayInit)] =>
pairs[pair(Name, Value)], insts[binaryAssign(Name, assignment(), newArray(ElementType, dims[], NDims, TVArrayInit))] ;
InitializedVariableWithAnExpression_AddToInstrAndLocalVariableLists:
--RC: Local variables do not have default values
getRealTypeAndName( Type, VarDeclId -> _, Name )
--------------------------------
Type, Value |-
variableDeclarators[initializedVariable(VarDeclId, Expr)] =>
pairs[pair(Name, Value)], insts[binaryAssign(Name, assignment(), Expr)] ;
NonInitializedVariable:
getRealTypeAndName( Type, VarDeclId -> _, Name )
--------------------------------
Type, Value |- variableDeclarators[VarDeclId] => pairs[pair(Name, Value)], insts[] ;
provided not_eq( initializedVariable(_, _), Name );
RecursiveRule:
Type, Value |- variableDeclarators[VarDecl] => LocVarL1, InstL1 &
Type, Value |- VarDeclL => LocVarL2, InstL2 &
appendtree( LocVarL1, LocVarL2, LocVarL3 ) & appendtree( InstL1, InstL2, InstL3 )
--------------------------------
Type, Value |- variableDeclarators[VarDecl.VarDeclL] => LocVarL3, InstL3 ;
set getElementTypeAndNDims is
judgement (Type -> Type, Dims);
GetElementTypeAndNdims_BaseCase:
(Type -> Type, dims[]) ;
provided not_eq( Type, arrayof(_) );
GetElementTypeAndNDims_Recurse:
(Type -> ElementType, NDims)
--------------------------------
(arrayof(Type) -> ElementType, dims[dim().NDims]) ;
end getElementTypeAndNDims ;
end addToLocalVariableList;
set getRealTypeAndName is
--SC: Computes the real type and name of a parameter, variable, etc.
--SC: given a type and a variable declarator id.
judgement (Type, VariableDeclaratorId -> Type, Identifier);
GetRealTypeAndName_BaseCase:
(Type, identifier i -> Type, identifier i) ;
GetRealTypeAndName_Recurse:
(arrayof(Type), VarDeclId -> RealType, Name)
--------------------------------
(Type, array(VarDeclId) -> RealType, Name) ;
end getRealTypeAndName;
set getRealName is
--SC: Computes the real name of a parameter, variable, etc.
--SC: given a variable declarator id.
judgement (VariableDeclaratorId -> Identifier);
GetRealName_BaseCase: (identifier i -> identifier i) ;
GetRealName_Recurse:
(VarDeclId -> Name)
--------------------------------
(array(VarDeclId) -> Name) ;
end getRealName;
set getMethodNameAndParameters is
--SC: Extracts the name of a method and the parameter list.
--SC: The real return type could also be computed here, in the same
--SC: fashion as for getRealTypeAndName, but currently the return type
--SC: does not seem to be used.
judgement (MethodDeclarator -> Identifier, Parameters);
getMethodNameAndParameters_BaseCase:
(methodDeclarator(Name, Params) -> Name, Params) ;
getMethodNameAndParameters_Recurse:
(mtdDecl -> Name, Params)
--------------------------------
(arrayMethodDeclarator(mtdDecl) -> Name, Params) ;
end getMethodNameAndParameters;
end java_object_list