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.collection.SetOfString;
011: import de.uka.ilkd.key.gui.configuration.ProofSettings;
012: import de.uka.ilkd.key.logic.Name;
013: import de.uka.ilkd.key.proof.GoalChooserBuilder;
014: import de.uka.ilkd.key.proof.mgt.RuleJustification;
015: import de.uka.ilkd.key.rule.Rule;
016: import de.uka.ilkd.key.strategy.SetOfStrategyFactory;
017: import de.uka.ilkd.key.strategy.StrategyFactory;
018:
019: /**
020: *
021: * This interface provides methods that allow to customize KeY for
022: * certain applications. It supports to customize
023: * <ul>
024: * <li> the rule base to be used </li>
025: * <li> the available strategies </li>
026: * <li> the goal selection strategy </li>
027: * </ul>
028: *
029: * Currently this is only rudimentary: possible extensions are
030: * <ul>
031: * <li> program model to use (java, misrac, csharp) </li>
032: * <li> integrate in plug-in framework allow addition of menu entries
033: * toolbar buttons etc.
034: * </li>
035: * </ul>
036: * etc.
037: */
038: public interface Profile {
039:
040: /** returns the rule source containg all taclets for this profile */
041: RuleCollection getStandardRules();
042:
043: /** the name of this profile */
044: String name();
045:
046: /** returns the strategy factories for the supported strategies */
047: SetOfStrategyFactory supportedStrategies();
048:
049: /**
050: * returns the strategy factory for the default strategy of this profile
051: */
052: StrategyFactory getDefaultStrategyFactory();
053:
054: /**
055: * returns true if strategy <code>strategyName</code> may be
056: * used with this profile.
057: * @return supportedStrategies()->exists(s | s.name.equals(strategyName))
058: */
059: boolean supportsStrategyFactory(Name strategyName);
060:
061: /**
062: * returns the StrategyFactory for strategy <code>strategyName</code>
063: * @param strategyName the Name of the strategy
064: * @return the StrategyFactory to build the demanded strategy
065: */
066: StrategyFactory getStrategyFactory(Name strategyName);
067:
068: /**
069: * returns the names of possible goalchoosers to be used by the
070: * automatic prover environment
071: */
072: SetOfString supportedGoalChoosers();
073:
074: /**
075: * returns the default builder for a goal chooser
076: */
077: GoalChooserBuilder getDefaultGoalChooserBuilder();
078:
079: /**
080: * sets the user selected goal chooser builder to be used as prototype
081: * @param name the String with the name of the goal chooser to be used
082: * @throws IllegalArgumentException if a goal chooser of the given name is not
083: * supported
084: */
085: void setSelectedGoalChooserBuilder(String name);
086:
087: /**
088: * returns a new builder instance for the selected goal choooser
089: */
090: GoalChooserBuilder getSelectedGoalChooserBuilder();
091:
092: /** returns the (default) justification for the given rule */
093: RuleJustification getJustification(Rule r);
094:
095: /**
096: *
097: * @param settings the ProofSettings to be updated to defaults provided by
098: * this profile
099: */
100: void updateSettings(ProofSettings settings);
101: }
|