| java.lang.Object
 de.uka.ilkd.key.logic.ldt.ADT
de.uka.ilkd.key.logic.ldt.LDT
All known Subclasses: de.uka.ilkd.key.logic.ldt.BooleanLDT, de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT,
| LDT | | abstract public class LDT extends ADT (Code) | | this class extends the class ADT and is used to represent language
datatype models e.g. a model for the java type int, boolean etc.
It contains the necessary function symbols, sorts and Taclets. The
class TypeConverter needs this class to convert java-program
constructs to logic terms.
|
| Constructor Summary | |
| public | LDT(Name name, Namespace sorts, Type type)
creates a new LDT complete with the target sort of the language
datatype, the java datatype, and sorts
Parameters:
name - the name of the language datatype model and the corresponding sort
Parameters:
sorts - namespace which contains the target sort
Parameters:
type - the type used in the java program esp. |
| Method Summary | |
| public Function | addFunction(Function f)
| | public Function | addFunction(Namespace funcNS, String funcName)
| | public boolean | containsFunction(Function op)
| | public Namespace | functions()
| | public String | getFile()
| | abstract public Function | getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services serv, ExecutionContext ec)
| | public KeYJavaType | getKeYJavaType(Type t)
| | abstract public boolean | hasLiteralFunction(Function f)
| | abstract public boolean | isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] subs, Services services, ExecutionContext ec)
| | abstract public boolean | isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term left, Term right, Services services, ExecutionContext ec)
| | abstract public boolean | isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, Services services, ExecutionContext ec)
| | public Type | javaType()
| | public SetOfTaclet | rules()
| | public Sort | targetSort()
| | public String | toString()
| | abstract public Term | translateLiteral(Literal lit)
| | abstract public Expression | translateTerm(Term t, ExtList children)
|
| sort | | final protected Sort sort(Code) | | the sort represented by the LDT
|
| type | | final protected Type type(Code) | | one LDT may model several program types; this is the list
of these types
|
| LDT | | public LDT(Name name, Namespace sorts, Type type)(Code) | | creates a new LDT complete with the target sort of the language
datatype, the java datatype, and sorts
Parameters:
name - the name of the language datatype model and the corresponding sort
Parameters:
sorts - namespace which contains the target sort
Parameters:
type - the type used in the java program esp. in the ASTof the java program |
| addFunction | | public Function addFunction(Function f)(Code) | | adds a function to the LDT
the added function (for convenience reasons) |
| addFunction | | public Function addFunction(Namespace funcNS, String funcName)(Code) | | looks up a function in the namespace and add it to the LDT
Parameters:
functions - a Namespace with symbols
Parameters:
String - the String with the name of the function to look up the added function (for convenience reasons) |
| functions | | public Namespace functions()(Code) | | returns the basic functions of the model
the basic functions of the model |
| getFile | | public String getFile()(Code) | | returns the file ID for the parser
|
| getKeYJavaType | | public KeYJavaType getKeYJavaType(Type t)(Code) | | returns the KeYJavaType for the the given type
Parameters:
t - the Type for which the coressponding KeYJavaType has to bereturned the KeYJavaType the the given type t |
| hasLiteralFunction | | abstract public boolean hasLiteralFunction(Function f)(Code) | | |
| isResponsible | | abstract public boolean isResponsible(de.uka.ilkd.key.java.expression.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
Parameters:
services - the Services
Parameters:
ec - the ExecutionContext in which the expression is evaluated true if the LDT offers an operation for the given javaoperator and the subterms |
| isResponsible | | abstract public boolean isResponsible(de.uka.ilkd.key.java.expression.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
Parameters:
services - the Services
Parameters:
ec - the ExecutionContext in which the expression is evaluated true if the LDT offers an operation for the given javaoperator and the subterms |
| isResponsible | | abstract public boolean isResponsible(de.uka.ilkd.key.java.expression.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
Parameters:
services - the Services
Parameters:
ec - the ExecutionContext in which the expression is evaluated * @param services TODO true if the LDT offers an operation for the given javaoperator and the subterm |
| javaType | | public Type javaType()(Code) | | returns the java type the model describes
the java type the model describes |
| rules | | public SetOfTaclet rules()(Code) | | returns the model specific rules
the model specific rules |
| targetSort | | public Sort targetSort()(Code) | | returns the sort the java type is mapped to
the sort the java type is mapped to |
| translateLiteral | | abstract public Term translateLiteral(Literal lit)(Code) | | translates a given literal to its logic counterpart
Parameters:
lit - the Literal to be translated the Term that represents the given literal in its logicform |
|
|