-- $Id: java_expr_evaluation.ty,v 1.14 10/.0/.2 .1:.1:.4 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_expr_evaluation is
use java;
use PSP;
import sub ( _, _, _ ) , sup ( _, _ )
from arith;
import
APIMethodOrConstructorCall (
Objects, ClassVariablesL, Ref, Ref |-
Identifier, java -> Objects, ClassVariablesL, Insts, ThreadStatus )
from java_api;
import
evaluateBinaryOperation (
|- Val, Val, BinaryOperator -> Val ) ,
evaluateUnaryOperation (
|- Val, BinaryOperator -> Val ) ,
getAttributeOrStaticVariableValue (
Objects, ClassVariablesL, ObjectId |- Identifier -> Val ) ,
getParameterOrLocalOrStaticVariableValue (
Env, ClassVariablesL, Identifier |- Identifier -> Val ) ,
getStaticVariableValue (
ClassVariablesL, Identifier |- Identifier -> Val ) ,
getVariableValue (
Objects, ClassVariablesL, Env, ObjectId |- Identifier -> Val )
from java_evaluate;
import
getClassDeclaration (
|- OptTypeName -> TypeDeclaration ) ,
getDirectAncestor (
|- OptTypeName -> OptTypeName ) ,
isAClass ( Identifier -> Bool ) ,
getFieldDeclaration (
Objects, OptTypeName, Vals, Bool |- Identifier -> FieldDeclaration, Identifier, Bool )
from java_inheritance;
import
createExceptionObject (
Objects, ObjectId |- Identifier, ExceptText -> ObjectId, Objects, Insts ) ,
createObject (
ObjectId |- ObjectNumber, OptTypeName -> Object, ObjectId ) ,
generateANumberForTheNewObject (
|- Objects -> ObjectNumber ) ,
getObjectType ( ObjectId |- Objects -> Type ) ,
getThreadCurrentMethod ( ObjectId |- Objects -> Identifier )
, makeBindedParamList ( Vals |- Parameters -> Pairs ) ,
makeClosure (
OptTypeName, Vals, ObjectId |- FieldDeclaration -> Clr ) ,
getInstructionsAndLocalVariables (
Insts, Locs |- Block => Insts, Locs )
from java_object_list;
import appendtree ( _, _, _ ) , diff ( _, _ ) , not_eq ( _, _ )
from prolog() ;
import
newArray (
Type, integer, ObjectId |- Objects -> Objects, ObjectId, Insts ) ,
newArrayWithValues (
Type, Vals |- Objects -> Objects, ObjectId ) ,
setArrayElement (
Ref, integer, Val, ObjectId |- Objects -> Objects, Insts ) ,
getArrayElement (
Ref, integer, ObjectId |- Objects -> Val, Objects, Insts )
from java_array_support;
var TVLit: Literal;
var TVValue, TVValue1, TVValue2, TVValue3: Val;
var TVObjRef: Ref;
var TVObjId: ObjectId;
var TVIdent, TVClName, TVObjName, TVMethName: Identifier;
var TVArgL: SemArguments;
var TVArrayInit: ArrayInitializer;
set evaluateExpression is
--SC: Evaluates an expression.
--
--SC: Allowed Expressions:
--SC: Literal (Ex: 2), Object reference (#1 or #T3), 'This' keyword,
--SC: Variable (varX), Class variable (Math.PI ie ClassName.ClassVarName)
--
--JC: Object list, Class variable list, Execution environment (parameters and
--JC: local variables), Current executing thread reference, Current object
--JC: reference, Execution mode
--JC: |- Expression to evaluate
--JC: -> Updated object and class variable lists, Updated environment,
--JC: New expression (which will be evaluated later), Instruction list to
--JC: execute at the next execution step of the current executing thread,
--JC: New status of the current executing thread.
judgement
Objects, ClassVariablesL, Env, ObjectId, ObjectId, Identifier |-
SemExpression -> Objects, ClassVariablesL, Env, SemExpression, Insts, ThreadStatus;
Literal:
--RC: If the expression is a literal, returns it.
--
--CS: 101
ObjL, ClVarL, Env, _, _, _ |- TVLit -> ObjL, ClVarL, Env, TVLit, insts[], runnable() ;
Reference:
--RC: If the expresssion is an object reference, returns it.
--
--CS: #T1 or #2
ObjL, ClVarL, Env, _, _, _ |- TVObjRef -> ObjL, ClVarL, Env, TVObjRef, insts[], runnable() ;
This:
--RC: If the expression is the 'this' keyword returns the Object
--RC: represented by the 'this' keyword
--
--CS: this
ObjL, ClVarL, Env, _, ObjId, _ |- this() -> ObjL, ClVarL, Env, ObjId, insts[], runnable() ;
IdentifierInANonStaticMethod:
--RC: If the expression (included in a non-static method) is an identifier
--RC: gets its value and returns it.
--
--CS: varX
getVariableValue(
ObjL, ClVarL, Env, ObjId |- TVIdent -> Value )
--------------------------------
ObjL, ClVarL, Env, _, ObjId, identifier "none" |-
TVIdent -> ObjL, ClVarL, Env, Value, insts[], runnable() ;
IdentifierInAStaticMethod:
--RC: If the expression (included in a static method) is an identifier,
--RC: gets its value and returns it.
--
--CS: var1
getParameterOrLocalOrStaticVariableValue(
Env, ClVarL, ClName |- TVIdent -> Value )
--------------------------------
ObjL, ClVarL, Env, _, _, ClName |- TVIdent -> ObjL, ClVarL, Env, Value, insts[], runnable() ;
provided diff( ClName, identifier "none" );
ConvertAccessToCompAccess:
--BSC: Access Expression evaluation
--
--RC: Convert an access operator into a comp_access operator.
--
--CS: Expression.Ident
evaluateExpression(
ObjL1, ClVarL1, Env1, OthId, ObjId, Mode |-
semAccess(Expr1, Ident) -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL, ThStatus )
--------------------------------
ObjL1, ClVarL1, Env1, OthId, ObjId, Mode |-
access(Expr1, Ident) -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL, ThStatus ;
ComplexAccessViaNull:
--RC: The referenced object has not been created, so its
--RC: elements cannot be accessed. So an exception is thrown.
--RC: NOTE! This rule will not catch uninitialized local variables (value = empty())
--RC: since this is a STATIC error.
--
--CS: null().Identifier
createExceptionObject(
ObjL1, OThId |-
identifier "NullPointerException", exceptText "Use of a pointer with a null value." -> _, ObjL1_1, InstL )
--------------------------------
ObjL1, ClVarL, Env, OThId, _, _ |-
semAccess(null(), _) -> ObjL1_1, ClVarL, Env, empty(), InstL, runnable() ;
ComplexAccessToAStaticVariableOrAnAttributeValue:
--RC: Retrieves the object attribute or the static variable value.
--RC: This object has already been created before this access, so its
--RC: reference is known.
--
--CS: #i.Ident;
getAttributeOrStaticVariableValue(
ObjL, ClVarL, TVObjId |- Ident -> Value )
--------------------------------
ObjL, ClVarL, Env, _, _, _ |-
semAccess(TVObjId, Ident) -> ObjL, ClVarL, Env, Value, insts[], runnable() ;
ComplexAccessToAStaticVariableValue:
--RC: Returns the class variable value.
--
--CS: Math.PI (i.e. ClName.ClassVariableName)
isAClass( TVClName -> true() ) &
getStaticVariableValue(
ClVarL, TVClName |- ClVarName -> Value )
--------------------------------
ObjL, ClVarL, Env, _, _, _ |-
semAccess(TVClName, ClVarName) -> ObjL, ClVarL, Env, Value, insts[], runnable() ;
ComplexAccess_IdentifierEvaluation:
--RC: The variable is an object name. Gets this object reference.
--
--CS: TVObjName.AttrName;
isAClass( TVObjName -> false() ) &
getVariableValue(
ObjL, ClVarL, Env, ObjId |- TVObjName -> TVObjRef )
--------------------------------
ObjL, ClVarL, Env, _, ObjId, _ |-
semAccess(TVObjName, AttrName) -> ObjL, ClVarL, Env, semAccess(TVObjRef, AttrName), insts[], runnable() ;
ComplexAccess_ExpressionEvaluation:
--RC: The left hand member of the access is not null, an object id, or
--RC: an identifier. So it is evaluated into a more simple expression
--RC: in order to evaluate this access.
--
--CS: Expression1.Identifier
--
--ESC: Access Expression Evaluation
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId1, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL, ThStatus )
--------------------------------
ObjL1, ClVarL1, Env1, OThId1, ObjId, Mode |-
semAccess(Expr1, Ident) -> ObjL1_1, ClVarL1_1, Env1_1, semAccess(Expr1_1, Ident), InstL, ThStatus ;
provided
not_eq( Expr1, objectId(_, _) ) & not_eq( Expr1, null() ) &
not_eq( Expr1, identifier _ );
ConvertArrayAccessToSemArrayAccess:
--BSC: Access Expression evaluation
--
--RC: Convert an arrayAccess operator into a semArrayAccess operator.
--
--CS: PrimaryNoNewArray [ Expression ] (Primary... is subset of Expr.)
evaluateExpression(
ObjL, ClVarL, Env, OthId, ObjId, Mode |-
semArrayAccess(Expr1, Expr2) -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OthId, ObjId, Mode |-
arrayAccess(Expr1, Expr2) -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus ;
ComplexArrayAccess_ArrayEvaluation:
--RC: The array part of the access is not yet a reference (null or object id).
--RC: Evaluate it one more step.
--
--CS: Expression1[Expression2]
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr1 -> ObjL_1, ClVarL_1, Env_1, Expr1_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semArrayAccess(Expr1, Expr2) -> ObjL_1, ClVarL_1, Env_1, semArrayAccess(Expr1_1, Expr2), InstL, ThStatus ;
provided not_eq( Expr1, objectId(_, _) ) & not_eq( Expr1, null() );
ComplexArrayAccess_IndexEvaluation:
--RC: The index part of the access is not yet an integer. Evaluate it one more step.
--
--CS: #4[Expression]
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semArrayAccess(TVObjRef, Expr) -> ObjL_1, ClVarL_1, Env_1, semArrayAccess(TVObjRef, Expr_1), InstL, ThStatus ;
provided not_eq( Expr, integer _ );
ComplexArrayAccess_NullPointer:
--RC: The array reference is null. Throw an exception. (Note that this is not
--RC: checked until the index has been fully evaluated.)
--RC: NOTE! This rule will not catch uninitialized local variables (value = empty())
--RC: since this is a STATIC error.
--
--CS: null()[7]
createExceptionObject(
ObjL, OThId |-
identifier "NullPointerException", exceptText "Use of a pointer with a null value." -> _, ObjL_1, InstL )
--------------------------------
ObjL, ClVarL, Env, OThId, _, _ |-
semArrayAccess(null(), integer _) -> ObjL_1, ClVarL, Env, empty(), InstL, runnable() ;
ComplexArrayAccess_GetElement:
--RC: Retrieves the value at the indicated index. Throws an exception if the index
--RC: is out of bounds.
--
--CS: #i[7];
getArrayElement(
TVObjId, i, OThId |- ObjL -> Value, ObjL_1, InstL )
--------------------------------
ObjL, ClVarL, Env, OThId, _, _ |-
semArrayAccess(TVObjId, integer i) -> ObjL_1, ClVarL, Env, Value, InstL, runnable() ;
NewObjectCreation:
--RC: Creates an instance of the given class and adds this instance to the
--RC: object list that contains all the objects created by the current
--RC: interpreted program. The next execution step of the current
--RC: executing thread will be the constructor call.
--
--CS: new Thread();
generateANumberForTheNewObject(
|- ObjL1 -> i ) &
createObject( OThId |- i, TVClName -> Obj, ObjId )
& appendtree( ObjL1, objects[Obj], ObjL1_1 )
--------------------------------
ObjL1, ClVarL, Env, OThId, _, _ |-
newObject(new(), TVClName, ArgL, fieldDeclarations[]) ->
ObjL1_1, ClVarL, Env, ObjId, insts[constructorCall1(TVClName, ArgL, ObjId)], runnable() ;
ConstructorCallWithoutArgument:
--BSC: Constructor Processings
--
--RC: Retrieves the constructor closure (super() was added at the top of
--RC: the constructor instruction list).
--
--CS: ClassName1()
getConstructorClosure(
ObjL, ClVarL, OThId |- TVClName, ObjId, vals[] -> Clr )
--------------------------------
ObjL, ClVarL, Env, OThId, _, _ |-
constructorCall1(TVClName, arguments[], ObjId) -> ObjL, ClVarL, Env, empty(), insts[Clr], runnable() ;
APIConstructorCallWithoutArgument:
--RC: Retrieves the API constructor closure (super() was added at the top
--RC: of the constructor instruction list).
--
--CS: Thread()
APIMethodOrConstructorCall(
ObjL1, ClVarL1, OThId, ObjId |-
TVClName, vals[] -> ObjL1_1, ClVarL1_1, insts[Clr], runnable() )
--------------------------------
ObjL1, ClVarL1, Env, OThId, _, _ |-
constructorCall1(TVClName, arguments[], ObjId) -> ObjL1_1, ClVarL1_1, Env, empty(), insts[Clr], runnable() ;
ConstructorCallWithArguments:
--RC: Before retrieving the constructor closure, the arguments need to be
--RC: evaluated. Makes an evaluation step for the first argument.
--
--CS: ClassName1(locVar2, 2+6, Obj1.Attr1)
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode |-
ArgL1 -> ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) &
appendtree( InstL1, insts[constructorCall2(ClName, ArgL1_1, TVObjRef)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode |-
constructorCall1(ClName, ArgL1, TVObjRef) -> ObjL1_1, ClVarL1_1, Env1_1, empty(), InstL1_1, runnable() ;
provided diff( ArgL1, arguments[] );
ConstructorCallWithEvaluatedArguments:
--RC: The constructor arguments are all evaluated. The corresponding
--RC: closure is retrieved and added to the instruction list.
--
--CS: ClassName1(25, 8, #4)
evaluateArgument(
ObjL, ClVarL, Env, OThId, ObjId1, Mode |- ArgL => ObjL, ClVarL, Env, ArgL, insts[] )
& convertCompArgumentsToValues( ArgL -> ValL )
&
getConstructorClosure(
ObjL, ClVarL, OThId |- ClName, ObjId2, ValL -> Clr )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId1, Mode |-
constructorCall2(ClName, ArgL, ObjId2) -> ObjL, ClVarL, Env, ObjId2, insts[Clr], runnable() ;
ConstructorCallWithArguments_ArgumentsEvaluation:
--RC: Evaluates the constructor arguments (resolves for example 2+6).
--RC: The aim is to obtain a list of simple values.
--
--CS: ClassName1(25, 2+6, Obj1.Attr1)
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode |-
ArgL1 => ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) & diff( ArgL1, ArgL1_1 )
& appendtree( InstL1, insts[constructorCall2(ClName, ArgL1_1, ObjId2)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode |-
constructorCall2(ClName, ArgL1, ObjId2) -> ObjL1_1, ClVarL1_1, Env1_1, empty(), InstL1_1, runnable() ;
APIConstructorCallWithEvaluatedArguments:
--RC: The API constructor arguments are all evaluated. The corresponding
--RC: closure is retrieved and added to the instruction list.
--
--CS: Thread("MyThread")
--
--ESC: Constructor processings
APIMethodOrConstructorCall(
ObjL1, ClVarL1, OThId, ObjId |-
TVIdent, ArgL -> ObjL1_1, ClVarL1_1, insts[Clr], runnable() )
--------------------------------
ObjL1, ClVarL1, Env, OThId, _, _ |-
constructorCall2(TVIdent, ArgL, ObjId) -> ObjL1_1, ClVarL1_1, Env, ObjId, insts[Clr], runnable() ;
provided diff( ArgL, arguments[] );
ConvertNewArray_DefaultValues:
--RC: Creates an array when some the size(s) of some of the dimensions
--RC: are given. Note that Java does not allow an array initializer
--RC: in this case.
convertDimsToSemArgs( NonEmptyDims -> Sizes ) &
appendtree( NonEmptyDims, EmptyDims, Dims ) &
computeArrayType( ElementType, Dims -> ArrayType ) &
evaluateArgument(
ObjL, ClVarL, Env, OThId, ObjId, Mode |- Sizes => ObjL_1, ClVarL_1, Env_1, Sizes_1, InstL
)
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
newArray(ElementType, NonEmptyDims, EmptyDims, arrayInitializer[]) ->
ObjL_1, ClVarL_1, Env_1, semNewArray(ArrayType, Sizes_1), InstL, runnable() ;
provided diff( NonEmptyDims, dims[] );
ConvertNewArray_ArrayInitializer:
--RC: Creates an array when an array initializer is given. Note that
--RC: Java does not allow any dimension sizes to be given in this case.
computeArrayType( ElementType, Dims -> ArrayType ) &
convertArrayInitializerToSemArgument(
ArrayType, ArrayInit -> Expr ) &
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
newArray(ElementType, dims[], Dims, ArrayInit) -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus ;
CreateNewArray_EvaluateSizes:
evaluateArgument(
ObjL, ClVarL, Env, OThId, ObjId, Mode |- Sizes => ObjL_1, ClVarL_1, Env_1, Sizes_1, InstL
)
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semNewArray(ArrayType, Sizes) -> ObjL_1, ClVarL_1, Env_1, semNewArray(ArrayType, Sizes_1), InstL, runnable() ;
provided
not_eq( Sizes, vals[_] ) &
allAreValues( Sizes -> false() );
CreateNewArray_SizesEvaluated:
convertCompArgumentsToValues( Sizes -> Sizes_1 )
&
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semNewArray(ArrayType, Sizes_1) -> ObjL_1, ClVarL_1, Env_1, Expr, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semNewArray(ArrayType, Sizes) -> ObjL_1, ClVarL_1, Env_1, Expr, InstL, ThStatus ;
provided
not_eq( Sizes, vals[_] ) &
allAreValues( Sizes -> true() );
-- !!! Should check for negative sizes somehow and throw an exception in that
-- !!! case. Or is it good enough to do let arraySupport check for it?
CreateNewArray_OneDimensional:
newArray(
ArrayType, n, OThId |- ObjL -> ObjL_1, ArrayId, InstL )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semNewArray(ArrayType, vals[integer n]) -> ObjL_1, ClVarL, Env, ArrayId, InstL, runnable() ;
CreateNewArray_MultiDimensional:
makeNewArrayExprList( n, ArrayType, Sizes -> Exprs ) &
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semNewInitializedArray(arrayof(ArrayType), Exprs) -> ObjL_1, ClVarL_1, Env_1, Expr, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semNewArray(arrayof(ArrayType), vals[integer n.Sizes]) -> ObjL_1, ClVarL_1, Env_1, Expr, InstL, ThStatus ;
provided not_eq( Sizes, vals[] );
CreateNewInitializedArray_EvaluateElements:
evaluateArgument(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
ArrayElems => ObjL_1, ClVarL_1, Env_1, ArrayElems_1, InstL )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semNewInitializedArray(ArrayType, ArrayElems) ->
ObjL_1, ClVarL_1, Env_1, semNewInitializedArray(ArrayType, ArrayElems_1), InstL, runnable() ;
provided allAreValues( ArrayElems -> false() );
CreateNewInitializedArray_Creation:
convertCompArgumentsToValues( ArrayElems -> ArrayElems_1 )
&
newArrayWithValues(
ArrayType, ArrayElems_1 |- ObjL -> ObjL_1, ArrayId )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semNewInitializedArray(ArrayType, ArrayElems) -> ObjL_1, ClVarL, Env, ArrayId, insts[], runnable() ;
provided allAreValues( ArrayElems -> true() );
ConvertPrefixIncr:
--RC: Translates e.g. ++i into i+=1.
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
binaryAssign(Expr, plusAssignment(), integer 1) -> ObjL_1, ClVarL_1, Env_1, Expr1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
prefix(incr(), Expr) -> ObjL_1, ClVarL_1, Env_1, Expr1, InstL, ThStatus ;
ConvertPrefixDecr:
--RC: Translates e.g. --i into i-=1.
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
binaryAssign(Expr, minusAssignment(), integer 1) -> ObjL_1, ClVarL_1, Env_1, Expr1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
prefix(decr(), Expr) -> ObjL_1, ClVarL_1, Env_1, Expr1, InstL, ThStatus ;
ConvertPostfixIncr:
--RC: Translates e.g. i++ into (i+=1)-1.
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
binary(binaryAssign(Expr, plusAssignment(), integer 1), minus(), integer 1) ->
ObjL_1, ClVarL_1, Env_1, Expr1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
postfix(Expr, incr()) -> ObjL_1, ClVarL_1, Env_1, Expr1, InstL, ThStatus ;
ConvertPostfixDecr:
--RC: Translates e.g. i-- into (i-=1)+1.
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
binary(binaryAssign(Expr, minusAssignment(), integer 1), plus(), integer 1) ->
ObjL_1, ClVarL_1, Env_1, Expr1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
postfix(Expr, decr()) -> ObjL_1, ClVarL_1, Env_1, Expr1, InstL, ThStatus ;
ConvertAssignIntoAssignComp1:
--BSC: Assignment
--
--RC: Convert an assign into a assign_comp before starting the
--RC: assignment.
--
--CS: Ident = Expression2;
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
semAssign(empty(), TVIdent, AOp, Expr1) -> ObjL1_1, ClVarL1_1, Env1_1, Expr2, InstL, ThStatus )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
binaryAssign(TVIdent, AOp, Expr1) -> ObjL1_1, ClVarL1_1, Env1_1, Expr2, InstL, ThStatus ;
ConvertAssignIntoAssignComp2:
--RC: Convert an assign into a assign_comp before starting theö
--RC: assignment.
--
--CS: Expression1 = Expression2;
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
semAssign(Expr2, Ident, AOp, Expr1) -> ObjL1_1, ClVarL1_1, Env1_1, Expr3, InstL, ThStatus )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
binaryAssign(access(Expr2, Ident), AOp, Expr1) -> ObjL1_1, ClVarL1_1, Env1_1, Expr3, InstL, ThStatus ;
ClassVariableAssignment_LastStep:
--RC: The value is assigned to the class variable.
--
--CS: ClassName2.ClVarName3 = 25;
setClassVariable(
TVClName, ClVarName, TVValue |- ClVarL1 -> ClVarL1_1 )
--------------------------------
ObjL, ClVarL1, Env, _, _, _ |-
semAssign(TVClName, ClVarName, assignment(), TVValue) -> ObjL, ClVarL1_1, Env, TVValue, insts[], runnable() ;
provided
isAClass( TVClName -> true() );
ClassVariableAssignment_HandleCompoundAssignment:
--RC: Translates e.g. A.b += 25 to A.b = A.b + 25. Safe since all parts
--RC: have been evaluated.
--CS: ClassName2.ClVarName3 += 25;
getOpFromCompundAssignOp( AOp -> Op ) &
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(TVClName, ClVarName, assignment(), binary(semAccess(TVClName, ClVarName), Op, TVValue)) ->
ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(TVClName, ClVarName, AOp, TVValue) -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus ;
provided
isAClass( TVClName -> true() ) &
isCompoundAssignOp( AOp -> true() );
ClassVariableAssignment_RightHandMemberEvaluation:
--RC: Before being assigned to the class variable, the right member needs
--RC: to be evaluated.
--
--CS: ClassName1.ClVarName2 = Obj.attr5;
isAClass( TVClName -> true() ) &
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(TVClName, ClVarName, AOp, Expr) ->
ObjL_1, ClVarL_1, Env_1, semAssign(TVClName, ClVarName, AOp, Expr_1), InstL, ThStatus ;
ComplexAssignValueToASimpleVariable:
--RC: Assigns a value to a variable (parameter or local variable).
--
--CS: var1 = 10;
assign(
ObjL1, ClVarL1, Env1, ObjId |- Ident, TVValue -> ObjL1_1, ClVarL1_1, Env1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, _, ObjId, _ |-
semAssign(empty(), Ident, assignment(), TVValue) -> ObjL1_1, ClVarL1_1, Env1_1, TVValue, insts[], runnable() ;
ComplexAssignValueToASimpleVariable_HandleCompoundAssignment:
--RC: Translates e.g. a += 25 to a = a + 25. Safe since all parts
--RC: have been evaluated.
--
--CS: var1 += 10;
getOpFromCompundAssignOp( AOp -> Op ) &
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(empty(), Ident, assignment(), binary(Ident, Op, TVValue)) ->
ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(empty(), Ident, AOp, TVValue) -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus ;
provided isCompoundAssignOp( AOp -> true() );
ComplexAssignExpressionToASimpleVariable:
--RC: Evaluates the right member of the assignment before assigning the
--RC: variable.
--
--CS: var1 = 25 + var2;
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(empty(), Ident, AOp, Expr) ->
ObjL_1, ClVarL_1, Env_1, semAssign(empty(), Ident, AOp, Expr_1), InstL, ThStatus ;
ComplexAssignValueToAnAttributeOrAStaticVariable:
--RC: Assigns a value to an attribute or a static variable.
--
--CS: #4.Attr = 25;
setAttributeOrStaticVariable(
ObjL1, ClVarL1, TVObjId |- Ident, TVValue -> ObjL1_1, ClVarL1_1 )
--------------------------------
ObjL1, ClVarL1, Env, _, _, _ |-
semAssign(TVObjId, Ident, assignment(), TVValue) -> ObjL1_1, ClVarL1_1, Env, TVValue, insts[], runnable() ;
ComplexAssignValueToAnAttributeOrAStaticVariable_HandleCompoundAssignment:
--RC: Translates e.g. #1.a += 25 to #1.a = #1.a + 25. Safe since all
--RC: parts have been evaluated.
--
--CS: #4.Attr = 25;
getOpFromCompundAssignOp( AOp -> Op ) &
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(TVObjId, Ident, assignment(), binary(semAccess(TVObjId, Ident), Op, TVValue)) ->
ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(TVObjId, Ident, AOp, TVValue) -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus ;
provided isCompoundAssignOp( AOp -> true() );
ComplexAssignExpressionViaNull:
--RC: Attempt to assign via a null reference to an object.
--RC: Throw an exception.
--
--CS: null().Attr = Var1 * Var2;
createExceptionObject(
ObjL1_1, OThId |-
identifier "NullPointerException", exceptText "Use of a pointer with a null value." -> _, ObjL1_2, InstL )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode |-
semAssign(null(), _, _, _) -> ObjL1_2, ClVarL1_1, Env1_1, empty(), InstL, runnable() ;
ComplexAssignExpressionToAnAttributeOrAStaticVariable:
--RC: Evaluates the right member of the assignment before assigning the
--RC: attribute or the class variable.
--
--CS: #4.Attr = 5 * var3;
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(TVObjId, Ident, AOp, Expr) ->
ObjL_1, ClVarL_1, Env_1, semAssign(TVObjId, Ident, AOp, Expr_1), InstL, ThStatus ;
ComplexAssignement_LeftHandMemberEvaluation:
--RC: Evaluates the left member of the assignment before the evaluation
--RC: of the right member and the assignment.
--
--CS: ObjName1.ObjAttr1.ObjAttr3 = 25 * Var5 + Var1;
--
--ESC: Assignment
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr1 -> ObjL_1, ClVarL_1, Env_1, Expr1_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semAssign(Expr1, Ident, AOp, Expr2) ->
ObjL_1, ClVarL_1, Env_1, semAssign(Expr1_1, Ident, AOp, Expr2), InstL, ThStatus ;
ConvertArrayAssignmentToSemArrayAssign:
--RC: Convert an assignment to an array element into a semArrayAssign operator.
--
--CS: Expression1[Expression2] = Expression3.
evaluateExpression(
ObjL, ClVarL, Env, OthId, ObjId, Mode |-
semArrayAssign(Expr1, Expr2, AOp, Expr3) -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OthId, ObjId, Mode |-
binaryAssign(arrayAccess(Expr1, Expr2), AOp, Expr3) -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus ;
ComplexArrayAssignment_ArrayEvaluation:
--RC: The array part of the assignment access is not yet a reference (null or object
--RC: id). Evaluate it one more step.
--
--CS: Expression1[Expression2] = Expression3
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr1 -> ObjL_1, ClVarL_1, Env_1, Expr1_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semArrayAssign(Expr1, Expr2, AOp, Expr3) ->
ObjL_1, ClVarL_1, Env_1, semArrayAssign(Expr1_1, Expr2, AOp, Expr3), InstL, ThStatus ;
provided not_eq( Expr1, objectId(_, _) ) & not_eq( Expr1, null() );
ComplexArrayAssignment_IndexEvaluation:
--RC: The index part of the access is not yet an integer. Evaluate it one more step.
--
--CS: #4[Expression2] = Expression3
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr2 -> ObjL_1, ClVarL_1, Env_1, Expr2_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semArrayAssign(TVObjRef, Expr2, AOp, Expr3) ->
ObjL_1, ClVarL_1, Env_1, semArrayAssign(TVObjRef, Expr2_1, AOp, Expr3), InstL, ThStatus ;
provided not_eq( Expr2, integer _ );
ComplexArrayAssignment_ValueEvaluation:
--RC: The value has not yet been fully evaluated. Evaluate it one more step.
--
--CS: #4[7] = Expression3
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr3 -> ObjL_1, ClVarL_1, Env_1, Expr3_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semArrayAssign(TVObjRef, integer i, AOp, Expr3) ->
ObjL_1, ClVarL_1, Env_1, semArrayAssign(TVObjRef, integer i, AOp, Expr3_1), InstL, ThStatus ;
provided isValue( Expr3 -> false() );
ComplexArrayAssignment_NullPointer:
--RC: The array reference is null. Throw an exception. (Note that this is not
--RC: checked until the index and the value has been fully evaluated.)
--RC: NOTE! This rule will not catch uninitialized local variables (value = empty())
--RC: since this is a STATIC error.
--
--CS: null()[7] = 42
createExceptionObject(
ObjL1, OThId |-
identifier "NullPointerException", exceptText "Use of a pointer with a null value." -> _, ObjL1_1, InstL )
--------------------------------
ObjL1, ClVarL, Env, OThId, _, _ |-
semArrayAssign(null(), integer _, _, TVValue) -> ObjL1_1, ClVarL, Env, empty(), InstL, runnable() ;
ComplexArrayAssignment_SetElement:
--RC: Sets the element at the indicated index to value. An exception is thrown
--RC: if the index is out of bounds, or if the element type is incompatible with
--RC: the dynamic type of the array.
--
--CS: #1[7] = 10;
setArrayElement(
TVObjId, i, TVValue, OThId |- ObjL -> ObjL_1, InstL )
--------------------------------
ObjL, ClVarL, Env, OThId, _, _ |-
semArrayAssign(TVObjId, integer i, assignment(), TVValue) -> ObjL_1, ClVarL, Env, TVValue, InstL, runnable() ;
ComplexArrayAssignment_HandleCompoundAssignment:
--RC: Translates e.g. #1[7] += 25 to #1[7] = #1[7] + 25. Safe since all
--RC: parts have been evaluated.
--
--CS: #1[7] = 10;
getOpFromCompundAssignOp( AOp -> Op ) &
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semArrayAssign(TVObjId, integer i, assignment(), binary(semArrayAccess(TVObjId, integer i), Op, TVValue)) ->
ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
semArrayAssign(TVObjId, integer i, AOp, TVValue) -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus ;
provided isCompoundAssignOp( AOp -> true() );
ExceptionThrownDuringABinaryOperationEvaluation:
--BSC: Binary Operator Expression
--
--RC: The binary operator evaluation has thrown an exception (for
--RC: example at the time of a division by zero).
--
--CS: 25 / 0;
evaluateBinaryOperation(
|- TVValue1, TVValue2, BinOp -> except(ClName, null(), ExceptText) )
&
createExceptionObject(
ObjL1, OThId |- ClName, ExceptText -> _, ObjL1_1, InstL )
--------------------------------
ObjL1, ClVarL, Env, OThId, _, _ |-
binary(TVValue1, BinOp, TVValue2) -> ObjL1_1, ClVarL, Env, empty(), InstL, runnable() ;
BinaryOperationBetweenTwoValues:
--RC: Evaluates the binary operation between the two values.
--
--CS: 25 + 4 or 100 < 200
evaluateBinaryOperation(
|- TVValue1, TVValue2, BinOp -> TVValue3 )
--------------------------------
ObjL1, ClVarL1, Env1, _, _, _ |-
binary(TVValue1, BinOp, TVValue2) -> ObjL1, ClVarL1, Env1, TVValue3, insts[], runnable() ;
BinaryOperation_LogicalOrWithTrueAsLeftValue:
--RC: The left member of the binary operation is already a value.
--
--CS: true() || ...
ObjL, ClVarL, Env, _, _, _ |-
binary(true(), lor(), _) -> ObjL, ClVarL, Env, true(), insts[], runnable() ;
BinaryOperation_LogicalAndWithFalseAsLeftValue:
--RC: The left member of the binary operation is already a value. The
--RC: right member is still an expression which needs to be evaluated
--RC: before the evaluation of the binary operation.
--
--CS: false() && .....
ObjL, ClVarL, Env, _, _, _ |-
binary(false(), land(), _) -> ObjL, ClVarL, Env, false(), insts[], runnable() ;
BinaryOperation_RightHandMemberEvaluation:
--RC: The left member of the binary operation is already a value. The
--RC: right member is still an expression which needs to be evaluated
--RC: before the evaluation of the binary operation.
--
--CS: 25 + Obj1.Attr3
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId1, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL, ThStatus )
--------------------------------
ObjL1, ClVarL1, Env1, OThId1, ObjId, Mode |-
binary(TVValue, BinOp, Expr1) -> ObjL1_1, ClVarL1_1, Env1_1, binary(TVValue, BinOp, Expr1_1), InstL, ThStatus ;
BinaryOperation_LeftHandMemberEvaluation:
--RC: The left member of the binary operation is still an expression which
--RC: needs to be evaluated before the evaluation of the right member.
--
--CS: Obj2.Attr4 + Obj1.Attr3
--
--ESC: Binary Operator Expression
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId1, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL1, ThStatus )
--------------------------------
ObjL1, ClVarL1, Env1, OThId1, ObjId, Mode |-
binary(Expr1, BinOp, Expr2) -> ObjL1_1, ClVarL1_1, Env1_1, binary(Expr1_1, BinOp, Expr2), InstL1, ThStatus ;
UnaryOperation_ArgumentEvaluation:
--RC: The argument is not yet a value. Evaluate it one more step.
--
--CS: -(7 + 3) or !(true && false)
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr -> ObjL_1, ClVarL_1, Env_1, Expr_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
unary(UnOp, Expr) -> ObjL_1, ClVarL_1, Env_1, unary(UnOp, Expr_1), InstL, ThStatus ;
provided isValue( Expr -> false() );
UnaryOperation_ApplyOperator:
--RC: Applies an unary to a value.
--RC: Unary operators don't throw exceptions.
--
--CS: -7 or !true
evaluateUnaryOperation(
|- TVValue, UnOp -> Result )
--------------------------------
ObjL, ClVarL, Env, _, _, _ |-
unary(UnOp, TVValue) -> ObjL, ClVarL, Env, Result, insts[], runnable() ;
CondExpr_PrediceteEvaluation:
--RC: The predicate is not yet a value. Evaluate it one more step.
--
--CS: p ? e1 : e2
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Pred -> ObjL_1, ClVarL_1, Env_1, Pred_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
cond(Pred, Expr1, Expr2) -> ObjL_1, ClVarL_1, Env_1, cond(Pred_1, Expr1, Expr2), InstL, ThStatus ;
provided isValue( Pred -> false() );
CondExpr_PredIsTrue:
--RC: Predicate evaluated to true. Select left expression for further
--RC: evaluation.
--
--CS: true ? e1 : e2
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr1 -> ObjL_1, ClVarL_1, Env_1, Expr1_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
cond(true(), Expr1, _) -> ObjL_1, ClVarL_1, Env_1, Expr1_1, InstL, ThStatus ;
CondExpr_PredIsFalse:
--RC: Predicate evaluated to true. Select left expression for further
--RC: evaluation.
--
--CS: false ? e1 : e2
evaluateExpression(
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
Expr2 -> ObjL_1, ClVarL_1, Env_1, Expr2_1, InstL, ThStatus )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
cond(false(), _, Expr2) -> ObjL_1, ClVarL_1, Env_1, Expr2_1, InstL, ThStatus ;
ThisWithoutArgument:
--BSC: This() Call Expression
--
--RC: This expression is only used in a constructor declaraction to invoke
--RC: the class constructor without argument.
--
--CS: this();
--
--PC: Firstly the class name and the corresponding class declaration are
--PC: retrieved. Finally, the obtained closure is added to the current
--PC: thread instruction list.
getThreadCurrentMethod( OThId |- ObjL -> ClName )
&
getConstructorClosure(
ObjL, ClVarL, OThId |- ClName, ObjId, vals[] -> Clr )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, _ |-
thisInvocation(arguments[]) -> ObjL, ClVarL, Env, empty(), insts[Clr], runnable() ;
ThisWithArguments_FirstArgumentsEvaluation:
--RC: This expression is only used in a constructor declaration to invoke
--RC: another constructor that also belongs to this same class. The
--RC: arguments used for this constructor need firstly to be evaluated.
--
--CS: this(Obj2.Attr5, 3+6*9, Obj1.getVal());
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
ArgL1 -> ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) &
appendtree( InstL1, insts[thisCall(this(), ArgL1_1)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
thisInvocation(ArgL1) -> ObjL1_1, ClVarL1_1, Env1_1, ObjId, InstL1_1, runnable() ;
provided diff( ArgL1, arguments[] );
ThisWithArguments_ArgumentsEvaluation:
--RC: The arguments of the this() call (used in a constructor to invoke an
--RC: other constructor of the same class) are evaluated step by step.
--
--CS: this(345, 3+6*9, Obj1.getVal());
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId1, ObjId, Mode |-
ArgL1 => ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) & diff( ArgL1, ArgL1_1 )
& appendtree( InstL1, insts[thisCall(this(), ArgL1_1)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId1, ObjId, Mode |-
thisCall(this(), ArgL1) -> ObjL1_1, ClVarL1_1, Env1_1, ObjId, InstL1_1, runnable() ;
ThisWithArguments_EvaluatedArguments:
--RC: All the arguments of the this() call (used in a constructor to
--RC: invoke another constructor of the same class) have been evaluated.
--RC: So the closure corresponding to this this() call is retrieved and
--RC: added to the current thread instruction list.
--
--CS: this(345, 57, 959);
--
--ESC: This() Call Expression
evaluateArgument(
ObjL, ClVarL, Env1, OThId, ObjId, Mode |- ArgL => ObjL, ClVarL, Env1, ArgL, insts[] )
& convertCompArgumentsToValues( ArgL -> ValueL )
&
getThreadCurrentMethod( OThId |- ObjL -> ClName )
&
getConstructorClosure(
ObjL, ClVarL, OThId |- ClName, ObjId, ValueL -> Clr )
--------------------------------
ObjL, ClVarL, Env1, OThId, ObjId, Mode |-
thisCall(this(), ArgL) -> ObjL, ClVarL, Env1, empty(), insts[Clr], runnable() ;
SuperWithoutArgument:
--BSC: Super Call Expression
--
--RC: This expression is only used in a constructor declaraction to invoke
--RC: the super class constructor (direct ancestor of the current class)
--RC: without argument.
--
--CS: super();
--
--PC: Firstly the current class and its direct ancestor are retrieved.
--PC: Finally, the obtained closure is added to the current thread
--PC: instruction list.
getThreadCurrentMethod( OThId |- ObjL -> ClName1 )
&
getDirectAncestor(
|- ClName1 -> ClName2 ) &
getConstructorClosure(
ObjL, ClVarL, OThId |- ClName2, ObjId, vals[] -> Clr )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, _ |-
superInvocation(arguments[]) -> ObjL, ClVarL, Env, OThId, insts[Clr], runnable() ;
SuperWithArguments_FirstArgumentsEvaluation:
--RC: This expression is only used in a constructor declaration to invoke
--RC: its direct ancestor constructor with its arguments. These latters
--RC: need firstly to be evaluated.
--
--CS: super(Obj2.Attr5, 3+6*9, Obj1.getVal());
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
ArgL1 -> ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) &
appendtree( InstL1, insts[superCall(super(), ArgL1_1)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
superInvocation(ArgL1) -> ObjL1_1, ClVarL1_1, Env1_1, empty(), InstL1_1, runnable() ;
provided diff( ArgL1, arguments[] );
SuperWithArguments_ArgumentsEvaluation:
--RC: The arguments of the super() call (used in a constructor to invoke
--RC: its direct ancestor constructor) are evaluated step by step.
--
--CS: super(345, 3+6*9, Obj1.getVal());
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
ArgL1 => ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) & diff( ArgL1, ArgL1_1 )
& appendtree( InstL1, insts[superCall(super(), ArgL1_1)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
superCall(super(), ArgL1) -> ObjL1_1, ClVarL1_1, Env1_1, empty(), InstL1_1, runnable() ;
SuperWithArguments_EvaluatedArguments:
--RC: All the arguments of the super() call (used in a constructor to
--RC: invoke its direct ancestor constructor have been evaluated.
--RC: So the closure corresponding to this super() call is retrieved and
--RC: added to the current thread instruction list.
--
--CS: super(345, 57, 959);
--
--ESC: Super() Call Expression
evaluateArgument(
ObjL, ClVarL, Env, OThId, ObjId, Mode |- TVArgL => ObjL, ClVarL, Env, TVArgL, insts[] )
&
convertCompArgumentsToValues( TVArgL -> ValueL )
&
getThreadCurrentMethod( OThId |- ObjL -> ClName1 )
&
getDirectAncestor(
|- ClName1 -> ClName2 ) &
getConstructorClosure(
ObjL, ClVarL, OThId |- ClName2, ObjId, ValueL -> Clr )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
superCall(super(), TVArgL) -> ObjL, ClVarL, Env, empty(), insts[Clr], runnable() ;
MethodCallWithoutReference_ReferenceRetrieval:
--BSC: Method call expression
--
--RC: This method is called without reference. That means that the method
--RC: is applied on the current object. Moreover, a special variable
--RC: called 7RETURN is added to the local variable list in order to handle
--RC: the value returned by this method.
--
--CS: getVal2();
addReturnVariableInLocalVariableList( LocVarL1 -> LocVarL1_1 )
--------------------------------
ObjL, ClVarL, env(ParamL, LocVarL1), _, ObjId, identifier "none" |-
call(TVMethName, ArgL) ->
ObjL, ClVarL, env(ParamL, LocVarL1_1), identifier "7RETURN", insts[methodCall1(identifier "virtual", ObjId, TVMethName, ArgL)],
runnable() ;
MethodCallWithoutReferenceInAStaticMethod:
--RC: This method is called without reference in a static method. So that
--RC: is a static method. Moreover, a special variable called 7RETURN
--RC: is added to the local variable list in order to handle the value
--RC: returned by this method.
--
--CS: getInstancesNumber();
addReturnVariableInLocalVariableList( LocVarL1 -> LocVarL1_1 )
--------------------------------
ObjL, ClVarL, env(ParamL, LocVarL1), _, _, ClName |-
call(TVMethName, ArgL) ->
ObjL, ClVarL, env(ParamL, LocVarL1_1), identifier "7RETURN", insts[staticMethodCall1(ClName, TVMethName, ArgL)], runnable() ;
provided diff( ClName, identifier "none" );
MethodCallWithAnEmptyObjectReference:
--RC: This method is called with a class name. That means that this method
--
--CS: null.currentThread();
createExceptionObject(
ObjL1, OThId |-
identifier "NullPointerException", exceptText "Use of a pointer with a null value." -> _, ObjL1_1, InstL )
--------------------------------
ObjL1, ClVarL, Env, OThId, _, _ |-
call(access(null(), MethName), ArgL) -> ObjL1_1, ClVarL, Env, empty(), InstL, runnable() ;
MethodCallWithAClassName:
--RC: This method is called with a class name. That means that this method
--RC: is static. Moreover, a special variable called 7RETURN is added to
--RC: the local variable list in order to handle the value returned by
--RC: this static method.
--
--CS: Thread.currentThread();
isAClass( TVClName -> true() ) &
addReturnVariableInLocalVariableList( LocVarL1 -> LocVarL1_1 )
--------------------------------
ObjL, ClVarL, env(ParamL, LocVarL1), _, _, _ |-
call(access(TVClName, MethName), ArgL) ->
ObjL, ClVarL, env(ParamL, LocVarL1_1), identifier "7RETURN", insts[staticMethodCall1(TVClName, MethName, ArgL)], runnable() ;
MethodCallOnAnObject:
--RC: This method is called on an object (so this method is non static).
--RC: Moreover, a special variable called 7RETURN is added to the local
--RC: variable list in order to handle the value returned by this method.
--
--CS: myObject.setAttrValue(var2 - var1);
getVariableValue(
ObjL, ClVarL, env(ParamL, LocVarL1), ObjId |- TVObjName -> TVObjRef )
&
addReturnVariableInLocalVariableList( LocVarL1 -> LocVarL1_1 )
--------------------------------
ObjL, ClVarL, env(ParamL, LocVarL1), _, ObjId, _ |-
call(access(TVObjName, MethName), ArgL) ->
ObjL, ClVarL, env(ParamL, LocVarL1_1), identifier "7RETURN", insts[methodCall1(identifier "virtual", TVObjRef, MethName, ArgL)],
runnable() ;
MethodCall_TargetEvaluationWithAnotherMethodCall:
--RC: Before executing the given method, the target object represented
--RC: here by a method call must be retrieved. Therefore this method call
--RC: is evaluated. Moreover, a special variable called 7RETURN is added to
--RC: the local variable list in order to handle the value returned by
--RC: this method.
--
--CS: myObject.bar().setAttrValue(var2 - var1);
evaluateExpression(
ObjL1, ClVarL1, Env, OThId, ObjId, Mode |-
call(Expr1, ArgL1) -> ObjL1_1, ClVarL1_1, env(ParamL1, LocVarL1), _, InstL1, ThStatus )
& diff( InstL1, insts[] ) &
appendtree( InstL1, insts[call(access(identifier "7RETURN", MethName), ArgL2)], InstL1_1 ) &
addReturnVariableInLocalVariableList( LocVarL1 -> LocVarL1_1 )
--------------------------------
ObjL1, ClVarL1, Env, OThId, ObjId, Mode |-
call(access(call(Expr1, ArgL1), MethName), ArgL2) ->
ObjL1_1, ClVarL1_1, env(ParamL1, LocVarL1_1), identifier "7RETURN", InstL1_1, ThStatus ;
MethodCall_TargetEvaluationWithNoOtherMethodCall:
--RC: Before executing the given method, the target object represented
--RC: here by an expression must be retrieved. Therefore this expression
--RC: is evaluated. Moreover, a special variable called 7RETURN is added to
--RC: the local variable list in order to handle the value returned by
--RC: this method.
--
--CS: myObject.Attr1.setAttrValue(var2 - var1);
not_eq( Expr1, call(_, _) ) &
evaluateExpression(
ObjL1, ClVarL1, Env, OThId, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, env(ParamL1, LocVarL1), Expr1_1, insts[], ThStatus ) &
appendtree(
insts[semAssign(empty(), identifier "7RETURN", assignment(), Expr1_1)], insts[call(access(identifier "7RETURN", MethName), ArgL)],
InstL2_1 ) &
addReturnVariableInLocalVariableList( LocVarL1 -> LocVarL1_1 )
--------------------------------
ObjL1, ClVarL1, Env, OThId, ObjId, Mode |-
call(access(Expr1, MethName), ArgL) ->
ObjL1_1, ClVarL1_1, env(ParamL1, LocVarL1_1), identifier "7RETURN", InstL2_1, ThStatus ;
NonStaticMethodCalledOnANonCreatedObject:
--RC: The method is called on a non created object. So an exception is
--RC: thrown.
--
--CS: void().getValue();
createExceptionObject(
ObjL1, OThId |-
identifier "NullPointerException", exceptText "Use of a pointer with a null value." -> _, ObjL1_1, InstL )
--------------------------------
ObjL1, ClVarL, Env, OThId, _, _ |-
methodCall1(_, null(), _, _) -> ObjL1_1, ClVarL, Env, empty(), InstL, runnable() ;
NonStaticMethodCallAPI_WithoutArgument:
--RC: The given method is a defined javacard API. This API does not have
--RC: argument.
--
--CS: myThread.start();
APIMethodOrConstructorCall(
ObjL1, ClVarL1, OThId, TVObjId |- MethName, vals[] -> ObjL1_1, ClVarL1_1, InstL, ThStatus
)
--------------------------------
ObjL1, ClVarL1, Env, OThId, _, _ |-
methodCall1(_, TVObjId, MethName, arguments[]) -> ObjL1_1, ClVarL1_1, Env, empty(), InstL, ThStatus ;
NonStaticMethodCallWithoutArgument_ClosureAddition:
--RC: Gets the closure corresponding to the given method call (this call
--RC: does not have any argument to evaluate) and adds it to the current
--RC: thread instruction list. (in this case, the object, on which the
--RC: given method has been called, has already been created).
--
--CS: #5.getValue();
getMethodClosure( ObjL |- MethName, TVObjId, vals[] -> Clr )
--------------------------------
ObjL, ClVarL, Env, _, _, _ |-
methodCall1(_, TVObjId, MethName, arguments[]) -> ObjL, ClVarL, Env, empty(), insts[Clr], runnable() ;
NonStaticMethodCallWithArguments_FirstArgumentEvaluation:
--RC: One evaluation step of the first argument is made.
--
--CS: #4.myMethod(Obj2.Attr2, 3+6*9, Obj1.getVal());
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode1 |-
ArgL1 -> ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) & diff( ArgL1, ArgL1_1 )
& appendtree( InstL1, insts[methodCall2(Mode2, TVObjId, MethName, ArgL1_1)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode1 |-
methodCall1(Mode2, TVObjId, MethName, ArgL1) -> ObjL1_1, ClVarL1_1, Env1_1, empty(), InstL1_1, runnable() ;
provided diff( ArgL1, arguments[] );
NonStaticMethodCallWithEvaluatedArguments_ClosureAddition:
--RC: All the arguments of the method call have been evaluated. So the
--RC: method declaration and the corresponding closure are retrieved.
--
--CS: #4.myMethod(345, 57, false);
evaluateArgument(
ObjL, ClVarL, Env, OThId, ObjId1, Mode |- ArgL => ObjL, ClVarL, Env, ArgL, insts[] )
& convertCompArgumentsToValues( ArgL -> ValueL )
&
getMethodClosure( ObjL |- MethName, ObjId2, ValueL -> Clr )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId1, Mode |-
methodCall2(_, ObjId2, MethName, ArgL) -> ObjL, ClVarL, Env, empty(), insts[Clr], runnable() ;
NonStaticMethodCallWithArguments_ArgumentsEvaluation:
--RC: The arguments of the method call are evaluated step by step before
--RC: the method declaration retrieval.
--
--CS: #4.myMethod(#5.Attr2, 3+6*9, Obj1.getVal());
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode1 |-
ArgL1 => ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) & diff( ArgL1, ArgL1_1 )
& appendtree( InstL1, insts[methodCall2(Mode2, ObjId2, MethName, ArgL1_1)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId1, Mode1 |-
methodCall2(Mode2, ObjId2, MethName, ArgL1) -> ObjL1_1, ClVarL1_1, Env1_1, empty(), InstL1_1, runnable() ;
NonStaticMethodCallAPI_WithEvaluatedArguments:
--RC: The given method is a defined javacard API. This API has arguments
--RC: which have been evaluated.
--
--CS: #4.wait(45);
evaluateArgument(
ObjL, ClVarL, Env, OThId, ObjId1, Mode |- ArgL => ObjL, ClVarL, Env, ArgL, insts[] )
& convertCompArgumentsToValues( ArgL -> ValueL )
&
APIMethodOrConstructorCall(
ObjL1, ClVarL1, OThId, ObjId2 |- MethName, ValueL -> ObjL1_1, ClVarL1_1, InstL, ThStatus )
--------------------------------
ObjL1, ClVarL1, Env, OThId, ObjId1, Mode |-
methodCall2(_, ObjId2, MethName, ArgL) -> ObjL1_1, ClVarL1_1, Env, empty(), InstL, ThStatus ;
StaticMethodCallWithoutArgument:
--RC: The static method call has no argument. So the corresponding closure
--RC: is retrieved.
--
--CS: MyClass.getInstanceNumber();
getStaticMethodClosure(
ObjL, OThId |- MethName, ClName, vals[] -> Clr )
--------------------------------
ObjL, ClVarL, Env, OThId, _, _ |-
staticMethodCall1(ClName, MethName, arguments[]) -> ObjL, ClVarL, Env, empty(), insts[Clr], runnable() ;
StaticMethodCallWithArguments_FirstArgumentEvaluation:
--RC: One evaluation step of the first argument is made.
--
--CS: MyClass.myMethod(Obj2.Attr2, 3+6*9, Obj1.getVal());
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
ArgL1 -> ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) &
appendtree( InstL1, insts[staticMethodCall2(ClName, MethName, ArgL1_1)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
staticMethodCall1(ClName, MethName, ArgL1) -> ObjL1_1, ClVarL1_1, Env1_1, empty(), InstL1_1, runnable() ;
provided diff( ArgL1, arguments[] );
StaticMethodCallWithArguments_ArgumentsEvaluation:
--RC: The arguments of the static method call are evaluated step by step
--RC: before the method declaration retrieval.
--
--CS: MyClass.myMethod(#5.Attr2, 3+6*9, Obj1.getVal());
evaluateArgument(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
ArgL1 => ObjL1_1, ClVarL1_1, Env1_1, ArgL1_1, InstL1 ) & diff( ArgL1, ArgL1_1 )
& appendtree( InstL1, insts[staticMethodCall2(ClName, MethName, ArgL1_1)], InstL1_1 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
staticMethodCall2(ClName, MethName, ArgL1) -> ObjL1_1, ClVarL1_1, Env1_1, empty(), InstL1_1, runnable() ;
StaticMethodCallWithEvaluatedArguments_ClosureAddition:
--RC: All the arguments of the static method call have been evaluated. So
--RC: the static method declaration and the corresponding closure are
--RC: retrieved.
--
--CS: MyClass.myMethod(345, 57, false);
--
--ESC: Method call expression
evaluateArgument(
ObjL, ClVarL, Env, OThId, ObjId, Mode |- ArgL => ObjL, ClVarL, Env, ArgL, insts[] )
& convertCompArgumentsToValues( ArgL -> ValueL )
&
getStaticMethodClosure(
ObjL, OThId |- MethName, ClName, ValueL -> Clr )
--------------------------------
ObjL, ClVarL, Env, OThId, ObjId, Mode |-
staticMethodCall2(ClName, MethName, ArgL) -> ObjL, ClVarL, Env, empty(), insts[Clr], runnable() ;
end evaluateExpression;
set addReturnVariableInLocalVariableList is
--SC: Adds the 7RETURN variable (used to set the return value of a method
--SC: call) to the most recent local variable pair list if it is not present
--SC: in this latter list. If it is already present (placed on the top of
--SC: this list), nothing is done.
--
--JC: Local variables
--JC: -> Local variable list with the 7RETURN variable
judgement (Locs -> Locs);
--iJC: Pair list
--iJC: -> Pair list with the 7RETURN pair.
judgement (Pairs => Pairs);
TakesTheOnlyFirstPairListInTheLocalVariableList:
--RC: The 7RETURN variable needs to be added in the most recent local
--RC: variable pair list. So only the first pair list is concerned about
--RC: this addition.
(PairL1 => PairL1_1)
--------------------------------
(locs[PairL1.LocVarL] -> locs[PairL1_1.LocVarL]) ;
EmptyPairList_7RETURNAddition:
(pairs[] => pairs[pair(identifier "7RETURN", empty())]) ;
RETURNAlreadyPresent_NoAddition:
(pairs[pair(identifier "7RETURN", Value).PairL] => pairs[pair(identifier "7RETURN", Value).PairL]) ;
RETURNAbsent_7RETURNAddition:
--RC: The first pair is checked to know if it is useful to add the 7RETURN
--RC: pair at the top of the local variable first pair list.
--RC: (The 7RETURN variable pair can only be the first pair of the list)
appendtree( pairs[pair(identifier "7RETURN", empty())], pairs[pair(identifier X, Value).PairL1], PairL1_1 )
--------------------------------
(pairs[pair(identifier X, Value).PairL1] => PairL1_1) ;
provided diff( identifier X, identifier "7RETURN" );
end addReturnVariableInLocalVariableList;
set getConstructorClosure is
--SC: Retrieves the instruction list and the environment corresponding to the
--SC: constructor declaraction. If there is neither a super() nor a this()
--SC: explicit invocation on top of the instruction list, a super()
--SC: invocation is added on its top.
--
--JC: Objects, Class variables, Current executing thread reference
--JC: |- Constructor name (also the class name),
--JC: Created object reference, Constructor parameter values
--JC: -> Closure corresponding to the given constructor call (the new created
--JC: object reference, constructor name, environment for the execution,
--JC: instruction list).
judgement
Objects, ClassVariablesL, ObjectId |- Identifier, ObjectId, Vals -> Clr;
--iJC: Arguments values, Current object reference
--iJC: |- Constructor declaration
--iJC: -> Closure
judgement Vals, ObjectId |- java -> Clr;
EntryRule_NonAPIConstructorCall:
getFieldDeclaration(
ObjL, ClName, ValueL, true() |- ClName -> ConstDec, _, true() ) &
ValueL, ObjId |- ConstDec -> Clr
--------------------------------
ObjL, _, _ |- ClName, ObjId, ValueL -> Clr ;
ExplicitThisOrSuperInvocationInTheConstructorDeclaration:
--RC: Retrieves the instruction list and the environment corresponding to
--RC: the constructor declaraction (in this case, there is already a
--RC: super() or this() explicit invocation).
getInstructionsAndLocalVariables(
insts[], locs[pairs[]] |- BlockElemL => InstL, LocVarL ) &
makeBindedParamList( ValueL |- ParamL -> BindParamL )
--------------------------------
ValueL, ObjId |-
constructorDeclaration(_, constructor(ClName, ParamL), _, constructorBody(SuperOrThis, BlockElemL)) ->
clr(ObjId, identifier "none", ClName, env(BindParamL, LocVarL), insts[SuperOrThis.InstL]) ;
NonExplicitThisOrSuperInvocationInTheConstructorDeclaration:
--RC: As there is no this() or super() explicit invocation on the top of
--RC: the constructor declaration instruction list, a super() invocation
--RC: must be added to the corresponding closure instruction list.
getInstructionsAndLocalVariables(
insts[], locs[pairs[]] |- Block => InstL, LocVarL ) &
makeBindedParamList( ValueL |- ParamL -> BindParamL )
--------------------------------
ValueL, ObjId |-
constructorDeclaration(_, constructor(ClName, ParamL), _, Block) ->
clr(ObjId, identifier "none", ClName, env(BindParamL, LocVarL), insts[superInvocation(arguments[]).InstL]) ;
APIConstructorCallWithoutArgument:
APIMethodOrConstructorCall(
ObjL1, ClVarL1, OThId, ObjId |- ClName, ValueL -> _, _, insts[Clr], _ )
--------------------------------
ObjL1, ClVarL1, OThId |- ClName, ObjId, ValueL -> Clr ;
end getConstructorClosure;
set getMethodClosure is
--SC: Gets the closure corresponding to a method call.
--
--JC: Objects, Class variables
--JC: |- Method name for which the closure is wanted, Object (on which the
--JC: method is called) reference, method parameter values
--JC: -> Closure for the given method call.
judgement Objects |- Identifier, Ref, Vals -> Clr;
getObjectType( ObjId |- ObjL -> ClName ) &
getFieldDeclaration(
ObjL, ClName, ValueL, false() |- MethName -> MethDec, _, true() ) &
makeClosure(
ClName, ValueL, ObjId |- MethDec -> Clr )
--------------------------------
ObjL |- MethName, ObjId, ValueL -> Clr ;
end getMethodClosure;
set getStaticMethodClosure is
--SC: Gets the closure corresponding to a static method call.
--
--JC: Objects, Class variables, current executing thread reference
--JC: |- Static method name for which the closure is wanted, Class name that
--JC: ccntains the given static method, Method parameter values
--JC: -> Closure for the given static method call.
judgement Objects, ObjectId |- Identifier, Identifier, Vals -> Clr;
getFieldDeclaration(
ObjL, ClName, ValueL, false() |- MethName -> MethDec, _, true() ) &
makeClosure(
ClName, ValueL, OThId |- MethDec -> Clr )
--------------------------------
ObjL, OThId |- MethName, ClName, ValueL -> Clr ;
end getStaticMethodClosure;
set assign is
--SC: Assign a value to an identifier. Firstly the variable is sought into
--SC: the parameter list, then into the local variable list and finally into
--SC: the object attributes or in the class variable list associated with the
--SC: object type.
--
--JC: Objects, Class variables, Environment, Current object reference
--JC: |- Identifier of the sought variable, Value to assign
--JC: -> Updated object list, Updated class variables, Updated environment;
--JC: (only one of these three elements is modified)
judgement
Objects, ClassVariablesL, Env, ObjectId |- Identifier, Val -> Objects, ClassVariablesL, Env;
ParameterAssignment:
setVariableIntoAPairList(
Ident, Value |- ParamL1 -> ParamL1_1, true() )
--------------------------------
ObjL, ClVarL, env(ParamL1, LocVarL), _ |-
Ident, Value -> ObjL, ClVarL, env(ParamL1_1, LocVarL) ;
LocalVariableAssignment:
setVariableIntoAPairList(
Ident, Value |- ParamL -> _, false() ) &
setLocalVariable(
Ident, Value |- LocVarL1 -> LocVarL1_1, true() )
--------------------------------
ObjL, ClVarL, env(ParamL, LocVarL1), _ |-
Ident, Value -> ObjL, ClVarL, env(ParamL, LocVarL1_1) ;
AttributeAssignment:
setVariableIntoAPairList(
Ident, Value |- ParamL -> _, false() ) &
setLocalVariable( Ident, Value |- LocVarL -> _, false() )
&
setAttribute( Ident, Value, ObjId |- ObjL1 -> ObjL1_1, true() )
--------------------------------
ObjL1, ClVarL, env(ParamL, LocVarL), ObjId |-
Ident, Value -> ObjL1_1, ClVarL, env(ParamL, LocVarL) ;
ClassVariableAssignment:
setVariableIntoAPairList(
Ident, Value |- ParamL -> _, false() ) &
setLocalVariable( Ident, Value |- LocVarL -> _, false() )
&
setAttribute( Ident, Value, ObjId |- ObjL -> _, false() )
&
setClassVariable(
ObjL, Ident, Value, ObjId |- ClVarL1 => ClVarL1_1 )
--------------------------------
ObjL, ClVarL1, env(ParamL, LocVarL), ObjId |-
Ident, Value -> ObjL, ClVarL1_1, env(ParamL, LocVarL) ;
end assign;
set setVariableIntoAPairList is
--SC: Assigns a value to a variable into a pair list.
--
--JC: Sought variable, Value to assign to this latter variable
--JC: |- Pair list
--JC: -> Updated pair list, true or false depending on the result of the
--JC: search of the variable into the list;
judgement Identifier, Val |- Pairs -> Pairs, Bool;
VariableFound_Assignment:
Ident, Value |- pairs[pair(Ident, _).PairL] -> pairs[pair(Ident, Value).PairL], true() ;
EmptyList_NoAssignment:
_, _ |- pairs[] -> pairs[], false() ;
RecursiveSearchIntoTheList:
Ident1, Value1 |- PairL1 -> PairL1_1, TF
--------------------------------
Ident1, Value1 |-
pairs[pair(Ident2, Value2).PairL1] -> pairs[pair(Ident2, Value2).PairL1_1], TF ;
provided diff( Ident2, Ident1 );
end setVariableIntoAPairList;
set setLocalVariable is
--SC: Assigns a value to a variable into the local variable list.
--
--JC: Sought local variable, Value to assign to this latter variable
--JC: |- Local variable list
--JC: -> Updated local variable list, true or false depending on the result
--JC: of the search of the variable into the list
judgement Identifier, Val |- Locs -> Locs, Bool;
EmptyList_NoAssignment:
_, _ |- locs[] -> locs[], false() ;
VariableFoundIntoTheFirstPairList_Assignment:
setVariableIntoAPairList(
Ident, Value |- PairL1 -> PairL1_1, true() )
--------------------------------
Ident, Value |- locs[PairL1.LocVarL] -> locs[PairL1_1.LocVarL], true() ;
RecursiveSearchIntoTheLocalVariableList:
setVariableIntoAPairList(
Ident, Value |- PairL -> _, false() ) &
Ident, Value |- LocVarL1 -> LocVarL1_1, TF
--------------------------------
Ident, Value |- locs[PairL.LocVarL1] -> locs[PairL.LocVarL1_1], TF ;
end setLocalVariable;
set setAttributeOrStaticVariable is
--SC: Assigns a value to an object attribute or a static variable.
--
--JC: Object, Class variables, Current object reference
--JC: |- Sought variable, Value to assign to this variable
--JC: -> Updated object list, Updated class variable list
--JC: (only one of these two lists is really updated).
judgement
Objects, ClassVariablesL, ObjectId |- Identifier, Val -> Objects, ClassVariablesL;
AttributeAssignment:
setAttribute( Ident, Value, ObjId |- ObjL1 -> ObjL1_1, true() )
--------------------------------
ObjL1, ClVarL, ObjId |- Ident, Value -> ObjL1_1, ClVarL ;
ClassVariableAssignment:
setAttribute( Ident, Value, ObjId |- ObjL -> _, false() )
&
setClassVariable(
ObjL, Ident, Value, ObjId |- ClVarL1 => ClVarL1_1 )
--------------------------------
ObjL, ClVarL1, ObjId |- Ident, Value -> ObjL, ClVarL1_1 ;
end setAttributeOrStaticVariable;
set setAttribute is
--SC: Assigns a value to an attribute.
--
--JC: Sought Variable, Value to assign to this latter variable
--JC: Current object reference
--JC: |- Object list
--JC: -> Updated object list (if the variable was found, the same if not ),
--JC: true or false depending on the result of the search of the variable
--JC: into the list;
judgement Identifier, Val, ObjectId |- Objects -> Objects, Bool;
GoodObject_AssignTheValueToTheAttributeIfFound:
setVariableIntoAPairList(
Ident, Value |- PairL1 -> PairL1_1, TF )
--------------------------------
Ident, Value, ObjId |-
objects[object(ObjId, Type, PairL1, Lock, WaitSet, Act).ObjL] ->
objects[object(ObjId, Type, PairL1_1, Lock, WaitSet, Act).ObjL], TF ;
RecursiveRule_NotTheGoodObject:
Ident, Value, ObjId1 |- ObjL1 -> ObjL1_1, TF
--------------------------------
Ident, Value, ObjId1 |-
objects[object(ObjId2, Type, PairL, Lock, WaitSet, Act).ObjL1] ->
objects[object(ObjId2, Type, PairL, Lock, WaitSet, Act).ObjL1_1], TF ;
provided diff( ObjId2, ObjId1 );
end setAttribute;
set setClassVariable is
--SC: Assigns the given value to its class variable.
--
--JC1: Class name of the class variable, Variable name,
--JC1: Value to assign to this latter variable
--JC1: |- Class variables
--JC1: -> Updated class variable list
judgement
Identifier, Identifier, Val |- ClassVariablesL -> ClassVariablesL;
--JC2: Objects, Sought variable, Value to assign to this latter variable,
--JC2: Current object reference (will give the class name)
--JC2: |- Class variable list
--JC2: => Updated class variable list
judgement
Objects, Identifier, Val, ObjectId |- ClassVariablesL => ClassVariablesL;
AssignValueToTheGivenClassVariable:
setVariableIntoAPairList(
Ident, Value |- PairL1 -> PairL1_1, true() )
--------------------------------
ClName, Ident, Value |-
classVariablesL[classVariables(ClName, PairL1).ClVarL] -> classVariablesL[classVariables(ClName, PairL1_1).ClVarL] ;
LookForTheRightClassBeforeTheAssignment:
ClName1, Ident, Value |- ClVarL1 -> ClVarL1_1
--------------------------------
ClName1, Ident, Value |-
classVariablesL[classVariables(ClName2, PairL).ClVarL1] ->
classVariablesL[classVariables(ClName2, PairL).ClVarL1_1] ;
provided diff( ClName1, ClName2 );
GetClassTypeBeforeTheAssignment:
getObjectType( ObjId |- ObjL -> ClName ) &
ClName, Ident, Value |- ClVarL1 -> ClVarL1_1
--------------------------------
ObjL, Ident, Value, ObjId |- ClVarL1 => ClVarL1_1 ;
end setClassVariable;
set evaluateArgument is
--SC: Evaluates an argument list, making one step of evaluation of one
--SC: argument at each use.
--
--JC1: Objects, Class variables, environment of the current method
--JC1: Current executing thread reference, Current object reference
--JC1: Mode of execution of the method : static or not
--JC1: |- Argument list
--JC1: -> Updated objects, Updated class variables, Updated environment,
--JC1: Updated complex argument list, instructions to execute at the next
--JC1: execution step of the current thread
judgement
Objects, ClassVariablesL, Env, ObjectId, ObjectId, Identifier |-
ArgumentList -> Objects, ClassVariablesL, Env, SemArguments, Insts;
--JC2: Objects, Class variables, environment of the current method
--JC2: Current executing thread reference, Current object reference
--JC2: Mode of execution of the method : static or not
--JC2: |- Complex argument list
--JC2: => Updated objects, Updated class variables, Updated environment,
--JC2: Updated complex argument list, instructions to execute at the next
--JC2: execution step of the current thread
judgement
Objects, ClassVariablesL, Env, ObjectId, ObjectId, Identifier |-
SemArguments => Objects, ClassVariablesL, Env, SemArguments, Insts;
EmptyArgumentList:
ObjL, ClVarL, Env, _, _, _ |- arguments[] -> ObjL, ClVarL, Env, semArguments[], insts[] ;
ConvertArgumentsToCompArgumentsAndFirstStepCompArgumentEvaluation:
convertArgumentsToCompArguments( ArgL -> CompArgL1 )
&
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
CompArgL1 => ObjL1_1, CLVarL1_1, Env1_1, CompArgL1_1, InstL
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
ArgL -> ObjL1_1, CLVarL1_1, Env1_1, CompArgL1_1, InstL ;
EmptyCompArgumentList_EvaluationEnd:
ObjL, ClVarL, Env, _, _, _ |- semArguments[] => ObjL, ClVarL, Env, semArguments[], insts[] ;
ValueAsFirstCompArgument_TailCompArgumentListEvaluation:
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
ExprL1 => ObjL1_1, ClVarL1_1, Env1_1, ExprL1_1, InstL &
appendtree( semArguments[TVValue], ExprL1_1, ExprL2 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
semArguments[TVValue.ExprL1] => ObjL1_1, ClVarL1_1, Env1_1, ExprL2, InstL ; -- !!! Why is the returned ThStatus thrown away?
ExpressionEvaluation:
evaluateExpression(
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
Expr1 -> ObjL1_1, ClVarL1_1, Env1_1, Expr1_1, InstL, _ )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
semArguments[Expr1] => ObjL1_1, ClVarL1_1, Env1_1, semArguments[Expr1_1], InstL ;
ExpressionAsFirstCompArgument_ExpressionEvaluation:
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
semArguments[Expr1] => ObjL1_1, ClVarL1_1, Env1_1, ExprL2, InstL &
appendtree( ExprL2, ExprL1, ExprL3 )
--------------------------------
ObjL1, ClVarL1, Env1, OThId, ObjId, Mode |-
semArguments[Expr1.ExprL1] => ObjL1_1, ClVarL1_1, Env1_1, ExprL3, InstL ;
provided diff( ExprL1, semArguments[] );
end evaluateArgument;
set convertArgumentsToCompArguments is
--SC: Converts a list of arguments into a comp argument list (useful for the
--SC: representation of the object references during small-step evaluation).
--SC: No argument evaluation is done during this conversion.
--
--JC: Arguments -> Complex arguments
judgement (ArgumentList -> SemArguments);
EmptyArgumentList_ConversionEnd:
(arguments[] -> semArguments[]) ;
RecursiveConversionRule:
(ArgL -> CompArgL)
--------------------------------
(arguments[Arg.ArgL] -> semArguments[Arg.CompArgL]) ;
end convertArgumentsToCompArguments;
set convertCompArgumentsToValues is
--SC: Converts a comp argument list into a value list.
--
--JC: Complex arguments -> Values
judgement (SemArguments -> Vals);
EmptyCompArgumentList: (semArguments[] -> vals[]) ;
RecursiveConversionRule:
(CompArgL -> ValueL)
--------------------------------
(semArguments[Value.CompArgL] -> vals[Value.ValueL]) ;
end convertCompArgumentsToValues;
set convertArrayInitializerToSemArgument is
judgement (Type, ArrayInitializer -> SemArgument);
convertVariableInitializersToSemArguments(
Type, ArrayInit -> Exprs )
--------------------------------
(arrayof(Type), ArrayInit -> semNewInitializedArray(arrayof(Type), Exprs)) ;
end convertArrayInitializerToSemArgument;
set convertVariableInitializersToSemArguments is
judgement (Type, ArrayInitializer -> SemArguments);
(_, arrayInitializer[] -> semArguments[]) ;
convertVariableInitializersToSemArguments(
Type, VarInits -> Exprs )
--------------------------------
(Type, arrayInitializer[VarInit.VarInits] -> semArguments[VarInit.Exprs]) ;
provided not_eq( VarInit, arrayInitializer[_] );
--RC: Recursive case, the variable initializer is an array initializer.
convertArrayInitializerToSemArgument( Type, TVArrayInit -> Expr )
&
convertVariableInitializersToSemArguments(
Type, VarInits -> Exprs )
--------------------------------
(Type, arrayInitializer[TVArrayInit.VarInits] -> semArguments[Expr.Exprs]) ;
end convertVariableInitializersToSemArguments;
set makeNewArrayExprList is
--SC: Builds semantic argument list of n expressions of the kind
--SC: semNewArray(Type, Sizes).
judgement (integer, Type, SemArguments -> SemArguments);
(0, _, _ -> semArguments[]) ; --RC: recursive case.
sub( n, 1, nminus1 ) & (nminus1, Type, Sizes -> Exprs)
--------------------------------
(n, Type, Sizes -> semArguments[semNewArray(Type, Sizes).Exprs]) ;
provided sup( n, 0 );
end makeNewArrayExprList;
set convertDimsToSemArgs is
--SC: Extract the expressions from a dimension list and make a semantic
--SC: argument list out of them.
judgement (Dims -> SemArguments);
(dims[] -> semArguments[]) ; --RC: Recursive case.
(Sizes -> Sizes_1)
--------------------------------
(dims[Size.Sizes] -> semArguments[Size.Sizes_1]) ;
end convertDimsToSemArgs;
set computeArrayType is
--SC: Computes the type of an array given the element type and a dimension
--SC: list.
judgement (Type, Dims -> Type);
(Type, dims[] -> Type) ; --RC: Recursive case.
(arrayof(Type), Dims -> ArrayType)
--------------------------------
(Type, dims[_.Dims] -> ArrayType) ;
end computeArrayType;
set isValue is
--SC: Checks if a SemExpression is a Value.
judgement (SemExpression -> Bool);
(true() -> true()) ;
(false() -> true()) ; --RC: Integers are values.
(integer _ -> true()) ; --RC: Floating point numbers are values.
(floating _ -> true()) ; --RC: Characters are values.
(character _ -> true()) ; --RC: Strings are values.
(string _ -> true()) ; --RC: References are values.
(objectId(_, _) -> true()) ;
(null() -> true()) ; --RC: Finally, empty and exceptions are also values.
--RC: (But exceptions probably should not be.)
(empty() -> true()) ;
(except(_, _, _) -> true()) ; --RC: Everything else is not a value.
(Expr -> false()) ;
provided
not_eq( Expr, true() ) & not_eq( Expr, false() ) & not_eq( Expr, integer _ )
& not_eq( Expr, floating _ ) & not_eq( Expr, character _ )
& not_eq( Expr, string _ ) & not_eq( Expr, objectId(_, _) )
& not_eq( Expr, null() ) & not_eq( Expr, empty() ) &
not_eq( Expr, except(_, _, _) );
end isValue;
set allAreValues is
--SC: Checks whether all arguments in a semantic argument list have been
--SC: evaluated to values or not.
judgement (SemArguments -> Bool);
(semArguments[] -> true()) ; --RC: Recursive rule, non value found:
isValue( Arg1 -> false() )
--------------------------------
(semArguments[Arg1.Args] -> false()) ; --RC: Recursive rule, only values so far:
isValue( Arg1 -> true() ) & (Args -> TF)
--------------------------------
(semArguments[Arg1.Args] -> TF) ;
end allAreValues;
set isCompoundAssignOp is
--SC: Checks whether an AssignOperator is a compund assignment operator
--SC: (+=, -=, etc.) or not.
judgement (AssignOperator -> Bool);
(plusAssignment() -> true()) ;
(minusAssignment() -> true()) ;
(timesAssignment() -> true()) ;
(divAssignment() -> true()) ;
(modAssignment() -> true()) ;
(xorAssignment() -> true()) ;
(andAssignment() -> true()) ;
(iorAssignment() -> true()) ;
(leftShiftAssignment() -> true()) ;
(rightShiftAssignment() -> true()) ;
(unsignedRightShiftAssignment() -> true()) ;
(AOp -> false()) ;
provided
not_eq( AOp, plusAssignment() ) & not_eq( AOp, minusAssignment() ) &
not_eq( AOp, timesAssignment() ) & not_eq( AOp, divAssignment() ) &
not_eq( AOp, modAssignment() ) & not_eq( AOp, xorAssignment() ) &
not_eq( AOp, andAssignment() ) & not_eq( AOp, iorAssignment() ) &
not_eq( AOp, leftShiftAssignment() ) & not_eq( AOp, rightShiftAssignment() ) &
not_eq( AOp, unsignedRightShiftAssignment() );
end isCompoundAssignOp;
set getOpFromCompundAssignOp is
--SC: Gets the binary numeric operator (+, -, etc.) from a compound
--SC: assignment operator (+=, -=, etc.).
judgement (AssignOperator -> BinaryOperator);
(plusAssignment() -> plus()) ;
(minusAssignment() -> minus()) ;
(timesAssignment() -> times()) ;
(divAssignment() -> div()) ;
(modAssignment() -> mod()) ;
(xorAssignment() -> xor()) ;
(andAssignment() -> and()) ;
(iorAssignment() -> ior()) ;
(leftShiftAssignment() -> leftShift()) ;
(rightShiftAssignment() -> rightShift()) ;
(unsignedRightShiftAssignment() -> unsignedRightShift()) ;
end getOpFromCompundAssignOp;
end java_expr_evaluation