-- $Id: java_evaluate.ty,v 1.11 99/08/10 14:48:03 hnilsson 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_evaluate is
use java;
use PSP;
import
div ( _, _, _ ) , inf ( _, _ ) , infeq ( _, _ ) ,
mult ( _, _, _ ) , sub ( _, _, _ ) , sup ( _, _ ) ,
supeq ( _, _ ) from arith;
import
getStaticVariables ( OptTypeName |- ClassVariablesL -> Pairs ) ,
getObjectType ( ObjectId |- Objects -> Identifier )
from java_object_list;
import diff ( _, _ ) , plus ( _, _, _ ) from prolog() ;
var TVVal: Val;
var TVIdent: Identifier;
set evaluateBinaryOperation is
--SC: Binary operator evaluation (logic or arithmetic evaluation).
--SC: If a division by zero is detected, an exception is raised.
--SC: Possible binary operators:
--SC: xor, and, or, eq, neq, gtreq, gtr, lesseq, less plus, minus, times, div
--
--JC: |- Value1, Value2, Binary operator
--JC: -> Result
judgement |- Val, Val, BinaryOperator -> Val;
Xor_true:
|- TF1, TF2, xor() -> true() ;
provided diff( TF1, TF2 );
Xor_false: |- TF, TF, xor() -> false() ;
And_false:
|- _, false(), land() -> false() ;
And_false:
|- false(), _, land() -> false() ;
And_true:
|- true(), true(), land() -> true() ;
Or_false:
|- false(), false(), lor() -> false() ;
Or_true: |- true(), _, lor() -> true() ;
Or_true: |- _, true(), lor() -> true() ;
Eq_false:
|- Val1, Val2, eq() -> false() ;
provided diff( Val1, Val2 );
Eq_true: |- Val, Val, eq() -> true() ;
Neq_true:
|- Val1, Val2, neq() -> true() ;
provided diff( Val1, Val2 );
Neq_false: |- Val, Val, neq() -> false() ;
GtrEq_true:
supeq( n1, n2 )
--------------------------------
|- integer n1, integer n2, gtrEq() -> true() ;
GtrEq_false:
inf( n1, n2 )
--------------------------------
|- integer n1, integer n2, gtrEq() -> false() ;
Gtr_true:
sup( n1, n2 )
--------------------------------
|- integer n1, integer n2, gtr() -> true() ;
Gtr_false:
infeq( n1, n2 )
--------------------------------
|- integer n1, integer n2, gtr() -> false() ;
LessEq_true:
infeq( n1, n2 )
--------------------------------
|- integer n1, integer n2, lessEq() -> true() ;
LessEq_false:
sup( n1, n2 )
--------------------------------
|- integer n1, integer n2, lessEq() -> false() ;
Less_true:
inf( n1, n2 )
--------------------------------
|- integer n1, integer n2, less() -> true() ;
Less_false:
supeq( n1, n2 )
--------------------------------
|- integer n1, integer n2, less() -> false() ;
Plus:
plus( n1, n2, n3 )
--------------------------------
|- integer n1, integer n2, plus() -> integer n3 ;
Times:
mult( n1, n2, n3 )
--------------------------------
|- integer n1, integer n2, times() -> integer n3 ;
Minus:
sub( n1, n2, n3 )
--------------------------------
|- integer n1, integer n2, minus() -> integer n3 ;
Div_by_Zero:
|-
integer n1, integer 0, div() -> except(identifier "ArithmeticException", null(), exceptText "Division by zero") ;
Div_notByZero:
div( n1, n2, n3 )
--------------------------------
|- integer n1, integer n2, div() -> integer n3 ;
provided diff( n2, 0 );
end evaluateBinaryOperation;
set evaluateUnaryOperation is
--SC: Unary operator evaluation (logic or arithmetic evaluation).
--SC: Handled operators: plus, minus, not
--SC: Missing operators: complement
--
--JC: |- Value, Unary operator
--JC: -> Result
judgement |- Val, UnaryOperator -> Val;
Not_true: |- true(), not() -> false() ;
Not_false: |- false(), not() -> true() ;
UnaryPlus:
|- integer n, plus() -> integer n ;
UnaryMinus:
sub( 0, n, minus_n )
--------------------------------
|- integer n, minus() -> integer minus_n ;
end evaluateUnaryOperation;
set getParameterOrLocalOrStaticVariableValue is
--SC: Gets the value of an identifier.
--
--JC: Environment of the method call, Class variable list, Current class name
--JC: |- Sought variable name
--JC: -> Value of the sought variable.
judgement Env, ClassVariablesL, Identifier |- Identifier -> Val;
Parameter:
getValueInPairList( ParamName |- ParamL -> Value, true() )
--------------------------------
env(ParamL, _), _, _ |- ParamName -> Value ;
LocalVariable:
getValueInPairList( LocalVarName |- ParamL -> _, false() )
&
getLocalVariableValue( LocalVarName |- LocalVarL -> Value, true() )
--------------------------------
env(ParamL, LocalVarL), _, _ |- LocalVarName -> Value ;
StaticVariable:
getValueInPairList( StaticVarName |- ParamL -> _, false() )
&
getLocalVariableValue( StaticVarName |- LocalVarL -> _, false() )
&
getStaticVariables( ClName |- ClVarL -> StaticPairL )
&
getValueInPairList( StaticVarName |- StaticPairL -> Value, true() )
--------------------------------
env(ParamL, LocalVarL), ClVarL, ClName |- StaticVarName -> Value ;
end getParameterOrLocalOrStaticVariableValue;
set getVariableValue is
--SC: Gets the value of an identifier.
--
--JC: Object list, Class variable list, environment of the current method
--JC: Current object reference
--JC: |- Sought variable name
--JC: -> Value of the sought variable
judgement
Objects, ClassVariablesL, Env, ObjectId |- Identifier -> Val;
Parameter:
getValueInPairList( ParamName |- ParamL -> Value, true() )
--------------------------------
_, _, env(ParamL, _), _ |- ParamName -> Value ;
LocalVariable:
getValueInPairList( LocalVarName |- ParamL -> _, false() )
&
getLocalVariableValue( LocalVarName |- LocalVarL -> Value, true() )
--------------------------------
_, _, env(ParamL, LocalVarL), _ |- LocalVarName -> Value ;
AttributeOrStaticVariable:
getValueInPairList( Ident |- ParamL -> _, false() ) &
getLocalVariableValue( Ident |- LocalVarL -> _, false() )
&
getAttributeOrStaticVariableValue(
ObjL, ClVarL, ObjId |- Ident -> Value )
--------------------------------
ObjL, ClVarL, env(ParamL, LocalVarL), ObjId |- Ident -> Value ;
end getVariableValue;
set getLocalVariableValue is
--SC: Gets the value of an identifier if it is a local variable.
--
--JC: Sought local variable
--JC: |- Local variable lists
--JC: -> Its value, True if found/ false otherwise
judgement Identifier |- Locs -> Val, Bool;
NoMoreLocalVariable_ValueNotFound:
TVIdent |- locs[] -> integer 0, false() ;
HasFoundTheLocalVariable:
getValueInPairList( Ident |- LocVarL -> Val, true() )
--------------------------------
Ident |- locs[LocVarL._] -> Val, true() ;
NotInThisLocalVariableList_recursiveRuleOnTheOtherLists:
getValueInPairList( Ident |- LocVarL -> _, false() ) &
Ident |- LocVarLL -> Val, TF
--------------------------------
Ident |- locs[LocVarL.LocVarLL] -> Val, TF ;
end getLocalVariableValue;
set getAttributeOrStaticVariableValue is
--RC: Gets the value of an identifier if it is an attribute or a class
--RC: variable.
--
--JC: Objects, Class Variables, Object identifier
--JC: |- Sought identifier (attribute or static variable)
--JC: -> its value
judgement Objects, ClassVariablesL, ObjectId |- Identifier -> Val;
getAttributeValue( ObjL, ObjId |- Ident -> Val, true() )
--------------------------------
ObjL, _, ObjId |- Ident -> Val ;
getObjectType( ObjId |- ObjL -> ClName ) &
getStaticVariableValue(
ClVarL, ClName |- StaticVarName -> Value )
--------------------------------
ObjL, ClVarL, ObjId |- StaticVarName -> Value ;
end getAttributeOrStaticVariableValue;
set getStaticVariableValue is
--RC: Gets the value of an identifier if it is a class variable.
--
--JC: Class Variables, Name of the class which owns the sought class variable
--JC: |- sought class variable name
--JC: -> its value
judgement ClassVariablesL, Identifier |- Identifier -> Val;
getStaticVariables( ClName |- ClVarL -> StaticPairL )
&
getValueInPairList( StaticVarName |- StaticPairL -> Value, true() )
--------------------------------
ClVarL, ClName |- StaticVarName -> Value ;
end getStaticVariableValue;
set getAttributeValue is
--SC: Gets the value of an attribute
--
--JC: Object list, object that owns the given attribute
--JC: |- the sought attribute
--JC: -> its value, True if the attribute was found/ False otherwise
judgement Objects, ObjectId |- Identifier -> Val, Bool;
IsTheGivenObject_GetAttributeValue:
getValueInPairList( Ident |- AttrL -> Val, TF )
--------------------------------
objects[object(ObjId, _, AttrL, _, _, _)._], ObjId |- Ident -> Val, TF ;
NotTheGivenObject_RecursiveRuleOnObjectList:
ObjL, ObjId1 |- Ident -> Val, TF
--------------------------------
objects[object(ObjId2, _, _, _, _, _).ObjL], ObjId1 |- Ident -> Val, TF ;
provided diff( ObjId2, ObjId1 );
end getAttributeValue;
set getValueInPairList is
--SC: Gets the value of an identifier in a pair list.
--
--JC: Sought identifier
--JC: |- Pair List
--JC: -> Found value (zero if the identifier is not found),
--JC: True if found/ False otherwise
judgement Identifier |- Pairs -> Val, Bool;
NotFoundTheIdentifier: Ident |- pairs[] -> integer 0, false() ;
HasFoundTheValue_EmptyReference:
Ident |- pairs[pair(Ident, empty())._] -> null(), true() ;
HasFoundTheValue_NonEmptyReference:
Ident |- pairs[pair(Ident, Val)._] -> Val, true() ;
provided diff( Val, empty() );
NotTheGivenIdentifier_RecursiveRule:
Ident1 |- PairL -> Val, TF
--------------------------------
Ident1 |- pairs[pair(Ident2, _).PairL] -> Val, TF ;
provided diff( Ident2, Ident1 );
end getValueInPairList;
end java_evaluate