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 16.12.2004
11: *
12: * TODO To change the template for this generated file go to
13: * Window - Preferences - Java - Code Style - Code Templates
14: */
15: package de.uka.ilkd.key.rule;
16:
17: import de.uka.ilkd.key.java.Services;
18: import de.uka.ilkd.key.logic.Term;
19: import de.uka.ilkd.key.rule.updatesimplifier.Update;
20:
21: /**
22: * @author bubel
23: *
24: * TODO To change the template for this generated type comment go to
25: * Window - Preferences - Java - Code Style - Code Templates
26: */
27: public interface IUpdateRule {
28: /**
29: * Determines whether this rule is applicable for the pair of update and
30: * target (the term on which the update will be applied) term
31: *
32: * @param update
33: * the Update to be applied on the given term
34: * @param target
35: * the Term on which the update is applied
36: * @return true if the rule can be applied on the update, target pair
37: */
38: public abstract boolean isApplicable(Update update, Term target);
39:
40: /**
41: * Applies the update on the target term. This method must only be called if
42: * <code>isApplicable</code> returns <code>true</code> for this
43: * combination of update and target
44: *
45: * @param update
46: * the Update to be applied on target
47: * @param target
48: * the Term on which the update is applied
49: * @param services
50: * the Services object
51: * @return the Term resulting from the update on the target
52: */
53: public abstract Term apply(Update update, Term target,
54: Services services);
55:
56: /**
57: * Derive a formula that describes in which cases the top-level operator
58: * (location) described by <code>target</code> is updated by the given
59: * update. This method must only be called if <code>isApplicable</code>
60: * returns <code>true</code> for this combination of update and target
61: *
62: * @param update
63: * the modification of function interpretations that is
64: * considered
65: * @param target
66: * description of the location we are interested in;
67: * precondition: <code>target.op() instanceof Location</code>
68: * @param services
69: * the Services object
70: * @return formula that evaluates to <tt>true</tt> iff <code>update</code>
71: * evaluates to a semantic update that affects the location
72: * described by <code>target</code>
73: */
74: public abstract Term matchingCondition(Update update, Term target,
75: Services services);
76: }
|