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:
11: /** this interface has to be implemented by all classes that want to
12: * act as a rule in the calculus. */package de.uka.ilkd.key.rule;
13:
14: import de.uka.ilkd.key.java.Services;
15: import de.uka.ilkd.key.logic.Name;
16: import de.uka.ilkd.key.proof.Goal;
17: import de.uka.ilkd.key.proof.ListOfGoal;
18:
19: public interface Rule {
20:
21: /**
22: * the rule is applied on the given goal using the
23: * information of rule application.
24: * @param goal the Goal on which to apply <tt>ruleApp</tt>
25: * @param services the Services with the necessary information
26: * about the java programs
27: * @param ruleApp the rule application to be executed
28: * @return all open goals below \old(goal.node()), i.e. the goals
29: * resulting from the rule application
30: */
31: ListOfGoal apply(Goal goal, Services services, RuleApp ruleApp);
32:
33: /**
34: * the name of the rule
35: */
36: Name name();
37:
38: /**
39: * returns the display name of the rule
40: */
41: String displayName();
42:
43: }
|