01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: package de.uka.ilkd.key.rule.updatesimplifier;
10:
11: import de.uka.ilkd.key.java.Services;
12: import de.uka.ilkd.key.logic.Term;
13: import de.uka.ilkd.key.logic.UpdateFactory;
14: import de.uka.ilkd.key.logic.op.*;
15: import de.uka.ilkd.key.rule.AbstractUpdateRule;
16: import de.uka.ilkd.key.rule.UpdateSimplifier;
17: import de.uka.ilkd.key.util.Debug;
18:
19: /**
20: * Applies an update on an array using rule ...
21: */
22: public class ApplyOnUpdate extends AbstractUpdateRule {
23:
24: private final UpdateFactory ufac;
25:
26: /**
27: * creates an instance of this rule used by the given update
28: * simplifier
29: */
30: public ApplyOnUpdate(UpdateSimplifier us) {
31: super (us);
32: // The update factory does not need <code>Services</code> for what we
33: // are doing with it
34: ufac = new UpdateFactory(null, us);
35: }
36:
37: /**
38: * determines whether this rule is applicable for the
39: * update x target (the term on which the update will be
40: * applied) pair
41: * @param update the Update to be applied on target
42: * @param target the Term on which the update is applied
43: * @return true if the top level operator of target is an
44: * attribute operator
45: */
46: public boolean isApplicable(Update update, Term target) {
47: return target.op() instanceof IUpdateOperator;
48: }
49:
50: /**
51: * determines whether this rule is applicable for the pair of update and
52: * target (the term on which the update will be applied) term
53: *
54: * @param update
55: * the Update to be applied on the given term
56: * @param target
57: * the Term on which the update is applied
58: * @param services
59: * the Services object
60: * @return true if the rule can be applied on the update, target pair
61: */
62: public Term apply(Update update, Term target, Services services) {
63: final Update targetUpdate = Update.createUpdate(target);
64: final Update composedUpdate = ufac.sequential(update,
65: targetUpdate);
66: final IUpdateOperator updateOp = (IUpdateOperator) target.op();
67: final Term subTarget = updateOp.target(target);
68: return ufac.apply(composedUpdate, subTarget);
69: }
70:
71: public Term matchingCondition(Update update, Term target,
72: Services services) {
73: // an update is not a location
74: Debug
75: .fail("matchingCondition(...) must not be called for target "
76: + target);
77: return null; // unreachable
78: }
79: }
|