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.java.ArrayOfProgramElement;
13: import de.uka.ilkd.key.logic.op.SchemaVariable;
14:
15: /** This class is used to store the instantiation of a schemavarible
16: * if it is a ProgramElement.
17: */
18:
19: public class ProgramListInstantiation extends InstantiationEntry {
20:
21: /** the pe the schemavariable is instantiated with */
22: private final ArrayOfProgramElement pes;
23:
24: /** creates a new ContextInstantiationEntry
25: * @param sv the SchemaVariable that is
26: * instantiated
27: * @param pes the ProgramElement array the
28: * SchemaVariable is instantiated with
29: */
30: ProgramListInstantiation(SchemaVariable sv,
31: ArrayOfProgramElement pes) {
32: super (sv);
33: this .pes = pes;
34: }
35:
36: /** returns the ProgramElement the SchemaVariable is instantiated with
37: * @return the ProgramElement the SchemaVariable is instantiated with
38: */
39: public ArrayOfProgramElement getProgramElements() {
40: return pes;
41: }
42:
43: /** returns the intantiation of the SchemaVariable
44: * @return the intantiation of the SchemaVariable
45: */
46: public Object getInstantiation() {
47: return pes;
48: }
49:
50: /** toString */
51: public String toString() {
52: return "[" + getSchemaVariable() + ", " + getProgramElements()
53: + "]";
54: }
55:
56: }
|