| java.lang.Object
 de.uka.ilkd.key.logic.TermBuilder
All known Subclasses: de.uka.ilkd.key.rule.metaconstruct.InReachableStatePOBuilder, de.uka.ilkd.key.parser.jml.JMLTranslator, de.uka.ilkd.key.jml.JMLSpec, de.uka.ilkd.key.java.TypeConverter,
| TermBuilder | | public class TermBuilder (Code) | | Use this class if you intend to build complex terms by hand. It is
more convenient than the @link{TermFactory} class.
Most convenient is its use when being subclassed. Therefore move the term
constructing methods of your application to a separate class and let the new
class extend the TermBuilder.
Attention: some methods of this class try to simplify some terms. So if you
want to be sure that the term looks exactly as you built it, you
will have to use the TermFactory.
|
| Method Summary | |
| public Term | FALSE(Services services)
| | public Term | NULL(Services services)
| | public Term | TRUE(Services services)
| | public Term | all(QuantifiableVariable lv, Term t2)
| | public Term | all(QuantifiableVariable[] lv, Term t2)
| | public Term | and(Term t1, Term t2)
| | public Term | and(Term[] subTerms)
| | public Term | and(ListOfTerm subTerms)
| | public Term | array(Term ref, Term idx)
| | public Term | box(JavaBlock jb, Term t)
| | public Term | dia(JavaBlock jb, Term t)
| | public Term | dot(Term o, ProgramVariable a)
| | public Term | equals(Term t1, Term t2)
| | public Term | equiv(Term t1, Term t2)
| | public Term | ex(QuantifiableVariable lv, Term t2)
| | public Term | ex(QuantifiableVariable[] lv, Term t2)
| | public Term | ff()
| | public Term | func(TermSymbol op)
| | public Term | func(TermSymbol op, Term s)
| | public Term | func(TermSymbol op, Term s1, Term s2)
| | public Term | func(TermSymbol op, Term[] s)
| | public Term | geq(Term t1, Term t2, Services services)
| | public Term | gt(Term t1, Term t2, Services services)
| | public Term | ife(Term cond, Term _then, Term _else)
| | public Term | imp(Term t1, Term t2)
| | public Term | leq(Term t1, Term t2, Services services)
| | public Term | lt(Term t1, Term t2, Services services)
| | public Term | not(Term t)
| | public Term | one(Services services)
| | public Term | or(Term t1, Term t2)
| | public Term | or(Term[] subTerms)
| | public Term | or(ListOfTerm subTerms)
| | public TermFactory | tf()
| | public Term | tt()
| | public Term | var(LogicVariable v)
| | public Term | var(ProgramVariable v)
| | public Term | var(ParsableVariable v)
| | public Term | zTerm(Services services, String numberString)
| | public Term | zero(Services services)
|
| TermBuilder | | public TermBuilder()(Code) | | |
| zTerm | | public Term zTerm(Services services, String numberString)(Code) | | builds a Term from a number, given by a String
Parameters:
services - Services which contains the number-functions
Parameters:
numberString - String representing an integer Term in Z-Notation representing the given number |
|
|