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.java;
12:
13: import de.uka.ilkd.key.java.reference.PackageReference;
14: import de.uka.ilkd.key.java.reference.PackageReferenceContainer;
15: import de.uka.ilkd.key.java.visitor.Visitor;
16: import de.uka.ilkd.key.util.ExtList;
17:
18: /**
19: * Package specification.
20: * taken from COMPOST and changed to achieve an immutable structure
21: */
22:
23: public class PackageSpecification extends JavaNonTerminalProgramElement
24: implements PackageReferenceContainer {
25:
26: /**
27: * Reference.
28: */
29:
30: protected final PackageReference reference;
31:
32: /**
33: * Package specification.
34: * @param children an ExtList with children
35: */
36:
37: public PackageSpecification(ExtList children) {
38: super (children);
39: reference = (PackageReference) children
40: .get(PackageReference.class);
41: }
42:
43: public SourceElement getLastElement() {
44: return reference;
45: }
46:
47: /**
48: * Returns the number of children of this node.
49: * @return an int giving the number of children of this node
50: */
51:
52: public int getChildCount() {
53: int result = 0;
54: if (reference != null)
55: result++;
56: return result;
57: }
58:
59: /**
60: * Returns the child at the specified index in this node's "virtual"
61: * child array
62: * @param index an index into this node's "virtual" child array
63: * @return the program element at the given position
64: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
65: * of bounds
66: */
67:
68: public ProgramElement getChildAt(int index) {
69: if (reference != null) {
70: if (index == 0)
71: return reference;
72: index--;
73: }
74: throw new ArrayIndexOutOfBoundsException();
75: }
76:
77: /**
78: * Get package reference.
79: * @return the package reference.
80: */
81:
82: public PackageReference getPackageReference() {
83: return reference;
84: }
85:
86: /** calls the corresponding method of a visitor in order to
87: * perform some action/transformation on this element
88: * @param v the Visitor
89: */
90: public void visit(Visitor v) {
91: v.performActionOnPackageSpecification(this );
92: }
93:
94: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
95: p.printPackageSpecification(this);
96: }
97: }
|