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: import de.uka.ilkd.key.rule.IteratorOfRuleSet;
11: import de.uka.ilkd.key.rule.RuleApp;
12: import de.uka.ilkd.key.rule.Taclet;
13:
14: /**
15: * This goal chooser takes care of a balanced unwinding of loops
16: * acorss different proof branches.
17: *
18: * Selects only goals on which no loop expand rule will be applied
19: * next. Then when no other goals are left it is done the other way
20: * round until all loops have been expanded. This implements a
21: * rudimentary fairness measure for symbolic execution for
22: * test case generation purposes preventing that shorter execution
23: * paths through a loop body are favoured over longer ones.
24: */
25: public class BalancedLoopGC extends DefaultGoalChooser {
26:
27: private boolean split = false;
28:
29: /**
30: * @return the next goal a taclet should be applied to
31: */
32: public Goal getNextGoal() {
33: Goal result;
34:
35: if (selectedList.isEmpty())
36: return null;
37: selectedList = rotateList(selectedList);
38: Goal first = selectedList.head();
39: RuleApp next;
40: do {
41: result = selectedList.head();
42: next = result.getRuleAppManager().peekNext();
43: selectedList = rotateList(selectedList);
44: } while (selectedList.head() != first && next != null
45: && (next.rule() instanceof Taclet)
46: && (split ^ loopExpandCriterion((Taclet) next.rule())));
47: if (selectedList.head() == first && next != null
48: && (next.rule() instanceof Taclet)
49: && (split ^ loopExpandCriterion((Taclet) next.rule()))) {
50: split = !split;
51: }
52:
53: return result;
54: }
55:
56: protected boolean loopExpandCriterion(Taclet t) {
57: return ruleSetCriterion(t, "loop_expand");
58: }
59:
60: protected boolean splitCriterion(Taclet t) {
61: return t.goalTemplates().size() > 1;
62: }
63:
64: protected boolean methodExpandCriterion(Taclet t) {
65: return ruleSetCriterion(t, "method_expand");
66: }
67:
68: protected boolean ruleSetCriterion(Taclet t, String ruleSetName) {
69: IteratorOfRuleSet it = t.getRuleSets().iterator();
70: while (it.hasNext()) {
71: if (it.next().name().toString().equals(ruleSetName)) {
72: return true;
73: }
74: }
75: return false;
76: }
77:
78: }
|