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.Term;
15: import de.uka.ilkd.key.logic.sort.Sort;
16:
17: abstract class AbstractTermSV extends SortedSchemaVariable {
18:
19: private final boolean rigidness;
20:
21: /** creates a new SchemaVariable
22: * @param name the Name of the SchemaVariable
23: * @param sort the Sort of the SchemaVariable and the matched type
24: * @param rigidness true iff this SV may only match rigid
25: * terms/formulas
26: * @param listSV a boolean which is true iff the schemavariable is allowed
27: * to match a list of terms
28: * @param strictSV boolean indicating if the schemavariable is declared as strict
29: * forcing exact type match
30: */
31: AbstractTermSV(Name name, Sort sort, boolean listSV,
32: boolean rigidness) {
33: super (name, Term.class, sort, listSV);
34: this .rigidness = rigidness;
35: }
36:
37: /**
38: * @return true if the value of "term" having this operator as
39: * top-level operator and may not be changed by modalities
40: */
41: public boolean isRigid() {
42: return rigidness;
43: }
44: }
|