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: package de.uka.ilkd.key.proof;
09:
10: /**
11: * Interface to be implemented by classes in order to customize the goal selection
12: * strategy of the automatic prover environment.
13: */
14: public interface IGoalChooser {
15:
16: /**
17: * Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
18: * @param p_proof
19: * *param p_goals the initial list of goals
20: */
21: public abstract void init(Proof p_proof, ListOfGoal p_goals);
22:
23: /**
24: * @return the next goal a taclet should be applied to
25: */
26: public abstract Goal getNextGoal();
27:
28: /**
29: * Remove p_goal from selectedList (e.g. no taclet can be applied to
30: * p_goal)
31: */
32: public abstract void removeGoal(Goal p_goal);
33:
34: /**
35: * The given node has become an internal node of the proof tree, and the
36: * children of the node are the given goals
37: * @param node
38: * @param newGoals
39: */
40: public abstract void updateGoalList(Node node, ListOfGoal newGoals);
41:
42: }
|