-- $Id: java_array_support.ty,v 1.3 99/08/10 10:43:31 mrusso Exp $
-- /***************************************************************************/
-- /* Copyright (C) 1997-1999 INRIA Sophia-Antipolis (Projet OASIS) */
-- /* BP 93 F-06902 Sophia Antipolis Cedex */
-- /* (+33) 4 92 38 75 62 http://www-sop.inria.fr/oasis/javacard */
-- /* All rights reserved */
-- /***************************************************************************/
-- Sets for arrays:
-- # Create an array with or without initial values
-- # Get elements from an array
-- # Set values into an array
-- # Compare values of two arrays
-- /***************************************************************************/
-- /* Created by Carine Courbis & Henrik Nilsson 20 April 1999 */
-- /***************************************************************************/
program java_array_support is
use java;
use PSP;
import
inf ( _, _ ) , infeq ( _, _ ) , sub ( _, _, _ ) ,
sup ( _, _ ) , supeq ( _, _ )
from arith;
import
appendtree ( _, _, _ ) , diff ( _, _ ) , equal ( _, _ ) , not_eq ( _, _ ) , plus ( _, _, _ ) , succ ( _, _ ) , writeln ( _ )
from prolog() ;
import
or ( |- Bool, Bool -> Bool )
from java_utility_functions;
import
ENVaddCreatedSimpleObjectToStatusList ( ObjectId ) ,
ENVsendNewObject ( Object )
from java_environment;
import
getInitialValueForAGivenType ( Type -> Val ) ,
isMyAncestor ( Type |- Type -> Bool )
from java_inheritance;
import
createExceptionObject (
Objects, ObjectId |- Identifier, ExceptText -> ObjectId, Objects, Insts ) ,
createExceptionObject (
Objects, ObjectId |- Identifier, ExceptText => ObjectId, Object, Insts ) ,
generateANumberForTheNewObject (
|- Objects -> ObjectNumber ) ,
getObjectType ( ObjectId |- Objects -> Type ) ,
getObject ( ObjectId |- Objects -> Object )
from java_object_list;
set newArray is
-- Public Set
--SC: Create a new array object and add it to the object list
--SC: All its elements are initialized with the default value of its type
--SC: If the array size is negative, a NegativeArraySizeException
--SC: object is created and added at the end of the object list
--SC: The OutOfMemoryError is not treated for the moment
--
--JC: array type, array length, current thread id (exception) |- objects
--JC: -> updated object list (the new array or exception object has been
--JC: added at the end of the object list), ID of the new array or exception,
--JC: next instructions to execute in case of exception
judgement
Type, integer, ObjectId |- Objects -> Objects, ObjectId, Insts;
--JC: ^, ^, new generated array id, current thread id (exception) |- ^
--JC: -> ^, ^, ^
judgement
Type, integer, ObjectNumber, ObjectId |- Objects -> Objects, ObjectId, Insts;
GenerateArrayObjectIdentifier_ThenTryToCreateTheArray:
generateANumberForTheNewObject(
|- ObjL1 -> ObjNb ) &
ArrayType, Len, ObjNb, OThId |- ObjL1 -> ObjL1_1, objectId(false(), ObjNb), InstL
--------------------------------
ArrayType, Len, OThId |- ObjL1 -> ObjL1_1, objectId(false(), ObjNb), InstL ;
InitializeElements_CreateArrayObject:
getInitialValueForAGivenType(
ElementType -> InitialVal ) &
initializeElements(
0, Len, InitialVal |- vals[] -> ElemL ) &
newArrayWithValuesAndLength(
arrayof(ElementType), Len, ElemL, ObjNb |- ObjL1 -> ObjL1_1, ObjId )
--------------------------------
arrayof(ElementType), Len, ObjNb, _ |- ObjL1 -> ObjL1_1, ObjId, insts[] ;
provided supeq( Len, 0 );
FoundTheRightObject_NegativeIndexOrIndexGreaterOrEqualToArrayLength_Exception:
createExceptionObject(
ObjL1, OThId |-
identifier "NegativeArraySizeException", exceptText "The array size is negative" -> ExObjId, ObjL1_1, InstL )
--------------------------------
_, Len, _, OThId |- ObjL1 -> ObjL1_1, ExObjId, InstL ;
provided inf( Len, 0 );
set initializeElements is
--SC: Create the array elements and initialize them with the given value
--SC: (normally the default value for the array element type)
--
--JC: offset (0 at the beginning), number of elements to create,
--JC: value used to initialize the elements |- current element list (empty
--JC: list at the beginning) -> initialized element list
judgement integer, integer, Val |- Vals -> Vals;
NoMoreElementToAdd:
Len, Len, _ |- ElemL -> ElemL ;
MoreElementToAdd:
succ( CurOff, NextOff ) &
NextOff, Len, InitVal |- vals[InitVal.ElemL] -> ElemL1_1
--------------------------------
CurOff, Len, InitVal |- ElemL -> ElemL1_1 ;
provided inf( CurOff, Len );
end initializeElements ;
end newArray;
set newArrayWithValues is
--SC: Create a new array object and add it to the object list
--SC: The OutOfMemoryError is not treated for the moment
--
--JC: array type, array initialisation values |- objets
--JC: -> updated object list (the new array has been added to the objet list)
--JC: ID of the new array
judgement Type, Vals |- Objects -> Objects, ObjectId;
FoundArrayLength_CreateArrayObject:
getArrayLength( 0 |- ElemL -> Len ) &
newArrayWithValuesAndLength(
ArrayType, Len, ElemL |- ObjL1 -> ObjL1_1, ObjId )
--------------------------------
ArrayType, ElemL |- ObjL1 -> ObjL1_1, ObjId ;
set getArrayLength is
--JC: Offset (0 at the beginning) |- element list -> array length
judgement integer |- Vals -> integer;
NoMoreElem: NbElem |- vals[] -> NbElem ;
RecursiveRule_MoreElem:
succ( CurOff, NextOff ) & NextOff |- ElemL -> NbElem
--------------------------------
CurOff |- vals[_.ElemL] -> NbElem ;
end getArrayLength ;
end newArrayWithValues;
set newArrayWithValuesAndLength is
--Private Set
--JC: array type, array length, array values |- objects
--JC: -> updated object list (the new array was appended to the objet list)
--JC: id of the new array
judgement Type, integer, Vals |- Objects -> Objects, ObjectId;
--JC: ^, ^, ^, generated array id |- ^ -> ^, ^
judgement
Type, integer, Vals, ObjectNumber |- Objects -> Objects, ObjectId;
CreateNewObject_GetObjId_AddItAtTheEndOfTheList:
generateANumberForTheNewObject(
|- ObjL1 -> ObjNb ) &
ArrayType, Len, ElemL, ObjNb |- ObjL1 -> ObjL1_1, objectId(false(), ObjNb)
--------------------------------
ArrayType, Len, ElemL |- ObjL1 -> ObjL1_1, objectId(false(), ObjNb) ;
CreateNewObjectWithObjId_AddItAtTheEndOfTheList:
appendtree(
ObjL1,
objects[
object(
objectId(false(), ObjNb), ArrayType, pairs[pair(identifier "length", integer Len), pair(identifier "7ARRAY", ElemL)], unlocked(),
waits[], empty())], ObjL1_1 )
--------------------------------
ArrayType, Len, ElemL, ObjNb |- ObjL1 -> ObjL1_1, objectId(false(), ObjNb) ;
do
ENVsendNewObject(
object(
objectId(false(), ObjNb), ArrayType, pairs[pair(identifier "length", integer Len), pair(identifier "7ARRAY", ElemL)],
unlocked(), waits[], empty()) ) &
ENVaddCreatedSimpleObjectToStatusList(
objectId(false(), ObjNb) );
end newArrayWithValuesAndLength;
set getArrayElement is
--SC: Get the indexth element of the array
--SC: If the index is negative or greater than or equal to the array
--SC: length, an exception object (ArrayIndexOutOfBoundsException)
--SC: is created
--SC: If the array is a null pointer, an NullPointerException is created
--SC: Henrik: But should not ba a null pointer since this has to be
--SC: checked earlier. Thus this check is redundant, and the type could
--SC: be ObjectId rather than Ref.
--
--JC: array Id, index, current executing thread id (exception)
--JC: |- object list -> Value of the indexth element,
--JC: object list (updated only if an exception has occured)
--JC: next instructions to execute in case of exception
judgement Ref, integer, ObjectId |- Objects -> Val, Objects, Insts;
--JC: index , object list(exception), ^
--JC: |- array object => ^, ^, ^
judgement
integer, Objects, ObjectId |- Object => Val, Objects, Insts;
InitGetElement:
getArrayElements(
ArrayId, Index, 1, OThId |- ObjL1 -> Values, ObjL1_1, InstL ) &
extractValue( |- Values -> ValElem )
--------------------------------
ArrayId, Index, OThId |- ObjL1 -> ValElem, ObjL1_1, InstL ;
InitGetElement:
getArrayElements(
Index, 1, ObjL1, OThId |- Array => Values, ObjL1_1, InstL ) &
extractValue( |- Values -> ValElem )
--------------------------------
Index, ObjL1, OThId |- Array => ValElem, ObjL1_1, InstL ;
set extractValue is
judgement |- Vals -> Val;
noValue: |- vals[] -> empty() ;
OneValue: |- vals[ValElem] -> ValElem ;
end extractValue ;
end getArrayElement;
set getArrayElements is
--SC: Get a consecutive list of elements of an array
--SC: If the index is negative or greater than or equal to the array
--SC: length, an exception object (ArrayIndexOutOfBoundsException)
--SC: is created as well as when the length of the required information
--SC: exceeds the bounds of the array
--SC: If the array is a null pointer, a NullPointerException is created
--
--JC: array Id, index, number of required elements, current executing thread
--JC: (only useful in case of exception) |- objects -> list of elements,
--JC: object list (updated only if an exception has occured)
--JC: next instructions to execute in case of exception
judgement
Ref, integer, integer, ObjectId |- Objects -> Vals, Objects, Insts;
--JC: Index, number of required elements, object list (useful to generate
--JC: the exception id), current thread id (exception) |- Array -> ^, ^, ^
judgement
integer, integer, Objects, ObjectId |- Object => Vals, Objects, Insts;
--iJC: true if the request is out of bounds (negative index, negative length,
--iJC: or index+length > array length) false otherwise, ^, ^, ^, ^
--iJC: |- array elements => ^, ^, ^
judgement
Bool, integer, integer, Objects, ObjectId |- Vals => Vals, Objects, Insts;
nullPointer_Exception:
createExceptionObject(
ObjL1, OThId |-
identifier "NullPointerException", exceptText "Use of a pointer with a null value" -> _, ObjL1_1, InstL )
--------------------------------
null(), _, _, OThId |- ObjL1 -> vals[], ObjL1_1, InstL ;
GetArrayObject:
getObject( ArrayId |- ObjL1 -> Array ) &
Index, Length, ObjL1, OThId |- Array => ArrayElems, ObjL1_1, InstL
--------------------------------
ArrayId, Index, Length, OThId |- ObjL1 -> ArrayElems, ObjL1_1, InstL ;
provided diff( ArrayId, null() );
ChecktheArrayBounds:
IsIndexOrLenNegative(
|- Index, Length -> TF1 ) &
IsIndexPlusLengthGreaterThanArrayLength(
ArrayLen |- Index, Length -> TF2 ) &
or( |- TF1, TF2 -> TF3 )
&
TF3, Index, Length, ObjL1, OThId |- ElemL => ArrayElems, ObjL1_1, InstL
--------------------------------
Index, Length, ObjL1, OThId |-
object(_, _, pairs[pair(identifier "length", integer ArrayLen), pair(identifier "7ARRAY", ElemL)], _, _, _) =>
ArrayElems, ObjL1_1, InstL ;
IndexAndLengthLessThanArrayLength_GetTheValues:
getValuesFromArray(
0, Index, Length |- ElemL -> ArrayElems )
--------------------------------
false(), Index, Length, ObjL, _ |- ElemL => ArrayElems, ObjL, insts[] ;
RequestOutOfArrayBounds_Exception:
createExceptionObject(
ObjL1, OThId |-
identifier "ArrayIndexOutOfBoundsException", exceptText "The index is negative or greater/equal to the size of the array"
->
_, ObjL1_1, InstL )
--------------------------------
true(), _, _, ObjL1, OThId |- _ => vals[], ObjL1_1, InstL ;
set getValuesFromArray is
--SC: Get a consecutive list of array elements
--
--JC: current offset (ie 0 at beginning), index, length
--JC: (how many elements are required)|- Array Elements
--JC: |- required array elements
judgement integer, integer, integer |- Vals -> Vals;
--iJC: current offset (ie 0 at beginning), length,
--iJC: temporary array values (vals[] at the beginning)
--iJC: |- Array Elements |- the required array values
judgement integer, integer, Vals |- Vals => Vals;
FillResult_endCase:
Length, Length, BufferValues |- _ => BufferValues ;
FillResult_recurseCase:
succ( CurOff, NextOff ) & appendtree( ResultVals1, vals[ValElem], ResultVals1_1 ) &
NextOff, Length, ResultVals1_1 |- ElemL => BufferValues
--------------------------------
CurOff, Length, ResultVals1 |- vals[ValElem.ElemL] => BufferValues ;
provided not_eq( CurOff, Length );
FoundElem:
0, Length, vals[] |- ArrayValues => BufferValues
--------------------------------
Index, Index, Length |- ArrayValues -> BufferValues ;
GoToTheOffsetElement_recurseCase:
succ( CurOff, NextOff ) &
NextOff, Index, Length |- ElemL -> BufferValues
--------------------------------
CurOff, Index, Length |- vals[_.ElemL] -> BufferValues ;
provided diff( CurOff, Index );
end getValuesFromArray ;
set IsIndexPlusLengthGreaterThanArrayLength is
-- Private Set
--SC: Check if the required information does not exceed the array
--SC: length. Return true if too much information is required, false
--SC: otherwise ie Index + Len <= Array Len return false
--
--JC: Array length |- Index, length of the required information ->
--JC: True if too much information is required ie out of array bounds
--JC: False otherwise
judgement integer |- integer, integer -> Bool;
--iJC: |- Array length, Index+required information length -> true/false
judgement |- integer, integer -> Bool;
FinalPositionSmallerThanOrEqualToArrayLength:
|- ArrayLen, IndexPlusLen -> false() ;
provided supeq( ArrayLen, IndexPlusLen );
FinalPositionLongerThanTheArrayLength:
|- ArrayLen, IndexPlusLen -> true() ;
provided inf( ArrayLen, IndexPlusLen );
ComputeFinalPosition:
plus( Index, Len, IndexPlusLen ) &
|- ArrayLen, IndexPlusLen -> TF
--------------------------------
ArrayLen |- Index, Len -> TF ;
end IsIndexPlusLengthGreaterThanArrayLength ;
set IsIndexOrLenNegative is
-- Private Set
--SC: Check if the given index or length is negative
--SC: Return true or false
--
--JC: |- Index, Len -> True if the index or length is negative
--JC: False otherwise
judgement |- integer, integer -> Bool;
NegativeOffset:
|- Index, _ -> true() ;
provided inf( Index, 0 );
NegativeLength:
|- _, Len -> true() ;
provided inf( Len, 0 );
PositiveOffsetAndLength:
|- Index, Len -> false() ;
provided
supeq( Index, 0 ) & supeq( Len, 0 );
end IsIndexOrLenNegative ;
end getArrayElements;
set setArrayElement is
--SC: Set the given value to the indexth element
--SC: If the index is negative or greater than or equal to the array
--SC: length, an exception object (ArrayIndexOutOfBoundsException)
--SC: is created
--SC: If the type of the given value is not a right type, an exception
--SC: object (ArrayStoreException) is created (No exception object
--SC: is created if the class of the value is a subclass of the array type
--SC: or if both the array type and the value type are primitive types)
--SC: If the array is a null pointer, an NullPointerException is created
--
--JC: array Id, index, value to set, current executing thread id (exception)
--JC: |- objects -> updated object list (the given value has been set
--JC: in the indexth element or an exception has occured if the index
--JC: is negative or greater than or equal to the array length),
--JC: next instructions to execute in case of exception
judgement Ref, integer, Val, ObjectId |- Objects -> Objects, Insts;
InitSetElement:
setArrayElements(
ArrayId, Index, 1, "Set", vals[ValElem], OThId |- ObjL1 -> ObjL1_1, InstL, _ )
--------------------------------
ArrayId, Index, ValElem, OThId |- ObjL1 -> ObjL1_1, InstL ;
end setArrayElement;
set setArrayElements is
--SC: This set is useful for 2 operations: set elements in an array
--SC: and fill in many elements of an array with only one value
--SC: 1] Set the given values from the indexth element to the
--SC: length -1 th element
--SC: 2] Fill with the given value from the indexth element to
--SC: the length -1 th element
--SC:
--SC: Exceptions:
--SC: If the index is negative or greater than or equal to the array
--SC: length, an exception object (ArrayIndexOutOfBoundsException)
--SC: is created
--SC: If the index+length > array length, an ArrayIndexOutOfBoundsException
--SC: is created
--SC: If the array id is null(), an NullPointerException is created
--SC: If the type of the given value is not a right type, an exception
--SC: object (ArrayStoreException) is created (No exception object
--SC: is created if the class of the value is a subclass of the array type
--SC: or if both the array type and the value type are primitive types)
--
--JC: array Id, Index, Length, "Set" or "Fill" operation
--JC: Values to set (in case of Fill only one value is in this list)
--JC: current executing thread (exception) |- Object list
--JC: -> updated object list (the given value has been set in the offset-th
--JC: element until the length-one th element or an exception has occured
--JC: if the index is greater than or equal to the array length),
--JC: next instructions to execute in case of exception
--JC: Index+Length (last offset position)
judgement
Ref, integer, integer, string, Vals, ObjectId |- Objects -> Objects, Insts, integer;
--iJC: same that above with the complete object list in the hypothesis
--iJC: (useful in case of exception to generate the id number)
judgement
ObjectId, integer, integer, string, Vals, Objects, ObjectId |-
Objects -> Objects, Insts, integer;
nullArrayId_NullPointerException:
createExceptionObject(
ObjL1, OThId |-
identifier "NullPointerException", exceptText "Use of a pointer with a null value" -> _, ObjL1_1, InstL )
--------------------------------
null(), _, _, _, _, OThId |- ObjL1 -> ObjL1_1, InstL, 0 ;
InitSetElements_NoNullPointer_NoNegativeLenOrIndex:
ArrayId, Index, Len, OpType, ValElems, ObjL1, OThId |- ObjL1 -> ObjL1_1, InstL, LastPos
--------------------------------
ArrayId, Index, Len, OpType, ValElems, OThId |- ObjL1 -> ObjL1_1, InstL, LastPos ;
provided
diff( ArrayId, null() ) & supeq( Index, 0 ) &
supeq( Len, 0 );
NegativeIndex_ArrayIndexOutOfBoundsException:
createExceptionObject(
ObjL1, OThId |-
identifier "ArrayIndexOutOfBoundsException", exceptText "The index is negative or greater/equal to the size of the array"
->
_, ObjL1_1, InstL )
--------------------------------
ArrayId, Index, _, _, _, OThId |- ObjL1 -> ObjL1_1, InstL, 0 ;
provided diff( ArrayId, null() ) & inf( Index, 0 );
NegativeLen_ArrayIndexOutOfBoundsException:
createExceptionObject(
ObjL1, OThId |-
identifier "ArrayIndexOutOfBoundsException", exceptText "The index is negative or greater/equal to the size of the array"
->
_, ObjL1_1, InstL )
--------------------------------
ArrayId, _, Len, _, _, OThId |- ObjL1 -> ObjL1_1, InstL, 0 ;
provided diff( ArrayId, null() ) & inf( Len, 0 );
FoundTheRightObject_RightArrayBounds_SetValues:
plus( Index, Len, ExpLastPos ) & infeq( ExpLastPos, ArrayLen )
&
setValuesToArray(
0, Index, ExpLastPos, ElementType, OpType, ValElems, ObjL1, OThId |-
ElemL1 -> ElemL1_1, LastPos, InstL, ExObjL ) & appendtree( ObjL2, ExObjL, ObjL2_1 )
--------------------------------
ArrayId, Index, Len, OpType, ValElems, ObjL1, OThId |-
objects[
object(ArrayId, arrayof(ElementType), pairs[pair(identifier "length", integer ArrayLen), pair(identifier "7ARRAY", ElemL1)], L, W, A).
ObjL2] ->
objects[
object(
ArrayId, arrayof(ElementType), pairs[pair(identifier "length", integer ArrayLen), pair(identifier "7ARRAY", ElemL1_1)], L, W, A).
ObjL2_1], InstL, LastPos ;
FoundTheRightObject_ExceedArrayBounds_Exception:
plus( Index, Len, ExpLastPos ) & sup( ExpLastPos, ArrayLen )
&
createExceptionObject(
ObjL1, OThId |-
identifier "ArrayIndexOutOfBoundsException", exceptText "The index is negative or greater/equal to the size of the array"
=>
_, ExObj, InstL ) &
appendtree( objects[object(ArrayId, T, pairs[pair(identifier "length", integer ArrayLen), ElemL], L, W, A).ObjL2], objects[ExObj], ObjL2_1
)
--------------------------------
ArrayId, Index, Len, _, _, ObjL1, OThId |-
objects[object(ArrayId, T, pairs[pair(identifier "length", integer ArrayLen), ElemL], L, W, A).ObjL2] ->
ObjL2_1, InstL, 0 ;
RecursiveRule_NotTheRightObject:
ArrayId, Index, Len, OpType, ValElems, ObjL1, OThId |- ObjL2 -> ObjL2_1, InstL, LastPos
--------------------------------
ArrayId, Index, Len, OpType, ValElems, ObjL1, OThId |-
objects[object(ObjId, T, A, L, W, Act).ObjL2] -> objects[object(ObjId, T, A, L, W, Act).ObjL2_1], InstL, LastPos ;
provided diff( ArrayId, ObjId );
set setValuesToArray is
--JC: current offset (0 at beginning), sought index,
--JC: expected last offset, array element type,
--JC: "Fill" or "Set" operation, Values to set (in case of Fill only
--JC: one value is in the list), object list (useful to generate the
--JC: exception id), current executing thread (exception)
--JC: |- array elements -> updated array elements
--JC: instructions (exception), exception object (exception)
judgement
integer, integer, integer, Type, string, Vals, Objects, ObjectId |-
Vals -> Vals, integer, Insts, Objects;
--iJC1: current offset, expected last offset, ^, ^, ^, ^, ^ |- ^
--iJC1: -> ^, ^, ^
judgement
integer, integer, Type, string, Vals, Objects, ObjectId |-
Vals => Vals, integer, Insts, Objects;
--iJC2: True if the value type is a subtype of the array type,
--iJC2: false otherwise (so an exception will be created),
--iJC2: ^, ^, ^, ^, ^, ^ |- ^ -> ^, ^, ^,
judgement
Bool, integer, integer, Type, string, Vals, Objects, ObjectId |-
Vals => Vals, integer, Insts, Objects;
var TVReferenceType: ReferenceType;
var TVPrimitiveType: PrimitiveType;
OnIndex_BeginOfSetValues:
Index, ExpLastPos, ElemType, OpType, ValElems, ObjL, OThId |-
ElemL1 => ElemL1_1, LastPos, InstL, ExObjL
--------------------------------
Index, Index, ExpLastPos, ElemType, OpType, ValElems, ObjL, OThId |-
ElemL1 -> ElemL1_1, LastPos, InstL, ExObjL ;
GoToIndex_Init:
succ( CurOff, NextOff ) &
NextOff, Index, ExpLastPos, ElemType, OpType, ValElems, ObjL, OThId |-
ElemL1 -> ElemL1_1, LastPos, InstL, ExObjL
--------------------------------
CurOff, Index, ExpLastPos, ElemType, OpType, ValElems, ObjL, OThId |-
vals[Elem.ElemL1] -> vals[Elem.ElemL1_1], LastPos, InstL, ExObjL ;
provided diff( CurOff, Index );
ObjectTypes_GetValueType_CheckIfTheValueTypeIsASubType:
getObjectType( objectId(TF1, ObjNb) |- ObjL -> ObjType )
&
isMyAncestor( TVReferenceType |- ObjType -> TF2 )
&
TF2, CurOff, ExpLastPos, TVReferenceType, OpType, vals[objectId(TF1, ObjNb).ElemL1], ObjL, OThId |-
ElemL2 => ElemL2_1, LastPos, InstL, ExObjL
--------------------------------
CurOff, ExpLastPos, TVReferenceType, OpType, vals[objectId(TF1, ObjNb).ElemL1], ObjL, OThId |-
ElemL2 => ElemL2_1, LastPos, InstL, ExObjL ;
provided diff( CurOff, ExpLastPos );
PrimitiveType_ObjectType_ExceptionObjectCreation:
false(), CurOff, _, _, _, _, ObjL, OThId |- ElemL => ElemL, CurOff, InstL, ExObjL
--------------------------------
CurOff, _, TVPrimitiveType, _, vals[objectId(_, _)._], ObjL, OThId |-
ElemL => ElemL, CurOff, InstL, ExObjL ;
ObjectType_PrimitiveType_ExceptionObjectCreation:
false(), CurOff, _, _, _, _, ObjL, OThId |- ElemL => ElemL, CurOff, InstL, ExObjL
--------------------------------
CurOff, _, TVReferenceType, _, vals[ValElem._], ObjL, OThId |-
ElemL => ElemL, CurOff, InstL, ExObjL ;
provided not_eq( ValElem, objectId(_, _) );
PrimitiveTypes_SetValue:
--c: Something must be done to check that we do not assign a float in a int ...
true(), CurOff, ExpLastPos, TVPrimitiveType, OpType, vals[ValElem.ElemL1], ObjL, OThId |-
ElemL2 => ElemL2_1, LastPos, InstL, ExObjL
--------------------------------
CurOff, ExpLastPos, TVPrimitiveType, OpType, vals[ValElem.ElemL1], ObjL, OThId |-
ElemL2 => ElemL2_1, LastPos, InstL, ExObjL ;
provided not_eq( ValElem, objectId(_, _) ) & diff( CurOff, ExpLastPos );
NoMoreElementToFill:
ExpLastPos, ExpLastPos, _, _, _, _, _ |-
ArrayElemL => ArrayElemL, ExpLastPos, insts[], objects[] ;
NoMoreElementToFill:
CurOff, _, _, _, vals[], _, _ |- ArrayElemL => ArrayElemL, CurOff, insts[], objects[] ;
NotASubClass_ExceptionObjectCreation:
createExceptionObject(
ObjL, OThId |-
identifier "ArrayStoreException", exceptText "Try to store a wrong type of object into an array of objects"
=>
_, ExObj, Insts )
--------------------------------
false(), CurOff, _, _, _, _, ObjL, OThId |- ElemL => ElemL, CurOff, Insts, objects[ExObj] ;
SetElement_RightTypes_recurseCase:
succ( CurOff, NextOff ) &
NextOff, ExpLastPos, ElemType, "Set", ElemL1, ObjL, OThId |-
ArrayElemL1 => ArrayElemL1_1, LastPos, Insts, ExObjL
--------------------------------
true(), CurOff, ExpLastPos, ElemType, "Set", vals[ValElem.ElemL1], ObjL, OThId |-
vals[_.ArrayElemL1] => vals[ValElem.ArrayElemL1_1], LastPos, Insts, ExObjL ;
provided diff( CurOff, ExpLastPos );
FillElement_RightTypes_recurseCase:
succ( CurOff, NextOff ) &
true(), NextOff, ExpLastPos, ElemType, "Fill", vals[ValElem], ObjL, OThId |-
ArrayElemL1 => ArrayElemL1_1, LastPos, Insts, ExObjL
--------------------------------
true(), CurOff, ExpLastPos, ElemType, "Fill", vals[ValElem], ObjL, OThId |-
vals[_.ArrayElemL1] => vals[ValElem.ArrayElemL1_1], LastPos, Insts, ExObjL ;
provided diff( CurOff, ExpLastPos );
NoMoreElementToFill:
true(), ExpLastPos, ExpLastPos, ElemType, "Fill", _, _, _ |-
ArrayElemL => ArrayElemL, ExpLastPos, insts[], objects[] ;
end setValuesToArray ;
end setArrayElements;
set arrayCompare is
judgement
ObjectId, integer, ObjectId, integer, integer, ObjectId |- Objects -> integer, Objects, Insts;
judgement
Insts, Vals, ObjectId, integer, integer, ObjectId |- Objects => integer, Objects, Insts;
judgement Insts, Objects |- Vals, Vals -> integer, Objects, Insts;
GetSrcArray:
getArrayElements(
SrcArrayId, SrcOff, Length, OThId |- ObjL1 -> SrcElem, ObjL1_1, Insts1 )
&
Insts1, SrcElem, DestArrayId, DestOff, Length, OThId |- ObjL1_1 => Result, ObjL1_2, Insts2
--------------------------------
SrcArrayId, SrcOff, DestArrayId, DestOff, Length, OThId |- ObjL1 -> Result, ObjL1_1, Insts2 ;
NoExceptionForTheSourceArray_GetDestArray:
getArrayElements(
DestArrayId, DestOff, Length, OThId |- ObjL1 -> DestElem, ObjL1_1, Insts1 )
& Insts1, ObjL1_1 |- SrcElem, DestElem -> Result, ObjL1_2, Insts2
--------------------------------
insts[], SrcElem, DestArrayId, DestOff, Length, OThId |- ObjL1 => Result, ObjL1_1, Insts2 ;
AnExceptionOccuredWhenGetingTheSourceArray:
Insts, _, _, _, _, _ |- ObjL => 1, ObjL, Insts ;
provided diff( Insts, insts[] );
NoExceptionForTheDestinationArray_ElementCompare:
ElementCompare( |- SrcElem, DestElem -> Result )
--------------------------------
insts[], ObjL |- SrcElem, DestElem -> Result, ObjL, insts[] ;
AnExceptionOccuredWhenGetingTheSourceArray:
Insts, ObjL |- _, _ -> 1, ObjL, Insts ;
provided diff( Insts, insts[] );
set ElementCompare is
judgement |- Vals, Vals -> integer;
SameElements_noMoreElementToCheck_0:
|- vals[], vals[] -> 0 ;
SameElements_recurseCase:
|- ValElemL1, ValElemL2 -> Result
--------------------------------
|- vals[ValElem.ValElemL1], vals[ValElem.ValElemL2] -> Result ;
SrcElementLessThanDestElement_endRecursion:
sub( 0, 1, Result )
--------------------------------
|- vals[integer ValElem1._], vals[integer ValElem2._] -> Result ;
provided
not_eq( ValElem1, objectId(_, _) ) & not_eq( ValElem2, objectId(_, _) ) &
inf( ValElem1, ValElem2 );
SrcElementGreaterThanDestElement_endRecursion:
|- vals[integer ValElem1._], vals[integer ValElem2._] -> 1 ;
provided sup( ValElem1, ValElem2 );
SrcElementLessThanDestElement_endRecursion:
sub( 0, 1, Result )
--------------------------------
|- vals[integer ValElem1._], vals[objectId(_, _)._] -> Result ;
SrcElementGreaterThanDestElement_endRecursion:
|- vals[objectId(_, _)._], vals[integer ValElem2._] -> 1 ;
SrcElementLessThanDestElement_endRecursion:
sub( 0, 1, Result )
--------------------------------
|-
vals[objectId(TF1, objectNumber ObjNb1)._], vals[objectId(TF2, objectNumber ObjNb2)._] -> Result ;
provided inf( ObjNb1, ObjNb2 );
SrcElementGreaterThanDestElement_endRecursion:
|-
vals[objectId(TF1, objectNumber ObjNb1)._], vals[objectId(TF2, objectNumber ObjNb2)._] -> 1 ;
provided sup( ObjNb1, ObjNb2 );
NotSameElement_endRecursion:
|- vals[objectId(TF1, ObjNb)._], vals[objectId(TF2, ObjNb)._] -> 1 ;
provided diff( TF1, TF2 );
end ElementCompare ;
end arrayCompare;
set resetArrayElements is
--
--JC: value used to reset the elements |- current element list (empty
--JC: list at the beginning) -> initialized element list
judgement Val |- Vals -> Vals;
NoMoreElementToReset: _ |- vals[] -> vals[] ;
MoreElementToReset:
InitVal |- ElemL -> ElemL1_1
--------------------------------
InitVal |- vals[_.ElemL] -> vals[InitVal.ElemL1_1] ;
end resetArrayElements;
end java_array_support