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.rule;
12:
13: /**
14: * Due to the immutability of {@link Taclet}s, they are created in the parsers
15: * using {@link TacletBuilder}s. This builder is used for
16: * {@link NoFindTaclet} rules. Besides this some tests are performed that avoid
17: * some common errors on applicability of taclets.
18: */
19: public class NoFindTacletBuilder extends TacletBuilder {
20:
21: /** builds and returns the RewriteTaclet that is specified by
22: * former set... / add... methods. If no name is specified then
23: * an Taclet with an empty string name is build. No specifications
24: * for variable conditions, goals or heuristics imply that the
25: * corresponding parts of the Taclet are empty. No specification for
26: * the if-sequent is represented as a sequent with two empty
27: * semisequences. No specification for the interactive or
28: * recursive flags imply that the flags are not set.
29: */
30: public NoFindTaclet getNoFindTaclet() {
31:
32: TacletPrefixBuilder prefixBuilder = new TacletPrefixBuilder(
33: this );
34: prefixBuilder.build();
35: return new NoFindTaclet(this .name, new TacletApplPart(ifseq,
36: varsNew, varsNotFreeIn, varsNewDependingOn,
37: variableConditions), goals, ruleSets, constraint,
38: attrs, prefixBuilder.getPrefixMap(), choices);
39: }
40:
41: /**
42: * adds a new goal descriptions to the goal descriptions of the Taclet.
43: * @param goal the TacletGoalTemplate specifying all the changes to be made
44: * to achieve one of the resulting goals
45: */
46: public void addTacletGoalTemplate(TacletGoalTemplate goal) {
47: goals = goals.prepend(goal);
48: }
49:
50: /**
51: * checks that a variableSV occurrs at most once in a quantifier of the
52: * ifs and finds and throws an exception otherwise
53: */
54: protected void checkBoundInIfAndFind() {
55: final BoundUniquenessChecker ch = new BoundUniquenessChecker(
56: ifSequent());
57: if (!ch.correct()) {
58: throw new TacletBuilderException(this ,
59: "A bound SchemaVariable occurs twice in if.");
60: }
61: }
62:
63: /**
64: * builds and returns the Taclet that is specified by
65: * former set... / add... methods. If no name is specified then
66: * an Taclet with an empty string name is build. No specifications
67: * for variable conditions, goals or heuristics imply that the
68: * corresponding parts of the Taclet are empty. No specification for
69: * the if-sequent is represented as a sequent with two empty
70: * semisequences. No specification for the interactive or
71: * recursive flags imply that the flags are not set. May throw an
72: * TacletBuilderException if a bound SchemaVariable occurs more than once in if
73: * and find.
74: */
75: public Taclet getTaclet() {
76: checkBoundInIfAndFind();
77: return getNoFindTaclet();
78: }
79: }
|