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: import de.uka.ilkd.key.logic.Term;
14:
15: /** Superclass of TacletBuilder objects that have a non-empty find clause.
16: * This should be all of them except NoFindTacletBuilder.
17: */
18:
19: public abstract class FindTacletBuilder extends TacletBuilder {
20:
21: protected Term find = null;
22:
23: /**
24: * checks that a SchemaVariable that is used to match pure variables
25: * (this means bound variables) occurs at most once in a quantifier of the
26: * ifs and finds and throws an exception otherwise
27: */
28: protected void checkBoundInIfAndFind() {
29: final BoundUniquenessChecker ch = new BoundUniquenessChecker(
30: getFind(), ifSequent());
31: if (!ch.correct()) {
32: throw new TacletBuilderException(this ,
33: "A bound SchemaVariable variables occurs twice "
34: + "in if and find.");
35: }
36: }
37:
38: /* Get the `find' term. This could be a term or a formula for a
39: * RewriteTaclet, but only a formula for an Antec/Succ Taclet.
40: */
41: public Term getFind() {
42: return find;
43: }
44:
45: }
|