| de.uka.ilkd.key.rule.IUpdateRule
All known Subclasses: de.uka.ilkd.key.rule.AbstractUpdateRule,
| IUpdateRule | | public interface IUpdateRule (Code) | |
author:
bubel
author:
TODO To change the template for this generated type comment go to
author:
Window - Preferences - Java - Code Style - Code Templates |
| apply | | abstract public Term apply(Update update, Term target, Services services)(Code) | | Applies the update on the target term. This method must only be called if
isApplicable returns true for this
combination of update and target
Parameters:
update - the Update to be applied on target
Parameters:
target - the Term on which the update is applied
Parameters:
services - the Services object the Term resulting from the update on the target |
| isApplicable | | abstract public boolean isApplicable(Update update, Term target)(Code) | | Determines whether this rule is applicable for the pair of update and
target (the term on which the update will be applied) term
Parameters:
update - the Update to be applied on the given term
Parameters:
target - the Term on which the update is applied true if the rule can be applied on the update, target pair |
| matchingCondition | | abstract public Term matchingCondition(Update update, Term target, Services services)(Code) | | Derive a formula that describes in which cases the top-level operator
(location) described by target is updated by the given
update. This method must only be called if isApplicable
returns true for this combination of update and target
Parameters:
update - the modification of function interpretations that isconsidered
Parameters:
target - description of the location we are interested in;precondition: target.op() instanceof Location
Parameters:
services - the Services object formula that evaluates to true iff updateevaluates to a semantic update that affects the locationdescribed by target |
|
|