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;
012:
013: import java.io.IOException;
014:
015: import de.uka.ilkd.key.java.visitor.Visitor;
016: import de.uka.ilkd.key.logic.op.SVSubstitute;
017:
018: /**
019: * A source element is a piece of syntax. It does not necessarily have
020: * a semantics, at least none that is machinable, for instance a
021: * {@link recoder.java.Comment}.
022: * taken from RECODER and changed to achieve an immutable structure
023: */
024:
025: public interface SourceElement extends SVSubstitute {
026:
027: /**
028: * Finds the source element that occurs first in the source.
029: * @return the first source element in the syntactical representation of
030: * this element, may be equals to this element.
031: * @see #getStartPosition()
032: */
033: SourceElement getFirstElement();
034:
035: /**
036: * Finds the source element that occurs last in the source.
037: * @return the last source element in the syntactical representation of
038: * this element, may be equals to this element.
039: * @see #getEndPosition()
040: */
041: SourceElement getLastElement();
042:
043: /**
044: Returns the start position of the primary token of this element.
045: To get the start position of the syntactical first token,
046: call the corresponding method of <CODE>getFirstElement()</CODE>.
047: @return the start position of the primary token.
048: */
049: Position getStartPosition();
050:
051: /**
052: Returns the end position of the primary token of this element.
053: To get the end position of the syntactical first token,
054: call the corresponding method of <CODE>getLastElement()</CODE>.
055: @return the end position of the primary token.
056: */
057: Position getEndPosition();
058:
059: /**
060: Returns the relative position (number of blank heading lines and
061: columns) of the primary token of this element.
062: To get the relative position of the syntactical first token,
063: call the corresponding method of <CODE>getFirstElement()</CODE>.
064: @return the relative position of the primary token.
065: */
066: Position getRelativePosition();
067:
068: /** complete position information */
069: PositionInfo getPositionInfo();
070:
071: /** calls the corresponding method of a visitor in order to
072: * perform some action/transformation on this element
073: * @param v the Visitor
074: */
075: void visit(Visitor v);
076:
077: /**
078: * Pretty print.
079: * @param w a pretty printer.
080: * @exception IOException occasionally thrown.
081: */
082: void prettyPrint(PrettyPrinter w) throws java.io.IOException;
083:
084: /**
085: * This method returns true if two program parts are equal modulo
086: * renaming. The equality is mainly a syntactical equality with
087: * some exceptions: if a variable is declared we abstract from the
088: * name of the variable, so the first declared variable gets
089: * e.g. the name decl_1, the second declared decl_2 and so on.
090: * Look at the following programs:
091: * {int i; i=0;} and { int j; j=0;} these would be seen like
092: * {int decl_1; decl_1=0;} and {int decl_1; decl_1=0;} which are
093: * syntactical equal and therefore true is returned (same thing for
094: * labels). But {int i; i=0;} and {int j; i=0;} (in the second
095: * block the variable i is declared somewhere outside)
096: * would be seen as {int decl_1; decl_1=0;} for the first one but
097: * {int decl_1; i=0;} for the second one. These are not
098: * syntactical equal, therefore false is returned.
099: */
100: boolean equalsModRenaming(SourceElement se, NameAbstractionTable nat);
101:
102: }
|