| java.lang.Object de.uka.ilkd.key.logic.ldt.ADT de.uka.ilkd.key.logic.ldt.LDT de.uka.ilkd.key.logic.ldt.BooleanLDT
BooleanLDT | public class BooleanLDT extends LDT (Code) | | This class inherits from LDT and implements all method that are
necessary to handle the primitive type boolean.
|
Method Summary | |
public Function | getFalseConst() | public Term | getFalseTerm() | public Function | getFunctionFor(de.uka.ilkd.key.java.expression.Operator op, Services services, ExecutionContext ec) | public Function | getTrueConst() | public Term | getTrueTerm() | public boolean | hasLiteralFunction(Function f) | public boolean | isResponsible(Literal lit) | public boolean | isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term[] subs, Services services, ExecutionContext ec) | public boolean | isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term left, Term right, Services services, ExecutionContext ec) | public boolean | isResponsible(de.uka.ilkd.key.java.expression.Operator op, Term sub, Services services, ExecutionContext ec) | public Term | translateLiteral(Literal lit) | public Expression | translateTerm(Term t, ExtList children) |
getFalseConst | public Function getFalseConst()(Code) | | returns the function representing the boolean value FALSE
the function representing the boolean value FALSE |
getTrueConst | public Function getTrueConst()(Code) | | returns the function representing the boolean value TRUE
the function representing the boolean value TRUE |
isResponsible | public boolean isResponsible(Literal lit)(Code) | | returns true if the LDT is responsible for this kind of literals
Parameters: lit - the Literal true if the LDT is responsible for this kind of literals |
isResponsible | 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 true if the LDT offers an operation for the given javaoperator and the subterms |
isResponsible | 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 true if the LDT offers an operation for the given javaoperator and the subterms |
isResponsible | 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 true if the LDT offers an operation for the given javaoperator and the subterm |
translateLiteral | 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 |
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)
|
|
|