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.rule.soundness;
012:
013: import java.io.IOException;
014:
015: import de.uka.ilkd.key.java.*;
016: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
017: import de.uka.ilkd.key.java.annotation.Annotation;
018: import de.uka.ilkd.key.java.reference.ExecutionContext;
019: import de.uka.ilkd.key.java.visitor.Visitor;
020: import de.uka.ilkd.key.logic.op.ArrayOfIProgramVariable;
021: import de.uka.ilkd.key.logic.op.IProgramVariable;
022: import de.uka.ilkd.key.rule.MatchConditions;
023: import de.uka.ilkd.key.util.ExtList;
024:
025: /**
026: * This class is used to represent atomic statements and expressions. Instances
027: * of this class have no identity themselves, but they are instead provided an
028: * instance of the class <code>ProgramSVSkolem</code> as operator symbol. The
029: * relationship between <code>ProgramSVSkolem</code> and
030: * <code>ProgramSVProxy</code> is similar to the relationship between
031: * <code>Operator</code> and <code>Term</code>
032: */
033: public class ProgramSVProxy implements NonTerminalProgramElement,
034: Statement, Expression {
035:
036: private final ProgramSVSkolem op;
037:
038: private final ArrayOfIProgramVariable influencingPVs;
039: private final ArrayOfStatement jumpTable;
040:
041: public ProgramSVProxy(ProgramSVSkolem p_op,
042: ArrayOfIProgramVariable p_influencingPVs,
043: ArrayOfStatement p_jumpTable) {
044: op = p_op;
045: influencingPVs = p_influencingPVs;
046: jumpTable = p_jumpTable;
047:
048: if (!op.checkInfluencingPVs(influencingPVs))
049: throw new IllegalArgumentException(
050: "Illegal program variables given as children");
051: if (!op.checkJumpTable(jumpTable))
052: throw new IllegalArgumentException(
053: "Illegal jump table given");
054: }
055:
056: public ProgramSVProxy(ExtList p_children) {
057: this ((ProgramSVSkolem) p_children.get(ProgramSVSkolem.class),
058: new ArrayOfIProgramVariable(
059: (IProgramVariable[]) p_children
060: .collect(IProgramVariable.class)),
061: new ArrayOfStatement((Statement[]) p_children
062: .collect(Statement.class)));
063: }
064:
065: public ProgramSVSkolem op() {
066: return op;
067: }
068:
069: public ArrayOfIProgramVariable getInfluencingPVs() {
070: return influencingPVs;
071: }
072:
073: public ArrayOfStatement getJumpTable() {
074: return jumpTable;
075: }
076:
077: /**
078: * Returns the number of children of this node.
079: * @return an int giving the number of children of this node
080: */
081: public int getChildCount() {
082: return 1 + influencingPVs.size() + jumpTable.size();
083: }
084:
085: /**
086: * Returns the child at the specified index in this node's "virtual"
087: * child array.
088: * @param index an index into this node's "virtual" child array
089: * @return the program element at the given position
090: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
091: * of bounds
092: */
093: public ProgramElement getChildAt(int index) {
094: if (index == 0)
095: return op;
096: else if (index <= influencingPVs.size())
097: return influencingPVs.getIProgramVariable(index - 1);
098: return jumpTable
099: .getStatement(index - 1 - influencingPVs.size());
100: }
101:
102: /**
103: *Get comments.
104: *@return the comments.
105: */
106: public Comment[] getComments() {
107: return new Comment[0];
108: }
109:
110: public KeYJavaType getKeYJavaType() {
111: return op().getKeYJavaType();
112: }
113:
114: public KeYJavaType getKeYJavaType(Services javaServ) {
115: return getKeYJavaType();
116: }
117:
118: public KeYJavaType getKeYJavaType(Services javaServ,
119: ExecutionContext ec) {
120: return getKeYJavaType();
121: }
122:
123: /**
124: * Finds the source element that occurs first in the source.
125: * @return the first source element in the syntactical representation of
126: * this element, may be equals to this element.
127: * @see #toSource()
128: * @see #getStartPosition()
129: */
130: public SourceElement getFirstElement() {
131: return this ;
132: }
133:
134: /**
135: * Finds the source element that occurs last in the source.
136: * @return the last source element in the syntactical representation of
137: * this element, may be equals to this element.
138: * @see #toSource()
139: * @see #getEndPosition()
140: */
141: public SourceElement getLastElement() {
142: return this ;
143: }
144:
145: /**
146: Returns the start position of the primary token of this element.
147: To get the start position of the syntactical first token,
148: call the corresponding method of <CODE>getFirstElement()</CODE>.
149: @return the start position of the primary token.
150: */
151: public Position getStartPosition() {
152: return Position.UNDEFINED;
153: }
154:
155: /**
156: Returns the end position of the primary token of this element.
157: To get the end position of the syntactical first token,
158: call the corresponding method of <CODE>getLastElement()</CODE>.
159: @return the end position of the primary token.
160: */
161: public Position getEndPosition() {
162: return Position.UNDEFINED;
163: }
164:
165: /**
166: Returns the relative position (number of blank heading lines and
167: columns) of the primary token of this element.
168: To get the relative position of the syntactical first token,
169: call the corresponding method of <CODE>getFirstElement()</CODE>.
170: @return the relative position of the primary token.
171: */
172: public Position getRelativePosition() {
173: return Position.UNDEFINED;
174: }
175:
176: /** calls the corresponding method of a visitor in order to
177: * perform some action/transformation on this element
178: * @param v the Visitor
179: */
180: public void visit(Visitor v) {
181: v.performActionOnProgramSVProxy(this );
182: }
183:
184: /**
185: * Pretty print.
186: * @param w a pretty printer.
187: * @exception IOException occasionally thrown.
188: */
189: public void prettyPrint(PrettyPrinter w) throws java.io.IOException {
190: w.printProgramSVProxy(this );
191: }
192:
193: /**
194: * This method returns true if two program parts are equal modulo
195: * renaming. The equality is mainly a syntactical equality with
196: * some exceptions: if a variable is declared we abstract from the
197: * name of the variable, so the first declared variable gets
198: * e.g. the name decl_1, the second declared decl_2 and so on.
199: * Look at the following programs:
200: * {int i; i=0;} and { int j; j=0;} these would be seen like
201: * {int decl_1; decl_1=0;} and {int decl_1; decl_1=0;} which are
202: * syntactical equal and therefore true is returned (same thing for
203: * labels). But {int i; i=0;} and {int j; i=0;} (in the second
204: * block the variable i is declared somewhere outside)
205: * would be seen as {int decl_1; decl_1=0;} for the first one but
206: * {int decl_1; i=0;} for the second one. These are not
207: * syntactical equal, therefore false is returned.
208: */
209: public boolean equalsModRenaming(SourceElement se,
210: NameAbstractionTable nat) {
211: if (this .getClass() != se.getClass()) {
212: return false;
213: }
214: if (((NonTerminalProgramElement) se).getChildCount() != getChildCount()) {
215: return false;
216: }
217: for (int i = 0; i < getChildCount(); i++) {
218: if (!(getChildAt(i))
219: .equalsModRenaming(((NonTerminalProgramElement) se)
220: .getChildAt(i), nat)) {
221: return false;
222: }
223: }
224: return true;
225: }
226:
227: /** @return String representation of the constraint */
228: public String toString() {
229: String res = "" + op().getProgramElementName() + "( ";
230: int i;
231: for (i = 0; i != getChildCount(); ++i) {
232: res += getChildAt(i);
233: if (i < getChildCount() - 1)
234: res += ", ";
235: }
236: return res + " )";
237: }
238:
239: public PositionInfo getPositionInfo() {
240: return PositionInfo.UNDEFINED;
241: }
242:
243: /**
244: *@return the annotations.
245: */
246: public Annotation[] getAnnotations() {
247: return new Annotation[0];
248: }
249:
250: public int getAnnotationCount() {
251: return 0;
252: }
253:
254: public MatchConditions match(SourceData source,
255: MatchConditions matchCond) {
256: // TODO Auto-generated method stub
257: return null;
258: }
259: }
|