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.java.NameAbstractionTable;
14: import de.uka.ilkd.key.java.SourceElement;
15: import de.uka.ilkd.key.logic.Term;
16:
17: public interface SchemaVariable extends Operator {
18:
19: /**
20: * this method tests on object identity
21: */
22: boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat);
23:
24: Class matchType();
25:
26: /** returns true iff this SchemaVariable is used to match
27: * bound (quantifiable) variables
28: * @return true iff this SchemaVariable is used to match
29: * bound (quantifiable) variables
30: */
31:
32: boolean isVariableSV();
33:
34: /** returns true iff this SchemaVariable is used to match
35: * a term but not a formula
36: * @return true iff this SchemaVariable is used to match
37: * a term but not a formula
38: */
39: boolean isTermSV();
40:
41: /** returns true iff this SchemaVariable is used to match
42: * a formula
43: * @return true iff this SchemaVariable is used to match
44: * a formula
45: */
46: boolean isFormulaSV();
47:
48: /** returns true iff this SchemaVariable is used to match
49: * a part of a program
50: * @return true iff this SchemaVariable is used to match
51: * a part of a program
52: */
53: boolean isProgramSV();
54:
55: /**
56: * returns true if the schemavariable can match a list of syntactical
57: * elements
58: * @return true if the schemavariable can match a list of syntactical
59: * elements
60: */
61: boolean isListSV();
62:
63: /**
64: * @return true iff this SchemaVariable is used to match
65: * modal operators
66: */
67: boolean isOperatorSV();
68:
69: /** returns true iff this SchemaVariable is used to match (create)
70: * a skolem term
71: * @return true iff this SchemaVariable is used to match (create)
72: * a skolem term
73: */
74: boolean isSkolemTermSV();
75:
76: /** returns true iff this SchemaVariable is used to store a name
77: * (e.g. of taclets or metavariables).
78: * This SV is never matched against anything in the sequent.
79: */
80: boolean isNameSV();
81:
82: /** @return arity of the Variable as int */
83: int arity();
84:
85: /**
86: * @return true if the value of "term" having this operator as
87: * top-level operator and may not be changed by modalities
88: */
89: boolean isRigid(Term term);
90:
91: /**
92: */
93: boolean isRigid();
94:
95: }
|