-- $Id: java_inheritance.ty,v 1.11 99/08/10 14:48:09 hnilsson Exp $
-- /***************************************************************************/
-- /* Copyright (C) 1997-1999 INRIA Sophia-Antipolis */
-- /* I. Attali, D. Caromel, 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_inheritance is
use java;
use PSP;
import
getClassAPIDirectAncestor (
|- OptTypeName -> OptTypeName ) ,
getAPIObjectAttributes (
|- OptTypeName -> Pairs )
from java_api;
import
getObjectType ( ObjectId |- Objects -> Type ) ,
getRealTypeAndName (
Type, VariableDeclaratorId -> Type, Identifier ) ,
getRealName ( VariableDeclaratorId -> Identifier ) ,
getMethodNameAndParameters (
MethodDeclarator -> Identifier, Parameters )
from java_object_list;
import getCompilationUnit ( _ )
from jfunctions;
import appendtree ( _, _, _ ) , diff ( _, _ ) , not_eq ( _, _ ) , eq ( _, _ )
from prolog() ;
var TVValue: Val;
var TVMethodDecl: MethodDeclarator;
set getFieldDeclaration is
--SC: Retrieves the field declaration for the given field. Returns false if
--SC: it is not found.
--
--JC: Objects, Current class name where the fields is sought, Field arguments
--JC: (useful to find the right method or constructor declaration),
--JC: True (for a constructor declaration)/ False (for an attribute or method
--JC: declaration)
--JC: |- Field name -> Field declaration, Name of the class that owns this field (can be
--JC: a different name from the given one. In this case, it is
--JC: an ancestor), True if found/False otherwise.
judgement
Objects, Identifier, Vals, Bool |- Identifier -> FieldDeclaration, Identifier, Bool;
FieldInTheGivenClass:
getClassDeclaration( |- ClName -> ClDec )
&
getFieldDeclarationInClass(
ObjL, FName, ArgL, TF |- ClDec -> FDec, true() )
--------------------------------
ObjL, ClName, ArgL, TF |- FName -> FDec, ClName, true() ;
FieldInAnAncestorNotInTheGivenClass:
getClassDeclaration( |- ClName1 -> ClDec )
&
getFieldDeclarationInClass(
ObjL, FName, ArgL, TF |- ClDec -> _, false() ) &
getDirectAncestor( |- ClName1 -> Ancestor )
&
getFieldDeclarationInAncestors(
ObjL, Ancestor, ArgL, TF |- FName -> FDec, ClName2, true() )
--------------------------------
ObjL, ClName1, ArgL, TF |- FName -> FDec, ClName2, true() ;
end getFieldDeclaration;
set getFieldDeclarationInClass is
--SC: Retrieves the field declaration for the given field. Returns false if
--SC: it is not found. The first call is done with a class declaration. The
--SC: field declaration list of this class is retrieved and each field
--SC: declaration is checked to find the sought field.
--
--JC: Objects, Sought field name, Field arguments (useful to find the right
--JC: method or constructor declaration), True (for a constructor
--JC: declaration)/ False (for an attribute or method declaration)
--JC: |- Field declaration (Class, Field list, Constructor, Method, Attribute)
--JC: -> Field declaration, True if found/False otherwise.
judgement
Objects, Identifier, Vals, Bool |- java -> FieldDeclaration, Bool;
GetClassFieldDeclarationList:
ObjL, FName, ArgL, TF1 |- FDecL -> FDec, TF2
--------------------------------
ObjL, FName, ArgL, TF1 |- classDeclaration(_, _, _, _, FDecL) -> FDec, TF2 ;
EmptyFieldDeclarationList:
_, _, _, _ |- fieldDeclarations[] -> _, false() ;
FirstFieldAnalysis_GoodOne:
ObjL, FName, ArgL, TF |- FDec -> FDec, true()
--------------------------------
ObjL, FName, ArgL, TF |- fieldDeclarations[FDec._] -> FDec, true() ;
FirstFieldNotTheGoodOne_TailAnalysis:
ObjL, FName, ArgL, TF1 |- FDec1 -> _, false() &
ObjL, FName, ArgL, TF1 |- FDecL -> FDec2, TF2
--------------------------------
ObjL, FName, ArgL, TF1 |- fieldDeclarations[FDec1.FDecL] -> FDec2, TF2 ;
ConstructorDeclarationWhenConstructorNotSought:
_, _, _, false() |- constructorDeclaration(_, _, _, _) -> _, false() ;
MethodDeclaration_NotTheSoughtMethodName:
getMethodNameAndParameters(
TVMethodDecl -> MethName, _ ) & diff( FName, MethName )
--------------------------------
_, FName, _, false() |- methodDeclaration(_, _, TVMethodDecl, _, _) -> _, false() ;
MethodDeclaration_SoughtMethodName_SignatureAnalysis:
getMethodNameAndParameters(
TVMethodDecl -> MethName, ParamL ) & diff( MethName, identifier "main" )
&
isTheParameterListCorrespondingToTheArgumentList(
ObjL, ArgL |- ParamL -> TF )
--------------------------------
ObjL, MethName, ArgL, false() |-
methodDeclaration(ModL, RType, TVMethodDecl, ThrowL, Block) ->
methodDeclaration(ModL, RType, TVMethodDecl, ThrowL, Block), TF ;
MainMethodDeclaration:
getMethodNameAndParameters(
TVMethodDecl -> identifier "main", _ )
--------------------------------
_, identifier "main", vals[], false() |-
methodDeclaration(ModL, RType, TVMethodDecl, ThrowL, Block) ->
methodDeclaration(ModL, RType, TVMethodDecl, ThrowL, Block), true() ;
FieldVariableDeclaration_VariableDeclarationAnalysis:
isADirectAttribute( FName |- IdentL -> TF )
--------------------------------
_, FName, _, false() |-
fieldVariableDeclaration(ModL, Type, IdentL) -> fieldVariableDeclaration(ModL, Type, IdentL), TF ;
MethodDeclarationWhenAConstructorIsSought:
_, _, _, true() |- methodDeclaration(_, _, _, _, _) -> _, false() ;
ConstructorDeclaration_NotTheSoughtConstructorName:
_, ConstName1, _, true() |-
constructorDeclaration(_, constructor(ConstName2, _), _, _) -> _, false() ;
provided diff( ConstName1, ConstName2 );
ConstructorDeclaration_SoughtConstructorName_SignatureAnalysis:
isTheParameterListCorrespondingToTheArgumentList(
ObjL, ArgL |- ParamL -> TF )
--------------------------------
ObjL, ConstName, ArgL, true() |-
constructorDeclaration(ModL, constructor(ConstName, ParamL), ThrowL, Block) ->
constructorDeclaration(ModL, constructor(ConstName, ParamL), ThrowL, Block), TF ;
FieldVariableDeclaration_ConstructorSought:
_, _, _, true() |- fieldVariableDeclaration(_, _, _) -> _, false() ;
end getFieldDeclarationInClass;
set isADirectAttribute is
--SC: Looks for a given field name in the variables declarator list.
--
--JC: Sought field name
--JC: |- Variable declarator list (that belongs to a class)
--JC: -> True if the field was found in the given variable declarator list/
--JC: False otherwise
judgement Identifier |- VariableDeclarators -> Bool;
FoundAttribute_InitializedAttr:
getRealName( VarDeclId -> AttrName )
--------------------------------
AttrName |- variableDeclarators[initializedVariable(VarDeclId, _)] -> true() ;
FoundAttribute_NonInitializedAttr:
getRealName( VarDeclId -> AttrName )
--------------------------------
AttrName |- variableDeclarators[VarDeclId] -> true() ;
NotFoundAttribute_InitializedAttr:
getRealName( VarDeclId -> AttrName2 ) &
diff( AttrName1, AttrName2 )
--------------------------------
AttrName1 |- variableDeclarators[initializedVariable(VarDeclId, _)] -> false() ;
NotFoundAttribute_NonInitializedAttr:
getRealName( VarDeclId -> AttrName2 ) &
diff( AttrName1, AttrName2 )
--------------------------------
AttrName1 |- variableDeclarators[VarDeclId] -> false() ;
RecursiveRule_TheFirstInitializedVariableIsNotTheSoughtOne:
getRealName( VarDeclId -> AttrName2 ) &
diff( AttrName1, AttrName2 ) & AttrName1 |- AttrL -> TF
--------------------------------
AttrName1 |- variableDeclarators[initializedVariable(VarDeclId, _).AttrL] -> TF ;
RecursiveRule_TheFirstNonInitializedVariableIsNotTheSoughtOne:
getRealName( VarDeclId -> AttrName2 ) &
diff( AttrName1, AttrName2 ) & AttrName1 |- AttrL -> TF
--------------------------------
AttrName1 |- variableDeclarators[VarDeclId.AttrL] -> TF ;
end isADirectAttribute;
set isTheParameterListCorrespondingToTheArgumentList is
--SC: Checks if the parameter list and the argument list have the same number
--SC: of elements and if the corresponding elements have the same type.
--
--JC: Objects, Values
--JC: |- Parameters
--JC: -> True if the parameter list and the argument list have the same
--JC: number of elements and the same types for each element/False otherwise
judgement Objects, Vals |- Parameters -> Bool;
EmptyLists_Correspondence:
_, vals[] |- parameters[] -> true() ;
NotTheSameNumberOfArguments_NoCorrespondence:
haveTheSameNumberOfElements( ArgL, ParL -> false() )
--------------------------------
_, ArgL |- ParL -> false() ;
SameNumberOfArgumentAndSameTypeForAllTheArguments_Correspondence:
haveTheSameNumberOfElements( ArgL, ParL -> true() )
&
haveCompatibleTypeForEachElement( ObjL |- ArgL, ParL -> TF )
--------------------------------
ObjL, ArgL |- ParL -> TF ;
end isTheParameterListCorrespondingToTheArgumentList;
set haveCompatibleTypeForEachElement is
--SC: Checks if the corresponding members of the two given lists have the
--SC: same type.
--
--JC: Objects
--JC: |- Values, Parameters
--JC: -> True if all the values and the corresponding parameters have the
--JC: same types/False otherwise
judgement Objects |- Vals, Parameters -> Bool;
--iJC: Objects |- Value, Parameter -> True if the given value and parameter
--iJC: have the same type/False otherwise
judgement Objects |- Val, Parameter :> Bool;
EmptyLists_SameType: _ |- vals[], parameters[] -> true() ;
DifferentTypesForTheFirstElementOfEachList:
ObjL |- Value, Param :> false()
--------------------------------
ObjL |- vals[Value._], parameters[Param._] -> false() ;
RecursiveRule_haveCompatibleTypeForTheFirstElementsOfEachList:
ObjL |- Value, Param :> true() & ObjL |- ValueL, ParamL -> TF
--------------------------------
ObjL |- vals[Value.ValueL], parameters[Param.ParamL] -> TF ;
TwoIntegers: _ |- integer _, parameter(_, int(), _) :> true() ;
TwoBytes: _ |- integer _, parameter(_, byte(), _) :> true() ;
TwoShorts: _ |- integer _, parameter(_, short(), _) :> true() ;
TwoFloats: _ |- floating _, parameter(_, float(), _) :> true() ;
TwoDifferentPrimitiveTypes:
_ |- floating _, parameter(_, ParamType, _) :> true() ;
provided not_eq( ParamType, float() );
TwoObjectTypes_CheckForAssignmentCompatibility:
getRealTypeAndName( Type, VarDeclId -> RealType, _ )
&
hasCompatibleObjectType(
ObjL |- objectId(TF1, objectNumber i), RealType -> TF2 )
--------------------------------
ObjL |- objectId(TF1, objectNumber i), parameter(_, Type, VarDeclId) :> TF2 ;
end haveCompatibleTypeForEachElement;
set hasCompatibleObjectType is
--SC: Checks if the object has a type which is assignment compatible with
--SC: the given type (it may be an implicit cast)
--
--JC: Objects |- Object reference, Type
--JC: -> True if the object is assignable to a variable with the given type,
--JC: False otherwise.
judgement Objects |- ObjectId, Type -> Bool;
HasCompatibleObjectType:
--RC: Gets the object type and checks if an object of this type is
--RC: assignable to a variable of the given type (implicit cast).
getObjectType( ObjId |- ObjL -> ObjType )
& isMyAncestor( Type |- ObjType -> TF )
--------------------------------
ObjL |- ObjId, Type -> TF ;
end hasCompatibleObjectType;
set haveTheSameNumberOfElements is
--SC: Checks if the two given lists have the same number
--SC: of elements.
--
--JC: Value list, parameter list -> True if the two given
--JC: lists have the same number of elements, false otherwise
judgement (Vals, Parameters -> Bool);
EmptyLists_SameNumber: (vals[], parameters[] -> true()) ;
MoreValuesThanParameters: (vals[_._], parameters[] -> false()) ;
LessValuesThanParameters: (vals[], parameters[_._] -> false()) ;
RecursiveRule:
(ValueL, ParamL -> TF)
--------------------------------
(vals[_.ValueL], parameters[_.ParamL] -> TF) ;
end haveTheSameNumberOfElements;
set isAThread is
--SC: Checks if the given type is a Thread sub-class or
--SC: implements the Runnable interface.
--
--JC1: Type name -> True or False
judgement (OptTypeName => Bool);
--JC2: Object -> True of False
judgement (Object -> Bool);
Thread_SubClassThread:
isMyAncestor( identifier "Thread" |- ClName -> true() )
--------------------------------
(ClName => true()) ;
Thread_RunnableInterfaceImplementation:
isMyAncestor( identifier "Thread" |- ClName -> false() ) &
isMyInterface( identifier "Runnable" |- ClName -> true() )
--------------------------------
(ClName => true()) ;
NotAThread:
isMyAncestor( identifier "Thread" |- ClName -> false() ) &
isMyInterface( identifier "Runnable" |- ClName -> false() )
--------------------------------
(ClName => false()) ;
IsAThread:
(object(objectId(true(), _), _, _, _, _, _) -> true()) ;
IsNotAThread:
(object(objectId(false(), _), _, _, _, _, _) -> false()) ;
end isAThread;
set isMyAncestor is
--SC: Checks if the second type is a subtype of the first one. The check is
--SC: done firstly in the programm classes and then if the ancestor is still
--SC: not found in the API classes hierarchy.
--
--JC: The ancestor type |- the possible subtype -> True/False
judgement Type |- Type -> Bool;
IAmMyAncestor: Type |- Type -> true() ;
TwoArrays_CheckElementTypes:
Type1 |- Type2 -> TF
--------------------------------
arrayof(Type1) |- arrayof(Type2) -> TF ;
IsMyDirectAncestor:
getDirectAncestor( |- ClName2 -> ClName1 )
--------------------------------
ClName1 |- ClName2 -> true() ;
provided
diff( ClName1, ClName2 ) & not_eq( ClName1, arrayof(_) ) &
not_eq( ClName2, arrayof(_) );
RecursiveRule_IsItMyIndirectAncestor:
getDirectAncestor( |- ClName2 -> Ancestor )
& diff( Ancestor, identifier "Object" ) &
isMyAncestor( ClName1 |- Ancestor -> TF )
--------------------------------
ClName1 |- ClName2 -> TF ;
provided
diff( ClName1, ClName2 ) & not_eq( ClName1, arrayof(_) ) &
not_eq( ClName2, arrayof(_) );
RecursiveRule_IsItMyIndirectAPIAncestor:
getClassAPIDirectAncestor(
|- ClName2 -> Ancestor ) & diff( ClName1, Ancestor )
& diff( Ancestor, identifier "Object" ) & ClName1 |- Ancestor -> TF
--------------------------------
ClName1 |- ClName2 -> TF ;
provided
diff( ClName1, ClName2 ) & not_eq( ClName1, arrayof(_) ) &
not_eq( ClName2, arrayof(_) );
NoMoreAncestor_IsNotMyAPIAncestor:
getClassAPIDirectAncestor(
|- ClName2 -> identifier "Object" )
--------------------------------
ClName1 |- ClName2 -> false() ;
provided
diff( ClName1, ClName2 ) & not_eq( ClName1, arrayof(_) ) &
not_eq( ClName2, arrayof(_) );
IsMyAPIAncestor:
getClassAPIDirectAncestor(
|- ClName2 -> ClName1 )
--------------------------------
ClName1 |- ClName2 -> true() ;
provided
diff( ClName1, ClName2 ) & not_eq( ClName1, arrayof(_) ) &
not_eq( ClName2, arrayof(_) );
NoMoreAncestor_IsNotMyAncestor:
getClassDeclaration(
|- ClName2 -> classDeclaration(_, _, none(), _, _) )
--------------------------------
ClName1 |- ClName2 -> false() ;
provided
diff( ClName1, ClName2 ) & not_eq( ClName1, arrayof(_) ) &
not_eq( ClName2, arrayof(_) );
ObjectAncestor_IsNotMyAncestor:
getClassDeclaration(
|- ClName2 -> classDeclaration(_, _, identifier "Object", _, _) )
--------------------------------
ClName1 |- ClName2 -> false() ;
provided
diff( ClName1, ClName2 ) & diff( ClName1, identifier "Object" ) &
not_eq( ClName1, arrayof(_) ) & not_eq( ClName2, arrayof(_) );
end isMyAncestor;
set isMyInterface is
--SC: Checks if the given interface is a direct or indirect interface for the
--SC: given class.
--
--JC: Interface name |- Class name -> True/False
judgement OptTypeName |- OptTypeName -> Bool;
NoInterfaceForTheGivenClass_IsNotMyInterface:
getClassDeclaration(
|- ClName -> classDeclaration(_, _, _, typeNames[], _) )
--------------------------------
InterfName |- ClName -> false() ;
provided diff( InterfName, ClName );
IsOneOfMyInterface:
getClassDeclaration(
|- ClName -> classDeclaration(_, _, _, InterfNameL, _) ) &
diff( InterfNameL, typeNames[] ) &
isTheInterfaceInTheList( InterfName |- InterfNameL -> true() )
--------------------------------
InterfName |- ClName -> true() ;
provided diff( InterfName, ClName );
IsItOneOfMyIndirectInterface_CheckInterfaceHierarchy:
getClassDeclaration(
|- ClName -> classDeclaration(_, _, _, InterfNameL, _) ) &
diff( InterfNameL, typeNames[] ) &
isMyInterfaceAncestor( InterfName |- InterfNameL => TF )
--------------------------------
InterfName |- ClName -> TF ;
provided diff( InterfName, ClName );
IsItOneOfMyIndirectInterface_CheckClassHierarchy:
getDirectAncestor( |- ClName1 -> ClName2 )
& diff( ClName2, identifier "Object" ) &
InterfName |- ClName2 -> TF
--------------------------------
InterfName |- ClName1 -> TF ;
NoInterfaceInTheAPI: _ |- _ -> false() ;
end isMyInterface;
set isTheInterfaceInTheList is
--SC: Checks if the given interface is in the given interface list.
--
--JC: Interface name |- Interface list -> True/False
judgement Identifier |- TypeNames -> Bool;
EmptyList_NotInTheList: _ |- typeNames[] -> false() ;
FoundTheInterfaceInTheList:
InterfName |- typeNames[InterfName._] -> true() ;
RecursiveRule:
InterfName1 |- InterfNameL -> TF
--------------------------------
InterfName1 |- typeNames[InterfName2.InterfNameL] -> TF ;
provided diff( InterfName1, InterfName2 );
end isTheInterfaceInTheList;
set isMyInterfaceAncestor is
--SC: Checks if the given interface (the first) is inherited by one other
--SC: interface.
--
--JC: Sought interface name
--JC: |- Interfaces name list
--JC: -> true if the first interface is inherited by one interface of the list
--JC: false otherwise.
judgement Identifier |- TypeNames => Bool;
--iJC: Sought interface name
--iJC: |- Interface name
--iJC: -> true if the first interface is inherited by the second interface
--iJC: false otherwise.
judgement Identifier |- Identifier -> Bool;
EmptyList_NotMyInterfaceAncestor: _ |- typeNames[] => false() ;
FoundTheInterfaceAncestor:
--RC: Finds the given interface name into the interface hierarchy of the
--RC: first element of the interface name list.
InterfName1 |- InterfName2 -> true()
--------------------------------
InterfName1 |- typeNames[InterfName2._] => true() ;
RecursiveRuleOnTheNextElement:
InterfName1 |- InterfName2 -> false() &
InterfName1 |- InterfNameL => TF
--------------------------------
InterfName1 |- typeNames[InterfName2.InterfNameL] => TF ;
FoundTheInterfaceAncestor:
--RC: Retrieves the interface declaraction from the program and finds the
--RC: given interface name in the interface name list.
getInterfaceDeclaration(
|- InterfName2 -> interfaceDeclaration(_, _, InterfNameL, _) ) &
isTheInterfaceInTheList( InterfName1 |- InterfNameL -> true() )
--------------------------------
InterfName1 |- InterfName2 -> true() ;
provided diff( InterfName1, InterfName2 );
NoInheritedInterface_NotFound:
getInterfaceDeclaration(
|- InterfName2 -> interfaceDeclaration(_, _, typeNames[], _) )
--------------------------------
InterfName1 |- InterfName2 -> false() ;
provided diff( InterfName1, InterfName2 );
RecursiveRule_GoUpInTheHierarchy:
getInterfaceDeclaration(
|- InterfName2 -> interfaceDeclaration(_, _, InterfNameL, _) ) &
diff( InterfNameL, typeNames[] ) &
isTheInterfaceInTheList( InterfName1 |- InterfNameL -> false() )
& InterfName1 |- InterfNameL => TF
--------------------------------
InterfName1 |- InterfName2 -> TF ;
provided diff( InterfName1, InterfName2 );
end isMyInterfaceAncestor;
set getDirectAncestor is
--SC: Gets the direct ancestor of the given class.
--
--JC: |- Class name -> Direct ancestor name
judgement |- OptTypeName -> OptTypeName;
GetDirectAncestor:
getClassDeclaration(
|- ClName1 -> classDeclaration(_, _, ClName2, _, _) ) &
diff( ClName2, none() )
--------------------------------
|- ClName1 -> ClName2 ;
ClassObjectAsDirectAncestor:
getClassDeclaration(
|- ClName -> classDeclaration(_, _, none(), _, _) )
--------------------------------
|- ClName -> identifier "Object" ;
GetAPIDirectAncestor:
getClassAPIDirectAncestor(
|- ClName -> Ancestor )
--------------------------------
|- ClName -> Ancestor ;
end getDirectAncestor;
set getFieldDeclarationInAncestors is
--SC: Looks for the field declaration of the given field name. If nothing was
--SC: found, returns false.
--
--JC: Objects, Name of the class where the field is sought,
--JC: Field argument values, True if the sought field is a constructor/False
--JC: |- Sought field name
--JC: -> Field declaration, Name of the class where the field was found,
--JC: True if found/False
judgement
Objects, Identifier, Vals, Bool |- Identifier -> FieldDeclaration, Identifier, Bool;
ImpossibleToFindAFieldDeclarationInAPI:
getClassAPIDirectAncestor( ClName1 -> _ )
--------------------------------
_, ClName1, _, _ |- _ -> _, _, false() ;
FieldDeclarationInClass:
getClassDeclaration( |- ClName -> ClDec )
&
getFieldDeclarationInClass(
ObjL, FName, ArgL, TF |- ClDec -> FDec, true() )
--------------------------------
ObjL, ClName, ArgL, TF |- FName -> FDec, ClName, true() ;
RecursiveRule_FieldDeclarationMaybeInAncestors:
getClassDeclaration( |- ClName1 -> ClDec )
&
getFieldDeclarationInClass(
ObjL, FName, ArgL, TF1 |- ClDec -> _, false() ) &
getDirectAncestor( |- ClName1 -> Ancestor )
& ObjL, Ancestor, ArgL, TF1 |- FName -> FDec, ClName2, TF2
--------------------------------
ObjL, ClName1, ArgL, TF1 |- FName -> FDec, ClName2, TF2 ;
FieldNotFound_NoMoreAncestor:
_, _, _, _ |- _ -> _, _, false() ;
end getFieldDeclarationInAncestors;
set makeAttributeList is
--SC: Determines the attribute list correponding to a given type (useful for
--SC: an object creation).
--
--JC: |- Class name of the new instance
--JC: -> Initialized Attribute list
judgement |- OptTypeName -> Pairs;
DeclarationObject_InProgramClasses:
getClassDeclaration( ClName1 -> ClDec ) &
getLocalAttributeList( |- ClDec -> LocAttrL )
&
getDirectAncestor( |- ClName1 -> ClName2 )
&
makeInheritedAttributeList( LocAttrL |- ClName2 -> AttrL )
--------------------------------
|- ClName1 -> AttrL ;
DeclarationObject_inAPI:
getAPIObjectAttributes( |- ClName -> AttrL
)
--------------------------------
|- ClName -> AttrL ;
end makeAttributeList;
set getLocalAttributeList is
--SC: Gets the attributes local to the given class.
--
--JC: |- Declaration
--JC: -> Local attribute list
judgement |- java -> Pairs;
--iJC: The common (part of) the type
--iJC: |- Variable declarators
--iJC: -> Corresponding pair list
judgement Type |- VariableDeclarators -> Pairs;
GetTheFieldsDeclaration:
|- FDecL -> LocAttrL
--------------------------------
|- classDeclaration(_, _, _, _, FDecL) -> LocAttrL ;
NoMoreLocalAttribute:
|- fieldDeclarations[] -> pairs[] ;
RecursiveRule:
|- FDec -> AttrL1 &
|- FDecL -> AttrL2 & appendtree( AttrL1, AttrL2, AttrL3 )
--------------------------------
|- fieldDeclarations[FDec.FDecL] -> AttrL3 ;
MethodDeclaration_NotAnAttribute:
|- methodDeclaration(_, _, _, _, _) -> pairs[] ;
ConstructorDeclaration_NotAnAttribute:
|- constructorDeclaration(_, _, _, _) -> pairs[] ;
StaticVariable_NotInAttributeList:
isThisModifierInTheList( static() |- ModL -> true() )
--------------------------------
|- fieldVariableDeclaration(ModL, _, _) -> pairs[] ;
FieldVariableDeclaration_PutInTheAttributeList:
isThisModifierInTheList( static() |- ModL -> false() )
& Type |- FVarL -> AttrL
--------------------------------
|- fieldVariableDeclaration(ModL, Type, FVarL) -> AttrL ;
VariableWithDefaultValue:
getRealTypeAndName( Type, VarDeclId -> RealType, RealName )
&
getInitialValueForAGivenType( RealType -> Value )
--------------------------------
Type |- variableDeclarators[VarDeclId] -> pairs[pair(RealName, Value)] ;
InitializedVariable:
getRealTypeAndName( Type, VarDeclId -> _, RealName )
--------------------------------
_ |- variableDeclarators[initializedVariable(VarDeclId, TVValue)] -> pairs[pair(RealName, TVValue)] ;
RecursiveRuleWithAnInitializedVariable:
getRealTypeAndName( Type, VarDeclId -> _, RealName )
& Type |- AttrNameL -> AttrL
--------------------------------
Type |- variableDeclarators[initializedVariable(VarDeclId, TVValue).AttrNameL] ->
pairs[pair(RealName, TVValue).AttrL] ;
RecursiveRuleWithANonInitializedVariable_DefaultValueUsed:
getRealTypeAndName( Type, VarDeclId -> RealType, RealName )
&
getInitialValueForAGivenType( RealType -> Value )
& Type |- AttrNameL -> AttrL
--------------------------------
Type |- variableDeclarators[VarDeclId.AttrNameL] -> pairs[pair(RealName, Value).AttrL] ;
end getLocalAttributeList;
set isThisModifierInTheList is
--SC: Checks if the given modifier is contained in the given modifier list.
--SC: Returns true if found, false otherwise
--
--JC: Sought modifier |- Modifier list -> True/False
judgement Modifier |- Modifiers -> Bool;
FoundModifier: Mod |- modifiers[Mod._] -> true() ;
ModifierNotFound: _ |- modifiers[] -> false() ;
RecursiveRule:
Mod1 |- ModL -> TF
--------------------------------
Mod1 |- modifiers[Mod2.ModL] -> TF ;
provided diff( Mod1, Mod2 );
end isThisModifierInTheList;
set makeInheritedAttributeList is
--SC: Makes a list that contains all the inherited attributes (A check is
--SC: done to avoid multiple attributes with the same name in this list to
--SC: manage with the attribute shadowing mecanism)
--
--JC: List that contains all the attributes already retrieved (useful to
--JC: avoid having multiple attributes with the same name in the case of
--JC: attribute shadowing)
--JC: |- Class name (class of which the inherited attributes are wanted)
--JC: -> Inherited Attributes
judgement Pairs |- java -> Pairs;
ObjectAsDirectAncestor_NoMoreInheritedAttributes:
AttrL |- identifier "Object" -> AttrL ;
APIGetInheritedAttributes:
getAPIObjectAttributes( ClName -> AttrL1 )
&
joinTwoListsWithoutDuplication(
|- RetAttrL, AttrL1 -> AttrL2 ) &
getClassAPIDirectAncestor(
|- ClName -> ClNameDirectAncestor ) &
AttrL2 |- ClNameDirectAncestor -> AttrL3
--------------------------------
RetAttrL |- ClName -> AttrL3 ;
HaveOneDirectAncestor_LookForInheritedAttributes:
getClassDeclaration( |- ClName -> ClDec )
& RetAttrL |- ClDec -> AttrL
--------------------------------
RetAttrL |- ClName -> AttrL ;
provided diff( ClName, identifier "Object" );
RecursiveRule_GetCurrentClassAttributesAndGetTheInheritedOnes:
getLocalAttributeList(
|- classDeclaration(_, ClName1, _, _, FDecL) -> AttrL1 ) &
joinTwoListsWithoutDuplication(
|- RetAttrL1, AttrL1 -> RetAttrL2 ) &
getDirectAncestor( |- ClName1 -> ClName2 )
& RetAttrL2 |- ClName2 -> AttrL2
--------------------------------
RetAttrL1 |- classDeclaration(_, ClName1, _, _, FDecL) -> AttrL2 ;
set joinTwoListsWithoutDuplication is
--SC: Joins two lists without duplicating two attributes
--SC: that have the same name.
--
--JC: |- Attribute list, Attribute list -> concatenated list
--JC: without double.
judgement |- Pairs, Pairs -> Pairs;
EmptyList: |- pairs[], AttrL -> AttrL ;
EmptyList: |- AttrL, pairs[] -> AttrL ;
AttributeNotInTheOtherList:
isAMember( AttrName |- AttrL1 -> false() ) &
|- AttrL1, AttrL2 -> AttrL3 &
appendtree( pairs[pair(AttrName, Value)], AttrL3, AttrL4 )
--------------------------------
|- AttrL1, pairs[pair(AttrName, Value).AttrL2] -> AttrL4 ;
AttributeInTheList:
isAMember( AttrName |- AttrL1 -> true() ) &
|- AttrL1, AttrL2 -> AttrL3
--------------------------------
|- AttrL1, pairs[pair(AttrName, _).AttrL2] -> AttrL3 ;
end joinTwoListsWithoutDuplication ;
end makeInheritedAttributeList;
set isAMember is
--SC: Determines if the given identifier is already in the given pair list.
--
--JC: The sought identifier (e.g. an attribute)
--JC: |- List in which the identifier is sought
--JC: -> True/False
judgement Identifier |- Pairs -> Bool;
NoMoreElementInTheList_NoFound: _ |- pairs[] -> false() ;
HasFoundTheIdentifier:
Ident |- pairs[pair(Ident, _)._] -> true() ;
RecursiveRule:
Ident1 |- PairL -> TF
--------------------------------
Ident1 |- pairs[pair(Ident2, _).PairL] -> TF ;
provided diff( Ident1, Ident2 );
end isAMember;
set getClassDeclaration is
--SC: Gets the declaration of a given class from the program tree.
--
--JC: |- Name of the sought class
--JC: -> Class declaration
judgement |- OptTypeName -> TypeDeclaration;
--iJC: Name of the sought class
--iJC: |- Type declarations of the program
--iJC: Declaration of the sought class.
judgement OptTypeName |- TypeDeclarations -> TypeDeclaration;
GetTheCompilationUnit:
ClName |- TDecL -> ClDec
--------------------------------
|- ClName -> ClDec ;
provided
getCompilationUnit( compilationUnit(_, _, TDecL) );
HasFoundTheClassDeclaration:
ClName1 |- typeDeclarations[classDeclaration(ModL, ClName1, ClName2, InterfL, FDecL)._] ->
classDeclaration(ModL, ClName1, ClName2, InterfL, FDecL) ;
RecursiveRule_NotTheRightClass:
ClName1 |- TDecL -> ClDec
--------------------------------
ClName1 |- typeDeclarations[classDeclaration(_, ClName2, _, _, _).TDecL] -> ClDec ;
provided diff( ClName1, ClName2 ) & diff( TDecL, typeDeclarations[] );
InterfaceDeclaration:
ClName1 |- TDecL -> ClDec
--------------------------------
ClName1 |- typeDeclarations[interfaceDeclaration(_, _, _, _).TDecL] -> ClDec ;
provided diff( TDecL, typeDeclarations[] );
end getClassDeclaration;
set isAClass is
--SC: Determines if the given identifier is a class name or not.
--
--JC: Maybe a class name
--JC: -> True if it is a class/False
judgement (Identifier -> Bool);
IsAClass_HasADeclaration:
getClassDeclaration( ClName -> _ )
--------------------------------
(ClName -> true()) ;
NotAClass: (_ -> false()) ;
end isAClass;
set getInterfaceDeclaration is
--SC: Gets the declaration of a given interface from the program tree.
--
--JC: |- Name of the sought interface
--JC: -> Interface declaration
judgement |- OptTypeName -> TypeDeclaration;
--iJC: Name of the sought interface
--iJC: |- Type declarations of the program
--iJC: Declaration of the sought interface.
judgement OptTypeName |- TypeDeclarations -> TypeDeclaration;
getCompilationUnit:
InterfName1 |- TDecL -> InterDec
--------------------------------
|- InterfName1 -> InterDec ;
provided
getCompilationUnit( compilationUnit(_, _, TDecL) );
HasFoundTheInterface:
InterfName |- typeDeclarations[interfaceDeclaration(ModL, InterfName, InterfL, FDecL)._] ->
interfaceDeclaration(ModL, InterfName, InterfL, FDecL) ;
RecursiveRule_NotTheRightInterface:
InterfName1 |- TDecL -> InterfDec
--------------------------------
InterfName1 |- typeDeclarations[interfaceDeclaration(_, InterfName2, _, _).TDecL] -> InterfDec ;
provided diff( InterfName1, InterfName2 );
RecursiveRule_NoAClass:
InterfName |- TDecL -> InterfDec
--------------------------------
InterfName |- typeDeclarations[classDeclaration(_, _, _, _, _).TDecL] -> InterfDec ;
end getInterfaceDeclaration;
set getInitialValueForAGivenType is
--SC: Gets the default value for the given type
--
--JC: Type (float, double, int, byte, short, char, boolean, class)
--JC: -> Default value (e.g. 0, 0.0, null...)
judgement (Type -> Val);
Float: (float() -> floating "0.0") ;
Double: (double() -> floating "0.0") ;
Int: (int() -> integer 0) ;
Byte: (byte() -> integer 0) ;
Short: (short() -> integer 0) ;
Char: (char() -> character "\0") ;
Boolean: (boolean() -> false()) ;
Other:
(Any -> null()) ;
provided
diff( Any, float() ) & diff( Any, double() ) & diff( Any, int() )
& diff( Any, short() ) & diff( Any, char() ) &
diff( Any, boolean() );
end getInitialValueForAGivenType;
end java_inheritance