|
| |
|
| java.lang.Object
 de.uka.ilkd.key.logic.ldt.ADT
de.uka.ilkd.key.logic.ldt.LDT
de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT
All known Subclasses: de.uka.ilkd.key.logic.ldt.LongLDT, de.uka.ilkd.key.logic.ldt.IntLDT, de.uka.ilkd.key.logic.ldt.CharLDT, de.uka.ilkd.key.logic.ldt.ShortLDT, de.uka.ilkd.key.logic.ldt.ByteLDT, de.uka.ilkd.key.logic.ldt.IntegerLDT, de.uka.ilkd.key.logic.ldt.IntegerDomainLDT,
| AbstractIntegerLDT | | abstract public class AbstractIntegerLDT extends LDT (Code) | | This class inherits from LDT and implements all method that are
necessary to handle integers, shorts and bytes.
It loads the needed rule file and offers method to convert java
number types to their logic counterpart
|
| Method Summary | |
| public Function | getArithAddition()
| | public Function | getArithDivision()
| | public Function | getArithJavaIntAddition()
returns the function symbol interpreted as the Java addition on
int (or promotabel to int) operators, i.e. | | public Function | getArithModulo()
| | public Function | getArithMultiplication()
| | public Function | getArithSubstraction()
| | public Function | getCharSymbol()
| | public Function | getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services serv, ExecutionContext ec)
| | public Function | getGreaterOrEquals()
| | public Function | getGreaterThan()
| | abstract public Function | getInBoundsPredicate()
| | public Function | getJDivision()
| | public Function | getJModulo()
| | public Function | getJavaAddInt()
| | public Function | getJavaAddLong()
| | public Function | getJavaBitwiseAndInt()
| | public Function | getJavaBitwiseAndLong()
| | public Function | getJavaBitwiseNegation()
| | public Function | getJavaBitwiseOrInt()
| | public Function | getJavaBitwiseOrLong()
| | public Function | getJavaBitwiseXOrInt()
| | public Function | getJavaBitwiseXOrLong()
| | public Function | getJavaCastByte()
| | public Function | getJavaCastChar()
| | public Function | getJavaCastInt()
| | public Function | getJavaCastLong()
| | public Function | getJavaCastShort()
| | public Function | getJavaDivInt()
| | public Function | getJavaDivLong()
| | public Function | getJavaMod()
| | public Function | getJavaMulInt()
| | public Function | getJavaMulLong()
| | public Function | getJavaShiftLeftInt()
| | public Function | getJavaShiftLeftLong()
| | public Function | getJavaShiftRightInt()
| | public Function | getJavaShiftRightLong()
| | public Function | getJavaSubInt()
| | public Function | getJavaSubLong()
| | public Function | getJavaUnaryMinusInt()
| | public Function | getJavaUnaryMinusLong()
| | public Function | getJavaUnsignedShiftRightInt()
| | public Function | getJavaUnsignedShiftRightLong()
| | public Function | getLessOrEquals()
| | public Function | getLessThan()
| | public Function | getModuloLong()
| | public Function | getNegativeNumberSign()
| | public Function | getNegativeSign()
returns the unary function symbol for representing the negative value
e.g. | | public Function | getNumberLiteralFor(int number)
| | public Function | getNumberSymbol()
| | public Function | getNumberTerminator()
| | public boolean | hasLiteralFunction(Function f)
| | public boolean | isResponsible(Operator op, Term[] subs, Services services, ExecutionContext ec)
| | public boolean | isResponsible(Operator op, Term left, Term right, Services services, ExecutionContext ec)
| | public boolean | isResponsible(Operator op, Term sub, Services services, ExecutionContext ec)
| | public Term | translateLiteral(Literal lit)
| | public Expression | translateTerm(Term t, ExtList children)
|
| CHAR_ID_NAME | | final public static Name CHAR_ID_NAME(Code) | | |
| NEGATIVE_LITERAL_STRING | | final public static String NEGATIVE_LITERAL_STRING(Code) | | Public name constants
|
| NUMBERS_NAME | | final public static Name NUMBERS_NAME(Code) | | |
| greaterThan | | final protected Function greaterThan(Code) | | the function symbols for the integer operations.
Used as shortcuts.
|
| inByte | | final protected Function inByte(Code) | | the predicate symbols for being within boundaries
|
| numbers | | final protected Function numbers(Code) | | the function symbols used to represent literals
|
| unsignedshiftrightJint | | final protected Function unsignedshiftrightJint(Code) | | |
| unsignedshiftrightJlong | | final protected Function unsignedshiftrightJlong(Code) | | |
| getArithAddition | | public Function getArithAddition()(Code) | | returns the function symbol used to represent addition of
arithmetical integers
the function symbol for integer addition |
| getArithDivision | | public Function getArithDivision()(Code) | | returns the function symbol used to represent division of
the arithmetical integers
the function symbol used to represent integer division |
| getArithJavaIntAddition | | public Function getArithJavaIntAddition()(Code) | | returns the function symbol interpreted as the Java addition on
int (or promotabel to int) operators, i.e. this addition performs a modulo
operation wrt. to the range of type int. This function is independent
of the chosen integer semantics.
In case you want to represent the Java addition on operands promotable to int
which shall be interpreted by the chosen integer semantics use
AbstractIntegerLDT.getJavaAddInt instead
mathematical interpreted function realising the Java addition on operands of or promotableto type int |
| getArithModulo | | public Function getArithModulo()(Code) | | returns the function symbol used to represent the modulo operation of
the arithmetical integers
the function symbol used to represent the integer modulo operation |
| getArithMultiplication | | public Function getArithMultiplication()(Code) | | returns the function symbol used to represent multiplication on
the arithmetical integers
the function symbol used to represent integer multiplication |
| getArithSubstraction | | public Function getArithSubstraction()(Code) | | returns the function symbol used to represent substraction of
arithmetical integers
the function symbol for integer substraction |
| getGreaterOrEquals | | public Function getGreaterOrEquals()(Code) | | returns the boolean function symbol to compare two integer values
val1, val2 if val1 is greater or equals
val2
the boolean function symbol to compare two integer values |
| getGreaterThan | | public Function getGreaterThan()(Code) | | returns the boolean function symbol to compare two integer values
val1, val2 if val1 is greater than
val2
the boolean function symbol to compare two integer values |
| getInBoundsPredicate | | abstract public Function getInBoundsPredicate()(Code) | | |
| getJDivision | | public Function getJDivision()(Code) | | returns the function symbol used to represent java-like division of
the arithmetical integers
the function symbol used to represent integer division |
| getJModulo | | public Function getJModulo()(Code) | | returns the function symbol used to represent the java-like modulo operation of
the arithmetical integers
the function symbol used to represent the integer modulo operation |
| getJavaAddInt | | public Function getJavaAddInt()(Code) | | the function representing the Java operator when one of the
operators is an or can be promoted to an int
function representing the generic Java operator function |
| getJavaAddLong | | public Function getJavaAddLong()(Code) | | the function representing the Java operator when one of the
operators is of type long
function representing the generic Java operator function |
| getJavaBitwiseAndInt | | public Function getJavaBitwiseAndInt()(Code) | | the function representing the Java operator when one of the
operators is an or can be promoted to int
function representing the generic Java operator function |
| getJavaBitwiseAndLong | | public Function getJavaBitwiseAndLong()(Code) | | the function representing the Java operator when one of the
operators is of type long
function representing the generic Java operator function |
| getJavaBitwiseNegation | | public Function getJavaBitwiseNegation()(Code) | | the function representing the Java operator ~
function representing the generic Java operator function |
| getJavaBitwiseOrInt | | public Function getJavaBitwiseOrInt()(Code) | | the function representing the Java operator |
when one of the operands is an or can be promoted to int
function representing the generic Java operator function |
| getJavaBitwiseOrLong | | public Function getJavaBitwiseOrLong()(Code) | | the function representing the Java operator |
when one of the operands is of type long
function representing the generic Java operator function |
| getJavaBitwiseXOrInt | | public Function getJavaBitwiseXOrInt()(Code) | | the function representing the Java operator ^
when one of the operands is an or can be promoted to int
function representing the generic Java operator function |
| getJavaBitwiseXOrLong | | public Function getJavaBitwiseXOrLong()(Code) | | the function representing the Java operator ^
when one of the operands is exact of type long
function representing the generic Java operator function |
| getJavaCastByte | | public Function getJavaCastByte()(Code) | | the function representing the Java operator (byte)
function representing the generic Java operator function |
| getJavaCastChar | | public Function getJavaCastChar()(Code) | | the function representing the Java operator (char)
function representing the generic Java operator function |
| getJavaCastInt | | public Function getJavaCastInt()(Code) | | the function representing the Java operator (int)
function representing the generic Java operator function |
| getJavaCastLong | | public Function getJavaCastLong()(Code) | | the function representing the Java operator (long)
function representing the generic Java operator function |
| getJavaCastShort | | public Function getJavaCastShort()(Code) | | the function representing the Java operator (short)
function representing the generic Java operator function |
| getJavaDivInt | | public Function getJavaDivInt()(Code) | | the function representing the Java operator /
when one of the operands is an or a subtype of int
function representing the generic Java operator function |
| getJavaDivLong | | public Function getJavaDivLong()(Code) | | the function representing the Java operator /
when one of the operands is exact of type long
function representing the generic Java operator function |
| getJavaMod | | public Function getJavaMod()(Code) | | the function representing the Java operator %
when one of the operands is an or a subtype of int
function representing the generic Java operator function |
| getJavaMulInt | | public Function getJavaMulInt()(Code) | | the function representing the Java operator *
when one of the operands is an or a subtype of int
function representing the generic Java operator function |
| getJavaMulLong | | public Function getJavaMulLong()(Code) | | the function representing the Java operator *
when one of the operands is exact of type long
function representing the generic Java operator function |
| getJavaShiftLeftInt | | public Function getJavaShiftLeftInt()(Code) | | the function representing the Java operator <<
when one of the operands is an or a subtype of int
function representing the generic Java operator function |
| getJavaShiftLeftLong | | public Function getJavaShiftLeftLong()(Code) | | the function representing the Java operator <<
when one of the operands is exact of type long
function representing the generic Java operator function |
| getJavaShiftRightInt | | public Function getJavaShiftRightInt()(Code) | | the function representing the Java operator >>
when one of the operands is an or a subtype of int
function representing the generic Java operator function |
| getJavaShiftRightLong | | public Function getJavaShiftRightLong()(Code) | | the function representing the Java operator >>
when one of the operands is exact of type long
function representing the generic Java operator function |
| getJavaSubInt | | public Function getJavaSubInt()(Code) | | the function representing the Java operator -
when one of the operands is an or a subtype of int
function representing the generic Java operator function |
| getJavaSubLong | | public Function getJavaSubLong()(Code) | | the function representing the Java operator -
when one of the operands is exact of type long
function representing the generic Java operator function |
| getJavaUnaryMinusInt | | public Function getJavaUnaryMinusInt()(Code) | | the function representing the Java operator -expr
when one of the operands is an or a subtype of int
function representing the generic Java operator function |
| getJavaUnaryMinusLong | | public Function getJavaUnaryMinusLong()(Code) | | the function representing the Java operator -exprLong
when one of the operands is exact of type long
function representing the generic Java operator function |
| getJavaUnsignedShiftRightInt | | public Function getJavaUnsignedShiftRightInt()(Code) | | the function representing the Java operator >>>
when one of the operands is an or a subtype of int
function representing the generic Java operator function |
| getJavaUnsignedShiftRightLong | | public Function getJavaUnsignedShiftRightLong()(Code) | | the function representing the Java operator >>>
when one of the operands is exact of type long
function representing the generic Java operator function |
| getLessOrEquals | | public Function getLessOrEquals()(Code) | | returns the boolean function symbol to compare two integer values
val1, val2 if val1 is lesser or equal than
val2
the boolean function symbol to compare two integer values |
| getLessThan | | public Function getLessThan()(Code) | | returns the boolean function symbol to compare two integer values
val1, val2 if val1 is lesser than
val2
the boolean function symbol to compare two integer values |
| getModuloLong | | public Function getModuloLong()(Code) | | returns a function mapping an arithmetic integer to its Java long representation
|
| getNegativeNumberSign | | public Function getNegativeNumberSign()(Code) | | returns the unary function symbol for representing a negative
number literal
the function symbol used to represent negative number literals |
| getNegativeSign | | public Function getNegativeSign()(Code) | | returns the unary function symbol for representing the negative value
e.g. -(var)
the function symbol used to represent the negative sign |
| getNumberLiteralFor | | public Function getNumberLiteralFor(int number)(Code) | | |
| isResponsible | | public boolean isResponsible(Operator op, Term[] subs, Services services, ExecutionContext ec)(Code) | | returns true if the LDT offers an operation for the given java
operator and the logic subterms
Parameters:
op - the de.uka.ilkd.key.java.expression.Operator totranslate
Parameters:
subs - the logic subterms of the java operator true if the LDT offers an operation for the given javaoperator and the subterms |
| isResponsible | | public boolean isResponsible(Operator op, Term left, Term right, Services services, ExecutionContext ec)(Code) | | returns true if the LDT offers an operation for the given
binary java operator and the logic subterms
Parameters:
op - the de.uka.ilkd.key.java.expression.Operator totranslate
Parameters:
left - the left subterm of the java operator
Parameters:
right - the right subterm of the java operator true if the LDT offers an operation for the given javaoperator and the subterms |
| isResponsible | | public boolean isResponsible(Operator op, Term sub, Services services, ExecutionContext ec)(Code) | | returns true if the LDT offers an operation for the given
unary java operator and the logic subterms
Parameters:
op - the de.uka.ilkd.key.java.expression.Operator totranslate
Parameters:
sub - the logic subterms of the java operator true if the LDT offers an operation for the given javaoperator and the subterm |
| translateLiteral | | public Term translateLiteral(Literal lit)(Code) | | translates a given integer literal to its logic counterpart
Parameters:
lit - the Literal to be translated (has to be anIntLiteral of an LongLiteral |
| Methods inherited from de.uka.ilkd.key.logic.ldt.LDT | public Function addFunction(Function f)(Code)(Java Doc)
public Function addFunction(Namespace funcNS, String funcName)(Code)(Java Doc)
public boolean containsFunction(Function op)(Code)(Java Doc)
public Namespace functions()(Code)(Java Doc)
public String getFile()(Code)(Java Doc)
abstract public Function getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services serv, ExecutionContext ec)(Code)(Java Doc)
public KeYJavaType getKeYJavaType(Type t)(Code)(Java Doc)
abstract public boolean hasLiteralFunction(Function f)(Code)(Java Doc)
abstract public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] subs, Services services, ExecutionContext ec)(Code)(Java Doc)
abstract public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term left, Term right, Services services, ExecutionContext ec)(Code)(Java Doc)
abstract public boolean isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, Services services, ExecutionContext ec)(Code)(Java Doc)
public Type javaType()(Code)(Java Doc)
public SetOfTaclet rules()(Code)(Java Doc)
public Sort targetSort()(Code)(Java Doc)
public String toString()(Code)(Java Doc)
abstract public Term translateLiteral(Literal lit)(Code)(Java Doc)
abstract public Expression translateTerm(Term t, ExtList children)(Code)(Java Doc)
|
|
|
|