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: /**
12: * rule application with specific information how and where the rule
13: * has to be applied
14: */package de.uka.ilkd.key.rule;
15:
16: import de.uka.ilkd.key.java.Services;
17: import de.uka.ilkd.key.logic.Constraint;
18: import de.uka.ilkd.key.logic.PosInOccurrence;
19: import de.uka.ilkd.key.proof.Goal;
20: import de.uka.ilkd.key.proof.ListOfGoal;
21:
22: public interface RuleApp {
23:
24: /**
25: * returns the rule of this rule application
26: */
27: Rule rule();
28:
29: /**
30: * returns the PositionInOccurrence (representing a ConstrainedFormula and
31: * a position in the corresponding formula) of this rule application
32: */
33: PosInOccurrence posInOccurrence();
34:
35: /**
36: * returns the constraint under which a rule is applicable
37: */
38: Constraint constraint();
39:
40: /** applies the specified rule at the specified position
41: * if all schema variables have been instantiated
42: * @param goal the Goal where to apply the rule
43: * @param services the Services encapsulating all java information
44: * @return list of new created goals
45: */
46: ListOfGoal execute(Goal goal, Services services);
47:
48: /** returns true if all variables are instantiated
49: * @return true if all variables are instantiated
50: */
51: boolean complete();
52:
53: }
|