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.op.Location;
14: import de.uka.ilkd.key.rule.AbstractUpdateRule;
15: import de.uka.ilkd.key.rule.UpdateSimplifier;
16: import de.uka.ilkd.key.util.Debug;
17:
18: /**
19: * Rule used by the update simplifier as application of an update on
20: * a rigid function or variable.
21: * Implements rule (...) described in ....
22: */
23: public class ApplyOnRigidTerm extends AbstractUpdateRule {
24:
25: /**
26: * creates an instance of this rule used by the given update
27: * simplifier
28: */
29: public ApplyOnRigidTerm(UpdateSimplifier us) {
30: super (us);
31: }
32:
33: /**
34: * determines whether this rule is applicable for the pair of
35: * update and target (the term on which the update will be
36: * applied) term.
37: * @param update the Update to be applied on target
38: * @param target the Term on which the update is applied
39: * @return true if the top level operator of target is a local
40: * variable
41: */
42: public boolean isApplicable(Update update, Term target) {
43: return target.isRigid();
44: }
45:
46: public Term apply(Update update, Term target, Services services) {
47: return target;
48: }
49:
50: public Term matchingCondition(Update update, Term target,
51: Services services) {
52: // these rigid operators should not be locations,
53: // otherwise something is very wrong
54: Debug.assertFalse(target.op() instanceof Location,
55: "Rewrite me!");
56: Debug
57: .fail("matchingCondition(...) must not be called for target "
58: + target);
59: return null; // unreachable
60: }
61: }
|