| de.uka.ilkd.key.logic.op.IUpdateOperator
All known Subclasses: de.uka.ilkd.key.logic.op.AnonymousUpdate, de.uka.ilkd.key.logic.op.QuanUpdateOperator,
| entryBegin | | int entryBegin(int locPos)(Code) | | the index of the first subterm belonging to update entrylocPos |
| entryEnd | | int entryEnd(int locPos)(Code) | | the index after the last subterm belonging to update entrylocPos. The entry is described within[entryBegin(i), entryEnd(i)) |
| getLocationPos | | int[] getLocationPos(Operator loc)(Code) | | returns an array with all location positions of loc
Parameters:
loc - a n Operator accessing a location all location positions of loc |
| location | | Location location(int n)(Code) | | returns the operator of n-th location
|
| location | | Term location(Term t, int n)(Code) | | returns the n-th location of the update as term
Parameters:
t - Term with this operator as top level operator
Parameters:
n - an int specifying the position of the requested location the n-th location of term t updated by this operator |
| locationCount | | int locationCount()(Code) | | returns the number of locations
the number of locations as int |
| locationSubtermsBegin | | int locationSubtermsBegin(int locPos)(Code) | | the index of the first subterm belonging to the location of entrylocPos |
| locationSubtermsEnd | | int locationSubtermsEnd(int locPos)(Code) | | the index after the last subterm belonging to the location ofupdate entry locPos. The location is describedwithin[locationSubtermsBegin(i), locationSubtermsEnd(i)) |
| locationsAsArray | | ArrayOfLocation locationsAsArray()(Code) | | returns the array of location operators which are updated
|
| replaceLocations | | IUpdateOperator replaceLocations(Location[] newLocs)(Code) | | Replace the locations of this operator without changing anything else.
This must not change the number of locations, i.e.
newLocs.length==locationCount()
|
| target | | Term target(Term t)(Code) | | return the subterm representing the formula/term the update is applied to
Parameters:
t - Term with this operator as top level operator the target of this update application |
| targetPos | | int targetPos()(Code) | | the index of the subterm representing the formula/term the updateis applied to |
| value | | Term value(Term t, int n)(Code) | | returns value the n-th location is updated with
Parameters:
t - Term with this operator as top level operator
Parameters:
n - an int specifying the position of the location the value the n-th location is updated with |
| valuePos | | int valuePos(int locPos)(Code) | | returns the number of the subterm representing the value to which
the locPos-th location is updated
|
|
|