| de.uka.ilkd.key.proof.IGoalChooser
All known Subclasses: de.uka.ilkd.key.proof.DefaultGoalChooser,
| IGoalChooser | | public interface IGoalChooser (Code) | | Interface to be implemented by classes in order to customize the goal selection
strategy of the automatic prover environment.
|
| Method Summary | |
| abstract public Goal | getNextGoal()
| | abstract public void | init(Proof p_proof, ListOfGoal p_goals)
Initialise this DefaultGoalChooser for use with a given Proof and a list of goals. | | abstract public void | removeGoal(Goal p_goal)
Remove p_goal from selectedList (e.g. | | abstract public void | updateGoalList(Node node, ListOfGoal newGoals)
|
| getNextGoal | | abstract public Goal getNextGoal()(Code) | | the next goal a taclet should be applied to |
| init | | abstract public void init(Proof p_proof, ListOfGoal p_goals)(Code) | | Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
Parameters:
p_proof - param p_goals the initial list of goals |
| removeGoal | | abstract public void removeGoal(Goal p_goal)(Code) | | Remove p_goal from selectedList (e.g. no taclet can be applied to
p_goal)
|
| updateGoalList | | abstract public void updateGoalList(Node node, ListOfGoal newGoals)(Code) | | The given node has become an internal node of the proof tree, and the
children of the node are the given goals
Parameters:
node -
Parameters:
newGoals - |
|
|