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: //
09: //
10:
11: package de.uka.ilkd.key.strategy;
12:
13: import de.uka.ilkd.key.logic.Named;
14: import de.uka.ilkd.key.proof.Proof;
15:
16: /**
17: * Interface for creating Strategy instances.
18: * The strategy name and the name of the strategy factory are assumed to be the same
19: * (you have to refactor if you want to change this).
20: */
21: public abstract class StrategyFactory implements Named {
22:
23: /**
24: * Create the strategy with the specified name.
25: * If there is no strategy with the specified name, this method behaves as
26: * if the name of the default strategy was given.
27: * @param proof the proof for which the strategy is to be created
28: * @param name the name of the strategy
29: * @return the strategy
30: */
31:
32: public static Strategy create(Proof proof, String name,
33: StrategyProperties strategyProperties) {
34:
35: StrategyFactory createdFactory = null;
36: try {
37: createdFactory = (StrategyFactory) Class.forName(
38: "de.uka.ilkd.key.strategy." + name + "$Factory")
39: .newInstance();
40: } catch (ClassNotFoundException e) {
41: throw new RuntimeException(e);
42: } catch (InstantiationException e) {
43: throw new RuntimeException(e);
44: } catch (IllegalAccessException e) {
45: throw new RuntimeException(e);
46: }
47:
48: return createdFactory.create(proof, strategyProperties);
49: }
50:
51: /**
52: * Create strategy for a proof.
53: * @param proof the Proof a strategy is created for
54: * @param strategyProperties the StrategyProperties to customize the
55: * strategy
56: * @return the newly created strategy
57: */
58: public abstract Strategy create(Proof proof,
59: StrategyProperties strategyProperties);
60:
61: }
|