| java.lang.Object
 de.uka.ilkd.key.rule.AbstractUpdateRule
de.uka.ilkd.key.rule.updatesimplifier.ApplyOnNonRigidWithExplicitDependencies
| ApplyOnNonRigidWithExplicitDependencies | | public class ApplyOnNonRigidWithExplicitDependencies extends AbstractUpdateRule (Code) | | This rule implements the update rule to be used for application on non rigid
functions with explicit dependency knowledge. The rule first sequentialzes
the simultaneous update and then propagates the independant part of the
update to the subterms. This rule may introduce new program
variables.
|
| Inner Class :public class ReplacementResult | |
| ApplyOnNonRigidWithExplicitDependencies | | public ApplyOnNonRigidWithExplicitDependencies(UpdateSimplifier updateSimplifier)(Code) | | Creates an instance of this rule for the given update simplifier
Parameters:
updateSimplifier - the UpdateSimplifier where the rule will be used |
| isApplicable | | public boolean isApplicable(Update update, Term target)(Code) | | This rule is applicable if the top operator of the target term is of kind
de.uka.ilkd.key.logic.op.NRFunctionWithExplicitDependencies
Parameters:
update - the Update to be applied on the target term
Parameters:
target - the Term on which the update is applied true iff this rule is responsible for simplication of the givenpair |
| matchingCondition | | public Term matchingCondition(Update update, Term target, Services services)(Code) | | as currently a
NRFunctionWithExplicitDependencies is not a
location and can therefore not appear on the left hand side of an update
this method must not be called. If this changes in future (e.g. the
attribute operator becomes a subclass of this kind of operator) the
method has to be implemented.
|
|
|