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.logic.op;
12:
13: import de.uka.ilkd.key.logic.Name;
14: import de.uka.ilkd.key.logic.sort.Sort;
15:
16: class FormulaSV extends AbstractTermSV {
17: /** creates a new SchemaVariable. That is used as placeholder for
18: * formulae.
19: * @param name the Name of the SchemaVariable
20: * @param rigidness true iff this SV may only match rigid
21: * terms/formulas
22: * @param listSV a boolean which is true iff the schemavariable is allowed
23: * to match a list of formulas
24: */
25: FormulaSV(Name name, boolean listSV, boolean rigidness) {
26: super (name, Sort.FORMULA, listSV, rigidness);
27: }
28:
29: /**
30: * returns true iff this SchemaVariable is used to match
31: * a formula
32: * @return true iff this SchemaVariable is used to match
33: * a formula
34: */
35: public boolean isFormulaSV() {
36: return true;
37: }
38:
39: /** toString */
40: public String toString() {
41: return toString("formula");
42: }
43: }
|