| java.lang.Object de.uka.ilkd.key.logic.op.AnonymousUpdate
arity | public int arity()(Code) | | returns the arity of the operator
|
entryBegin | public int entryBegin(int locPos)(Code) | | |
entryEnd | public int entryEnd(int locPos)(Code) | | |
getAnonymousOperator | public static AnonymousUpdate getAnonymousOperator(Name name)(Code) | | returns the anonymous update of the given name or creates a
new one if it does not exist
Parameters: name - the Name of the anon update operator to look for the anonymous update operator |
getNewAnonymousOperator | public static AnonymousUpdate getNewAnonymousOperator()(Code) | | returns a new anonymous update
a new anonymous update |
isRigid | public boolean isRigid(Term term)(Code) | | true if the value of "term" having this operator as top-leveloperator and may not be changed by modalities |
locationCount | public int locationCount()(Code) | | |
locationSubtermsBegin | public int locationSubtermsBegin(int locPos)(Code) | | |
locationSubtermsEnd | public int locationSubtermsEnd(int locPos)(Code) | | |
locationsAsArray | public ArrayOfLocation locationsAsArray()(Code) | | |
sort | public Sort sort(Term[] term)(Code) | | returns the sort a term would have if constructed with this operator and
the given sunterms. It is assumed that the term would be allowed if
constructed.
Parameters: term - an array of Term containing the subterms of a (potential)simultaneous update term sort of the simultaneous update term consisting of the givensubterms, if this op would be the top symbol |
target | public Term target(Term t)(Code) | | the index of the subterm representing the formula/term the updateis applied to |
targetPos | public int targetPos()(Code) | | the position of the term the anonymous update is applied to
the sub term position of the target term |
validTopLevel | public boolean validTopLevel(Term term)(Code) | | checks whether the top level structure of the given
Term is
syntactically valid, given the assumption that the top level operator of
the term is the same as this Operator. The assumption that the top level
operator and the operator are equal is NOT checked.
true iff the top level structure of the Termis valid. |
valuePos | public int valuePos(int locPos)(Code) | | |
|
|