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: package de.uka.ilkd.key.rule.inst;
11:
12: import de.uka.ilkd.key.logic.op.SchemaVariable;
13:
14: /** This is an abstract clas that encapsulates a schemvariable and its
15: * instantiation. It is needed because schemavariables can be
16: * instantiated as ProgramElements and as Terms accroding to their
17: * type. But we have to put the pair (schemavariable,
18: * term/programelment) in one map. Therefore a map from
19: * SchemaVariable to InstantiationEntry is used
20: */
21: public abstract class InstantiationEntry {
22:
23: /** the instantiated SchemaVariable */
24: private final SchemaVariable sv;
25:
26: /** creates a new InstantiationEntry with the given SchemaVariable
27: * @param sv the SchemaVariable that is instantiated
28: */
29: InstantiationEntry(SchemaVariable sv) {
30: this .sv = sv;
31: }
32:
33: /** returns the intantiation of the SchemaVariable
34: * @return the intantiation of the SchemaVariable
35: */
36: public abstract Object getInstantiation();
37:
38: /** returns the SchemaVariable that is instantiated
39: * @return the SchemaVariable that is instantiated
40: */
41: public SchemaVariable getSchemaVariable() {
42: return sv;
43: }
44: }
|