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: /*
10: * Created on 09.12.2004
11: */
12: package de.uka.ilkd.key.rule.updatesimplifier;
13:
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.logic.Term;
16: import de.uka.ilkd.key.logic.op.AnonymousUpdate;
17: import de.uka.ilkd.key.rule.AbstractUpdateRule;
18: import de.uka.ilkd.key.rule.UpdateSimplifier;
19: import de.uka.ilkd.key.util.Debug;
20:
21: /**
22: * Applies an update U on an anonymous update A. Only the latter one survives.
23: * @author bubel
24: */
25: public class ApplyOnAnonymousUpdate extends AbstractUpdateRule {
26:
27: /**
28: * create an instance of this rule
29: * @param updateSimplifier
30: */
31: public ApplyOnAnonymousUpdate(UpdateSimplifier updateSimplifier) {
32: super (updateSimplifier);
33: }
34:
35: /* (non-Javadoc)
36: * @see de.uka.ilkd.key.rule.UpdateRule#isApplicable(de.uka.ilkd.key.rule.updatesimplifier.Update, de.uka.ilkd.key.logic.Term)
37: */
38: public boolean isApplicable(Update update, Term target) {
39: return target.op() instanceof AnonymousUpdate;
40: }
41:
42: /* (non-Javadoc)
43: * @see de.uka.ilkd.key.rule.UpdateRule#apply(de.uka.ilkd.key.rule.updatesimplifier.Update, de.uka.ilkd.key.logic.Term)
44: */
45: public Term apply(Update update, Term target, Services services) {
46: logEnter(update, target);
47: Term result = updateSimplifier().simplify(target, services);
48: logExit(result);
49: return result;
50: }
51:
52: public Term matchingCondition(Update update, Term target,
53: Services services) {
54: // an anonymous update is not a location
55: Debug
56: .fail("matchingCondition(...) must not be called for target "
57: + target);
58: return null; // unreachable
59: }
60: }
|