| java.lang.Object
 de.uka.ilkd.key.logic.Term
All known Subclasses: de.uka.ilkd.key.logic.ProgramTerm, de.uka.ilkd.key.logic.QuanUpdateTerm, de.uka.ilkd.key.logic.BoundVarsTerm, de.uka.ilkd.key.logic.SubstitutionTerm, de.uka.ilkd.key.logic.IfExThenElseTerm, de.uka.ilkd.key.logic.QuantifierTerm, de.uka.ilkd.key.logic.OpTerm,
| Term | | abstract public class Term implements SVSubstitute(Code) | | In contrast to the distinction of formulas and terms as made by most of the
inductive definition of the syntax of a logic, an instance of this class can
stand for a term or a formula. This is done for implementation reasons, as
their structure is quite similar and there are good reasons concerning the
software's design/architecture (for example using same visitors, reduction of
case distinction, unified interfaces etc.). However, they are strictly
separated by their sorts. A formula (and just a formula) must have
the sort
Sort.FORMULA . Terms of a different sort are terms in the
customary logic sense. A term of sort formula is allowed exact there, where a
formuala in logic is allowed to appear, same for terms of different sorts.
Some words about other design decisions:
- terms are immutable, this means after a term object is created, it
cannot be changed. The advantage is that we can use term sharing and
saving a lot of memory space.
- Term has to be created using the
TermFactory and
not by using the constructors itself.
- Term is subclassed, but all subclasses have to be package private, so
that all other classes except
TermFactory know only the class
Term and its interface. Even most classes of the logic package.
- as it is immutable, most (all) attributes should be declared final
Term supports the
Visitor pattern. Two different visit strategies are
currently supported:
Term.execPostOrder(Visitor) and
Term.execPreOrder(Visitor) .
|
| Field Summary | |
| final public static ArrayOfQuantifiableVariable | EMPTY_VAR_LIST
| | protected SetOfQuantifiableVariable | freeVars
| | protected SetOfMetavariable | metaVars
|
| EMPTY_VAR_LIST | | final public static ArrayOfQuantifiableVariable EMPTY_VAR_LIST(Code) | | empty list of variables
|
| freeVars | | protected SetOfQuantifiableVariable freeVars(Code) | | caches the free variables of this term
|
| metaVars | | protected SetOfMetavariable metaVars(Code) | | caches the meta variables of this term
|
| Term | | protected Term(Operator op, Sort sort)(Code) | | creates a Term with top operator op
Parameters:
op - Operator at the top of the termstructure that startshere.
Parameters:
sort - the Sort of the term |
| arity | | abstract public int arity()(Code) | | returns the arity of the term
arity of the term |
| calculateHash | | protected int calculateHash()(Code) | | |
| checked | | public Term checked()(Code) | | checks whether the Term is valid on the top level. If this is
the case this method returns the Term unmodified. Otherwise a
TermCreationException is thrown.
this Term if the top level of the Term is valid. |
| depth | | abstract public int depth()(Code) | | returns the longest path from the top of the term to one of its leaves
an int representing the depth of this term |
| equals | | public boolean equals(Object o)(Code) | | true if o is syntactical equal to this term
Parameters:
o - the Object to be compared with this term true iff the given Term has the same values inoperator, sort, arity, varsBoundHere and javaBlock as this object. |
| equalsModRenaming | | public boolean equalsModRenaming(Object o)(Code) | | compares if two terms are equal modulo bound renaming
true iff the given Term has the same values inoperator, sort, arity, varsBoundHere and javaBlock as this objectmodulo bound renaming |
| execPostOrder | | public void execPostOrder(Visitor visitor)(Code) | | the visitor is handed through till the bottom of the tree and
then it walks upwards while at each upstep the method visit of
the visitor is called
Parameters:
visitor - the Visitor |
| execPreOrder | | public void execPreOrder(Visitor visitor)(Code) | | the visitor walks downwards the tree
while at each downstep the method visit of
the visitor is called
Parameters:
visitor - the Visitor |
| executableJavaBlock | | public JavaBlock executableJavaBlock()(Code) | | The primary diamond in this formula. Note that the default
implementation is the same as javaBlock() but
the semantics is different. See SimultaneousUpdateTerm.
|
| fillCaches | | protected void fillCaches()(Code) | | fills the cache variables
must be called in the constructors
|
| freeVars | | public SetOfQuantifiableVariable freeVars()(Code) | | returns the set of free quantifiable variables occuring in this term
the SetOfFree |
| hasRigidSubterms | | public boolean hasRigidSubterms()(Code) | | true iff all subterms of this term are rigid accordingto the value the method "isRigid" returns for them (this doesnot imply this term to be rigid itself!) |
| hashCode | | public int hashCode()(Code) | | returns the hashcode of the term
the hashcode of the Term. |
| isRigid | | final public boolean isRigid()(Code) | | retrieves if the evaluation of the term is state independant. It is
guaranteed that if the result is true then the value is
state independant. In case of false no such guarantee is
given i.e. the terms value may be the same in all states or not.
(safe approximation)
false if the value of this term may be changed bymodalities (otherwise, however, the result may also be false) |
| javaBlock | | public JavaBlock javaBlock()(Code) | | JavaBlock if term has diamond at the top level |
| metaVars | | public SetOfMetavariable metaVars()(Code) | | returns the set of metavariables that are part of this term
(metavariables are thought as placeholder for some gound term, whereas
the variables in freeVars are bound by some quantifier above)
the set of metavariables |
| op | | public Operator op()(Code) | | the top operator in "A and B" it is "and", in f(x,y) it is "f"
operator at the top |
| sort | | public Sort sort()(Code) | | returns the sort of the term
the sort of the term |
| sub | | abstract public Term sub(int nr)(Code) | | returns the nr-th direct subterm
Parameters:
nr - the int specifying the nr-th direct subterm |
| subAt | | public Term subAt(PosInTerm pos)(Code) | | returns subterm at the position specified by the given PosInTerm pos.
Parameters:
pos - the position of the wanted subterm the subterm that is specified by pos |
| toString | | public String toString()(Code) | | returns a linearized textual representation of this term
|
| varsBoundHere | | abstract public ArrayOfQuantifiableVariable varsBoundHere(int n)(Code) | | returns the array of variables the top level operator binds at the n-th
sub term
the bound variables for the n-th subterm |
|
|