001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010:
011: package de.uka.ilkd.key.java.declaration;
012:
013: import java.util.LinkedList;
014:
015: import de.uka.ilkd.key.java.Comment;
016: import de.uka.ilkd.key.java.PrettyPrinter;
017: import de.uka.ilkd.key.java.ProgramElement;
018: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
019: import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
020: import de.uka.ilkd.key.java.visitor.Visitor;
021: import de.uka.ilkd.key.jml.UsefulTools;
022: import de.uka.ilkd.key.logic.ProgramElementName;
023: import de.uka.ilkd.key.util.ExtList;
024:
025: /**
026: * Interface declaration.
027: *
028: */
029:
030: public class InterfaceDeclaration extends TypeDeclaration {
031:
032: /**
033: * Extending.
034: */
035:
036: protected final Extends extending;
037:
038: /**
039: * Interface declaration.
040: */
041:
042: public InterfaceDeclaration() {
043: extending = null;
044: }
045:
046: /** Construct a new outer or member interface class. */
047: public InterfaceDeclaration(Modifier[] modifiers,
048: ProgramElementName name, ProgramElementName fullName,
049: Extends extended, MemberDeclaration[] members,
050: boolean isLibrary) {
051: super (modifiers, name, fullName, members, false, isLibrary);
052: extending = extended;
053: }
054:
055: /** Construct a new outer or member interface class. */
056: public InterfaceDeclaration(Modifier[] modifiers,
057: ProgramElementName name, Extends extended,
058: MemberDeclaration[] members, boolean isLibrary) {
059: this (modifiers, name, name, extended, members, isLibrary);
060: }
061:
062: /**
063: * uses children list to create non-anonymous class
064: * @param children an ExtList that may contain: an Extends
065: * (as pointer to a class), ProgramElementName (as name),
066: * several MemberDeclaration (as members of
067: * the type), a parentIsInterfaceDeclaration (indicating if parent is
068: * interface), several Modifier (as modifiers of the type decl), a Comment
069: * @param fullName the fully qualified ProgramElementName of the declared
070: * type
071: * @param isLibrary a boolean flag indicating if this interface is part of
072: * a library (library interfaces come often with a specification and are
073: * only available as bytecode)
074: */
075: public InterfaceDeclaration(ExtList children,
076: ProgramElementName fullName, boolean isLibrary) {
077: super (children, fullName, isLibrary);
078: extending = (Extends) children.get(Extends.class);
079: }
080:
081: public InterfaceDeclaration(ProgramElementName name) {
082: this (
083: new de.uka.ilkd.key.java.declaration.Modifier[] {},
084: name,
085: null,
086: new de.uka.ilkd.key.java.declaration.MemberDeclaration[] {},
087: true);
088: }
089:
090: /**
091: * Returns the number of children of this node.
092: * @return an int giving the number of children of this node
093: */
094: public int getChildCount() {
095: int result = 0;
096: if (modArray != null)
097: result += modArray.size();
098: if (name != null)
099: result++;
100: if (extending != null)
101: result++;
102: if (members != null)
103: result += members.size();
104: return result;
105: }
106:
107: /**
108: * Returns the child at the specified index in this node's "virtual"
109: * child array
110: * @param index an index into this node's "virtual" child array
111: * @return the program element at the given position
112: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
113: * of bounds
114: */
115: public ProgramElement getChildAt(int index) {
116: int len;
117: if (modArray != null) {
118: len = modArray.size();
119: if (len > index) {
120: return modArray.getModifier(index);
121: }
122: index -= len;
123: }
124: if (name != null) {
125: if (index == 0)
126: return name;
127: index--;
128: }
129: if (extending != null) {
130: if (index == 0)
131: return extending;
132: index--;
133: }
134: if (members != null) {
135: len = members.size();
136: if (len > index) {
137: return members.getMemberDeclaration(index);
138: }
139: index -= len;
140: }
141: throw new ArrayIndexOutOfBoundsException();
142: }
143:
144: /**
145: * Get extended types.
146: * @return the extends.
147: */
148:
149: public Extends getExtendedTypes() {
150: return extending;
151: }
152:
153: /**
154: * Interfaces are always abstract.
155: */
156: public boolean isAbstract() {
157: return true;
158: }
159:
160: /**
161: * Interfaces are never native.
162: */
163: public boolean isNative() {
164: return false;
165: }
166:
167: /**
168: * Interfaces are never protected.
169: */
170: public boolean isProtected() {
171: return false;
172: }
173:
174: /**
175: * Interfaces are never private.
176: */
177: public boolean isPrivate() {
178: return false;
179: }
180:
181: /**
182: * Interfaces are never strictfp.
183: */
184:
185: public boolean isStrictFp() {
186: return false;
187: }
188:
189: /**
190: * Interfaces are never synchronized.
191: */
192: public boolean isSynchronized() {
193: return false;
194: }
195:
196: /**
197: * Interfaces are never transient.
198: */
199: public boolean isTransient() {
200: return false;
201: }
202:
203: /**
204: * Interfaces are never volatile.
205: */
206: public boolean isVolatile() {
207: return false;
208: }
209:
210: public boolean isInterface() {
211: return true;
212: }
213:
214: /**
215: * returns the local declared supertypes
216: */
217: public ListOfKeYJavaType getSupertypes() {
218: ListOfKeYJavaType types = SLListOfKeYJavaType.EMPTY_LIST;
219: if (extending != null) {
220: for (int i = extending.getTypeReferenceCount() - 1; i >= 0; i--) {
221: types = types.prepend(extending.getTypeReferenceAt(i)
222: .getKeYJavaType());
223: }
224: }
225: return types;
226: }
227:
228: /** calls the corresponding method of a visitor in order to
229: * perform some action/transformation on this element
230: * @param v the Visitor
231: */
232: public void visit(Visitor v) {
233: v.performActionOnInterfaceDeclaration(this );
234: }
235:
236: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
237: p.printInterfaceDeclaration(this );
238: }
239:
240: /**
241: * returns the comments belonging to this InterfaceDeclaration + Comments
242: * declared in the body of the class that contain jml invariant or
243: * constraint statements.
244: * @return the comments.
245: */
246: public Comment[] getComments() {
247: Comment[] c1 = super .getComments();
248: LinkedList jmlComments = new LinkedList();
249: //HACK: RECODER interprets comments, that are intended to be refering
250: // to the interface, as comments belonging to fields or methods.
251: for (int i = 0; i < getChildCount(); i++) {
252: final ProgramElement p = getChildAt(i);
253: final Comment[] c2 = p.getComments();
254: if (c2 != null) {
255: for (int j = 0; j < c2.length; j++) {
256: if (UsefulTools.isClassSpec(c2[j])
257: || (p instanceof Modifier)) {
258: jmlComments.add(c2[j]);
259: }
260: }
261: }
262: }
263: final Comment[] c2 = new Comment[c1.length + jmlComments.size()];
264: System.arraycopy(c1, 0, c2, 0, c1.length);
265: for (int i = c1.length; i < c2.length; i++) {
266: c2[i] = (Comment) jmlComments.removeFirst();
267: }
268: return c2;
269: }
270: }
|