001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: package de.uka.ilkd.key.proof.init;
009:
010: import de.uka.ilkd.key.gui.Main;
011: import de.uka.ilkd.key.proof.SetOfGoalChooserBuilder;
012: import de.uka.ilkd.key.proof.mgt.ComplexRuleJustification;
013: import de.uka.ilkd.key.proof.mgt.ComplexRuleJustificationBySpec;
014: import de.uka.ilkd.key.proof.mgt.RuleJustification;
015: import de.uka.ilkd.key.rule.ListOfBuiltInRule;
016: import de.uka.ilkd.key.rule.Rule;
017: import de.uka.ilkd.key.rule.UpdateSimplificationRule;
018: import de.uka.ilkd.key.rule.UseMethodContractRule;
019: import de.uka.ilkd.key.strategy.FOLStrategy;
020: import de.uka.ilkd.key.strategy.JavaCardDLStrategy;
021: import de.uka.ilkd.key.strategy.SetOfStrategyFactory;
022: import de.uka.ilkd.key.strategy.StrategyFactory;
023:
024: /**
025: * This profile sets up KeY for verification of JavaCard programs.
026: *
027: */
028: public class JavaProfile extends AbstractProfile {
029:
030: private final static StrategyFactory DEFAULT = new JavaCardDLStrategy.Factory();
031:
032: protected JavaProfile(String standardRules,
033: SetOfGoalChooserBuilder gcb, Main main) {
034: super (standardRules, gcb, main);
035: }
036:
037: protected JavaProfile(String standardRules, Main main) {
038: super (standardRules, main);
039: }
040:
041: public JavaProfile() {
042: this ("standardRules.key", null);
043: }
044:
045: public JavaProfile(Main main) {
046: this ("standardRules.key", main);
047: }
048:
049: protected SetOfStrategyFactory getStrategyFactories() {
050: SetOfStrategyFactory set = super .getStrategyFactories();
051: set = set.add(DEFAULT);
052: set = set.add(new FOLStrategy.Factory());
053: return set;
054: }
055:
056: protected UseMethodContractRule getContractRule() {
057: return UseMethodContractRule.INSTANCE;
058: }
059:
060: protected UpdateSimplificationRule getUpdateSimplificationRule() {
061: return UpdateSimplificationRule.INSTANCE;
062: }
063:
064: protected ListOfBuiltInRule initBuiltInRules() {
065:
066: // update simplifier
067: ListOfBuiltInRule builtInRules = super .initBuiltInRules()
068: .prepend(getUpdateSimplificationRule());
069:
070: //contract insertion rule, ATTENTION: ProofMgt relies on the fact
071: // that Contract insertion rule is the FIRST element of this list!
072: builtInRules = builtInRules.prepend(getContractRule());
073:
074: return builtInRules;
075: }
076:
077: /**
078: * determines the justification of rule <code>r</code>. For a method contract rule it
079: * returns a new instance of a {@link ComplexRuleJustification} otherwise the rule
080: * justification determined by the super class is returned
081: *
082: * @return justification for the given rule
083: */
084: public RuleJustification getJustification(Rule r) {
085: return r == getContractRule() ? new ComplexRuleJustificationBySpec()
086: : super .getJustification(r);
087: }
088:
089: /**
090: * the name of the profile
091: */
092: public String name() {
093: return "Java Profile";
094: }
095:
096: /**
097: * the default strategy factory to be used
098: */
099: public StrategyFactory getDefaultStrategyFactory() {
100: return DEFAULT;
101: }
102:
103: }
|