|
| |
|
| java.lang.Object
 de.uka.ilkd.key.rule.updatesimplifier.Update
| Update | | abstract public class Update (Code) | | represents an update and is used as basis data structure for the
updatesimplifier. Currently this is only a naive default implementation.
|
| Inner Class :public static class UpdateInParts extends Update | |
| createUpdate | | public static Update createUpdate(AssignmentPair[] pairs)(Code) | | creates an update representation out of the top level operator of the
given update term
|
| createUpdate | | public static Update createUpdate(Term t)(Code) | | creates an update representation out of the top level operator of the
given update term. If it is no update term an update with zero assignment
pairs is returned (only for temporarly representations)
|
| freeVars | | abstract public SetOfQuantifiableVariable freeVars()(Code) | | the set of quantifiable variables that turn up free in thisupdate (when applying the update, it might happen that suchvariables have to be renaming to avoid collisions) |
| getAllAssignmentPairs | | abstract public ArrayOfAssignmentPair getAllAssignmentPairs()(Code) | | |
| getAssignmentPairs | | abstract public ArrayOfAssignmentPair getAssignmentPairs(Location loc)(Code) | | determines and returns all assignment pairs whose location part has the
same top level operator as the given one
|
| hasLocation | | abstract public boolean hasLocation(Location loc)(Code) | | returns true if the given location is updated by this update
Parameters:
location - the Operator specifying the location which is updated true if location occurs on the left side of an assignment pair inthis update |
| isAnonymousUpdate | | public boolean isAnonymousUpdate()(Code) | | returns true if this update object describes an anonymous update
|
| location | | abstract public Location location(int n)(Code) | | returns the n-th location operator
Parameters:
n - an int specifying the position of the location operator to beretrieved the n-tl location operator |
| locationCount | | abstract public int locationCount()(Code) | | returns the number of locations
the number of locations as int |
|
|
|