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: import de.uka.ilkd.key.rule.ListOfObject;
14:
15: public class ListInstantiation extends InstantiationEntry {
16:
17: /** the pe the schemavariable is instantiated with */
18: private final ListOfObject list;
19:
20: /** creates a new ContextInstantiationEntry
21: * @param sv the SchemaVariable that is
22: * instantiated
23: * @param pes the List the
24: * SchemaVariable is instantiated with
25: */
26: ListInstantiation(SchemaVariable sv, ListOfObject pes) {
27: super (sv);
28: this .list = pes;
29: }
30:
31: /** returns the intantiation of the SchemaVariable
32: * @return the intantiation of the SchemaVariable
33: */
34: public Object getInstantiation() {
35: return list;
36: }
37:
38: /** returns the intantiation of the SchemaVariable
39: * @return the intantiation of the SchemaVariable
40: */
41: public ListOfObject getList() {
42: return list;
43: }
44:
45: /** toString */
46: public String toString() {
47: return "[" + getSchemaVariable() + ", " + getInstantiation()
48: + "]";
49: }
50:
51: }
|