de.uka.ilkd.key.symbolic_execution.strategy

Class SymbolicExecutionGoalChooser

java.lang.Object

de.uka.ilkd.key.prover.impl.DefaultGoalChooser

de.uka.ilkd.key.prover.impl.DepthFirstGoalChooser

de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionGoalChooser

All Implemented Interfaces:

GoalChooser

public class SymbolicExecutionGoalChooser
extends DepthFirstGoalChooser

This GoalChooser is a special implementation of the default DepthFirstGoalChooser. The difference is that a rule which creates a new symbolic execution tree node on a Goal is only applied if all other Goals will also creates new symbolic execution tree nodes. This has the advantage that invalid branches may closed before new symbolic execution tree nodes are created.

The order in which new symbolic execution tree nodes are created is also managed by this GoalChooser. The idea is that on each Goal a new symbolic execution tree node is created before on one Goal a second one will be created. This has the affect that for instance on all branches of a branch statement the next statement is evaluated before the first branch executes the second statement.

A second criteria is the used custom StopCondition of the current Proof. Goals on that the next set node is allowed are preferred to branches on which is not allowed. This is required to make sure that for instance a step over or step return result is completely performed on all Goals before on one Goal a further set node is executed.

Author:

Martin Hentschel

See Also:

SymbolicExecutionGoalChooserBuilder

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Set<Goal>	goalsToPrefer This Set is used to count on which Goals a symbolic execution node was executed.
private StopCondition	stopCondition The optional custom stop condition used in the current proof.

Fields inherited from class de.uka.ilkd.key.prover.impl.DefaultGoalChooser

allGoalsSatisfiable, currentSubtreeRoot, goalList, nextGoalCounter, nextGoals, proof, selectedList

Constructor Summary

Constructors

Constructor and Description
SymbolicExecutionGoalChooser()

Method Summary

Modifier and Type	Method and Description
Goal	getNextGoal()
void	init(Proof p_proof, ImmutableList<Goal> p_goals) Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.
void	removeGoal(Goal p_goal) Remove p_goal from selectedList (e.g. no taclet can be applied to p_goal)
void	updateGoalList(Node node, ImmutableList<Goal> newGoals) The given node has become an internal node of the proof tree, and the children of the node are the given goals

Methods inherited from class de.uka.ilkd.key.prover.impl.DepthFirstGoalChooser

insertNewGoals, updateGoalListHelp

Methods inherited from class de.uka.ilkd.key.prover.impl.DefaultGoalChooser

findMinimalSubtree, findMinimalSubtreeBelow, isSatisfiableSubtree, removeClosedGoals, rotateList, setupGoals

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

goalsToPrefer

private java.util.Set<Goal> goalsToPrefer

This Set is used to count on which Goals a symbolic execution node was executed. Initially it is filled in getNextGoal() with all possible Goals. Every call of getNextGoal() will then remove a Goal from this list. If a Goal is not contained in this list it is skipped in getNextGoal() until the Set is empty which indicates that on all Goals a symbolic execution tree node was created. Then the process starts again.

stopCondition

private StopCondition stopCondition

The optional custom stop condition used in the current proof.

Constructor Detail

SymbolicExecutionGoalChooser

public SymbolicExecutionGoalChooser()

Method Detail

getNextGoal

public Goal getNextGoal()

Specified by:

getNextGoal in interface GoalChooser

Overrides:

getNextGoal in class DepthFirstGoalChooser

Returns:

the next goal a taclet should be applied to

init

public void init(Proof p_proof,
                 ImmutableList<Goal> p_goals)

Initialise this DefaultGoalChooser for use with a given Proof and a list of goals.

Specified by:

init in interface GoalChooser

Overrides:

init in class DefaultGoalChooser

Parameters:

p_proof - *param p_goals the initial list of goals

removeGoal

public void removeGoal(Goal p_goal)

Remove p_goal from selectedList (e.g. no taclet can be applied to p_goal)

Specified by:

removeGoal in interface GoalChooser

Overrides:

removeGoal in class DefaultGoalChooser

updateGoalList

public void updateGoalList(Node node,
                           ImmutableList<Goal> newGoals)

The given node has become an internal node of the proof tree, and the children of the node are the given goals

Specified by:

updateGoalList in interface GoalChooser

Overrides:

updateGoalList in class DefaultGoalChooser