|
| |
|
| de.uka.ilkd.key.rule.updatesimplifier.AssignmentPair
All known Subclasses: de.uka.ilkd.key.rule.updatesimplifier.AssignmentPairImpl, de.uka.ilkd.key.rule.updatesimplifier.AbstractAssignmentPairLazy,
| AssignmentPair | | public interface AssignmentPair (Code) | | Models an assignment pair l_i := t_i of an update.
This data structure is only used for update simplification.
|
| Inner Class :public static class LocationAsKey | |
| boundVars | | ArrayOfQuantifiableVariable boundVars()(Code) | | Variables that be used to express parallel execution of
unboundedly/infinitely many updates
variables that are bound for this assignment pair |
| equalLocations | | boolean equalLocations(AssignmentPair p)(Code) | | compares the location of the given assignment pair with the
current location and returns true if they are equal
Parameters:
p - the AssignmentPair whose location is compared true if the location that is updated is equal to the locationof the given assignment pair |
| freeVars | | SetOfQuantifiableVariable freeVars()(Code) | | the set of quantifiable variables that turn up free in thisassignment pair |
| guard | | Term guard()(Code) | | The guard this update might have. This returns the formula true
in case of an unguarded assignment
|
| location | | Location location()(Code) | | returns the location operator
the location specifying operator |
| locationAsTerm | | Term locationAsTerm()(Code) | | returns the location
the left side of the assignment |
| locationHashCode | | int locationHashCode()(Code) | | TODO: must guards and bound variables also be considered at this point?
returns an int fulfilling the usual hashcode properties but
without consideration of the value part of the assignment pair
an int as location hashcode |
| locationSubs | | Term[] locationSubs()(Code) | | returns the locations sub terms
the left side of the assignment |
| nontrivialGuard | | boolean nontrivialGuard()(Code) | | If this returns true then one cannot assume that the guard
is valid (always true)
|
| value | | Term value()(Code) | | returns the value that is assigned to the location and adds
if necessary (i.e. the static type T of the location as term is not a
supersort) a type cast (T) in front.
the right side of the assignment |
| valueUnsafe | | Term valueUnsafe()(Code) | | returns the value that is assigned to the location
without adding any cast. Use this method with care.
the right side of the assignment |
|
|
|