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.RuleSource;
11: import de.uka.ilkd.key.rule.ListOfBuiltInRule;
12:
13: /**
14: * This class contains the standard rules provided by a profile.
15: */
16: public class RuleCollection {
17:
18: private final ListOfBuiltInRule standardBuiltInRules;
19: private final RuleSource standardTaclets;
20:
21: public RuleCollection(RuleSource standardTaclets,
22: ListOfBuiltInRule standardBuiltInRules) {
23: this .standardTaclets = standardTaclets;
24: this .standardBuiltInRules = standardBuiltInRules;
25: }
26:
27: /** returns the rule source containg all taclets for this profile */
28: public RuleSource getTacletBase() {
29: return standardTaclets;
30: }
31:
32: /** returns a list of all built in rules to be used */
33: public ListOfBuiltInRule getStandardBuiltInRules() {
34: return standardBuiltInRules;
35: }
36:
37: /** toString */
38: public String toString() {
39: return "Taclets: " + standardTaclets.toString() + "\n BuiltIn:"
40: + standardBuiltInRules;
41: }
42:
43: }
|