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.init;
09:
10: import de.uka.ilkd.key.proof.mgt.ComplexRuleJustification;
11: import de.uka.ilkd.key.proof.mgt.ComplexRuleJustificationBySpec;
12: import de.uka.ilkd.key.proof.mgt.RuleJustification;
13: import de.uka.ilkd.key.rule.ListOfBuiltInRule;
14: import de.uka.ilkd.key.rule.Rule;
15: import de.uka.ilkd.key.rule.UpdateSimplificationRule;
16: import de.uka.ilkd.key.rule.UseMethodContractRule;
17: import de.uka.ilkd.key.strategy.FOLStrategy;
18: import de.uka.ilkd.key.strategy.JavaCardDLStrategy;
19: import de.uka.ilkd.key.strategy.SetOfStrategyFactory;
20: import de.uka.ilkd.key.strategy.StrategyFactory;
21:
22: /**
23: * This profile is only used by test cases written for and to test KeY.
24: * @author bubel
25: */
26: public class JUnitTestProfile extends AbstractProfile {
27:
28: private final static StrategyFactory DEFAULT = new JavaCardDLStrategy.Factory();
29:
30: public JUnitTestProfile() {
31: super ("standardRules-junit.key", null);
32: }
33:
34: protected SetOfStrategyFactory getStrategyFactories() {
35: SetOfStrategyFactory set = super .getStrategyFactories();
36: set = set.add(DEFAULT);
37: set = set.add(new FOLStrategy.Factory());
38: return set;
39: }
40:
41: protected UseMethodContractRule getContractRule() {
42: return UseMethodContractRule.INSTANCE;
43: }
44:
45: protected UpdateSimplificationRule getUpdateSimplificationRule() {
46: return UpdateSimplificationRule.INSTANCE;
47: }
48:
49: protected ListOfBuiltInRule initBuiltInRules() {
50:
51: // update simplifier
52: ListOfBuiltInRule builtInRules = super .initBuiltInRules()
53: .prepend(getUpdateSimplificationRule());
54:
55: //contract insertion rule, ATTENTION: ProofMgt relies on the fact
56: // that Contract insertion rule is the FIRST element of this list!
57: builtInRules = builtInRules.prepend(getContractRule());
58:
59: return builtInRules;
60: }
61:
62: /**
63: * determines the justification of rule <code>r</code>. For a method contract rule it
64: * returns a new instance of a {@link ComplexRuleJustification} otherwise the rule
65: * justification determined by the super class is returned
66: *
67: * @return justification for the given rule
68: */
69: public RuleJustification getJustification(Rule r) {
70: return r == getContractRule() ? new ComplexRuleJustificationBySpec()
71: : super .getJustification(r);
72: }
73:
74: /**
75: * the name of the profile
76: */
77: public String name() {
78: return "Profile For JUnit Tests";
79: }
80:
81: /**
82: * the default strategy factory to be used
83: */
84: public StrategyFactory getDefaultStrategyFactory() {
85: return DEFAULT;
86: }
87:
88: }
|