| java.lang.Object de.uka.ilkd.key.proof.DefaultGoalChooser de.uka.ilkd.key.proof.BalancedLoopGC
BalancedLoopGC | public class BalancedLoopGC extends DefaultGoalChooser (Code) | | This goal chooser takes care of a balanced unwinding of loops
acorss different proof branches.
Selects only goals on which no loop expand rule will be applied
next. Then when no other goals are left it is done the other way
round until all loops have been expanded. This implements a
rudimentary fairness measure for symbolic execution for
test case generation purposes preventing that shorter execution
paths through a loop body are favoured over longer ones.
|
getNextGoal | public Goal getNextGoal()(Code) | | the next goal a taclet should be applied to |
loopExpandCriterion | protected boolean loopExpandCriterion(Taclet t)(Code) | | |
methodExpandCriterion | protected boolean methodExpandCriterion(Taclet t)(Code) | | |
splitCriterion | protected boolean splitCriterion(Taclet t)(Code) | | |
Fields inherited from de.uka.ilkd.key.proof.DefaultGoalChooser | protected ListOfGoal selectedList(Code)(Java Doc)
|
|
|