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.LocationVariable;
14: import de.uka.ilkd.key.logic.op.SetAsListOfQuantifiableVariable;
15: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
16: import de.uka.ilkd.key.rule.AbstractUpdateRule;
17: import de.uka.ilkd.key.rule.UpdateSimplifier;
18:
19: /**
20: * Rule used by the update simplifier as application of an update on
21: * a local variable or static variable
22: * Implements rule (S1) described in ....
23: */
24: public class ApplyOnLocalVariableOrStaticField extends
25: AbstractUpdateRule {
26:
27: /**
28: * creates an instance of this rule used by the given update
29: * simplifier
30: */
31: public ApplyOnLocalVariableOrStaticField(UpdateSimplifier us) {
32: super (us);
33: }
34:
35: /**
36: * determines whether this rule is applicable for the pair of
37: * update and target (the term on which the update will be
38: * applied) term.
39: * @param update the Update to be applied on target
40: * @param target the Term on which the update is applied
41: * @return true if the top level operator of target is a local
42: * variable
43: */
44: public boolean isApplicable(Update update, Term target) {
45: return target.op() instanceof LocationVariable;
46: }
47:
48: /**
49: */
50: public Term apply(Update update, Term target, Services services) {
51: logEnter(update, target);
52:
53: final Term result = UpdateSimplifierTermFactory.DEFAULT
54: .createIfExCascade(createCascade(update, target),
55: target);
56:
57: logExit(result);
58:
59: return result;
60: }
61:
62: private PVIfExCascade createCascade(Update update, Term target) {
63: return new PVIfExCascade(update
64: .getAssignmentPairs((LocationVariable) target.op()));
65: }
66:
67: private static class PVIfExCascade extends
68: IterateAssignmentPairsIfExCascade {
69:
70: public PVIfExCascade(ArrayOfAssignmentPair pairs) {
71: super (pairs);
72: }
73:
74: public Term getCondition() {
75: return getCurrentPair().guard();
76: }
77:
78: protected SetOfQuantifiableVariable criticalVars() {
79: return SetAsListOfQuantifiableVariable.EMPTY_SET;
80: }
81: }
82:
83: public Term matchingCondition(Update update, Term target,
84: Services services) {
85: return UpdateSimplifierTermFactory.DEFAULT
86: .matchingCondition(createCascade(update, target));
87: }
88: }
|