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.ArrayOfKeYJavaType;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.java.annotation.Annotation;
019: import de.uka.ilkd.key.java.statement.JumpStatement;
020: import de.uka.ilkd.key.java.visitor.Visitor;
021: import de.uka.ilkd.key.logic.ProgramElementName;
022: import de.uka.ilkd.key.logic.op.ArrayOfIProgramVariable;
023: import de.uka.ilkd.key.logic.op.SchemaVariable;
024:
025: /**
026: * This class represents statement and expression skolem symbols, which can be
027: * used within programs. Instances of (the subclasses of) this class can be
028: * used as operator together with the class <code>ProgramSVProxy</code>
029: */
030: public abstract class ProgramSVSkolem implements StateDependingObject,
031: NonTerminalProgramElement {
032:
033: private final ProgramElementName name;
034:
035: private final ArrayOfKeYJavaType influencingPVTypes;
036: private final int jumpCnt;
037:
038: /**
039: * @param p_name The name of the symbol
040: * @param p_influencingPVTypes An array of the types of the program variable
041: * arguments
042: * @param p_jumpCnt the size of the jump table
043: */
044: public ProgramSVSkolem(ProgramElementName p_name,
045: ArrayOfKeYJavaType p_influencingPVTypes, int p_jumpCnt) {
046: name = p_name;
047: influencingPVTypes = p_influencingPVTypes;
048: jumpCnt = p_jumpCnt;
049: }
050:
051: public ArrayOfKeYJavaType getInfluencingPVTypes() {
052: return influencingPVTypes;
053: }
054:
055: public int getJumpCount() {
056: return jumpCnt;
057: }
058:
059: public boolean checkJumpTable(ArrayOfStatement p_jumpTable) {
060: if (getJumpCount() != p_jumpTable.size())
061: return false;
062:
063: int i = getJumpCount();
064: while (i-- != 0) {
065: if (!(p_jumpTable.getStatement(i) instanceof SchemaVariable || p_jumpTable
066: .getStatement(i) instanceof JumpStatement))
067: return false;
068: }
069:
070: return true;
071: }
072:
073: public boolean checkInfluencingPVs(
074: ArrayOfIProgramVariable p_influencingPVs) {
075: if (getInfluencingPVTypes().size() != p_influencingPVs.size())
076: return false;
077:
078: int i;
079: for (i = 0; i != p_influencingPVs.size(); ++i) {
080: if (!(p_influencingPVs.getIProgramVariable(i) instanceof SchemaVariable || p_influencingPVs
081: .getIProgramVariable(i).getKeYJavaType() == getInfluencingPVTypes()
082: .getKeYJavaType(i)))
083: return false;
084: }
085:
086: return true;
087: }
088:
089: public ProgramElementName getProgramElementName() {
090: return name;
091: }
092:
093: /**
094: * Returns the number of children of this node.
095: * @return an int giving the number of children of this node
096: */
097: public int getChildCount() {
098: return 1;
099: }
100:
101: /**
102: * Returns the child at the specified index in this node's "virtual"
103: * child array.
104: * @param index an index into this node's "virtual" child array
105: * @return the program element at the given position
106: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
107: * of bounds
108: */
109: public ProgramElement getChildAt(int index) {
110: return getProgramElementName();
111: }
112:
113: /**
114: *Get comments.
115: *@return the comments.
116: */
117: public Comment[] getComments() {
118: return new Comment[0];
119: }
120:
121: public KeYJavaType getKeYJavaType() {
122: return null;
123: }
124:
125: /**
126: * Finds the source element that occurs first in the source.
127: * @return the first source element in the syntactical representation of
128: * this element, may be equals to this element.
129: * @see #toSource()
130: * @see #getStartPosition()
131: */
132: public SourceElement getFirstElement() {
133: return this ;
134: }
135:
136: /**
137: * Finds the source element that occurs last in the source.
138: * @return the last source element in the syntactical representation of
139: * this element, may be equals to this element.
140: * @see #toSource()
141: * @see #getEndPosition()
142: */
143: public SourceElement getLastElement() {
144: return this ;
145: }
146:
147: /**
148: Returns the start position of the primary token of this element.
149: To get the start position of the syntactical first token,
150: call the corresponding method of <CODE>getFirstElement()</CODE>.
151: @return the start position of the primary token.
152: */
153: public Position getStartPosition() {
154: return Position.UNDEFINED;
155: }
156:
157: /**
158: Returns the end position of the primary token of this element.
159: To get the end position of the syntactical first token,
160: call the corresponding method of <CODE>getLastElement()</CODE>.
161: @return the end position of the primary token.
162: */
163: public Position getEndPosition() {
164: return Position.UNDEFINED;
165: }
166:
167: /**
168: Returns the relative position (number of blank heading lines and
169: columns) of the primary token of this element.
170: To get the relative position of the syntactical first token,
171: call the corresponding method of <CODE>getFirstElement()</CODE>.
172: @return the relative position of the primary token.
173: */
174: public Position getRelativePosition() {
175: return Position.UNDEFINED;
176: }
177:
178: /** calls the corresponding method of a visitor in order to
179: * perform some action/transformation on this element
180: * @param v the Visitor
181: */
182: public void visit(Visitor v) {
183: v.performActionOnProgramSVSkolem(this );
184: }
185:
186: /**
187: * Pretty print.
188: * @param w a pretty printer.
189: * @exception IOException occasionally thrown.
190: */
191: public void prettyPrint(PrettyPrinter w) throws java.io.IOException {
192: w.printProgramElementName(getProgramElementName());
193: }
194:
195: /**
196: * This method returns true if two program parts are equal modulo
197: * renaming. The equality is mainly a syntactical equality with
198: * some exceptions: if a variable is declared we abstract from the
199: * name of the variable, so the first declared variable gets
200: * e.g. the name decl_1, the second declared decl_2 and so on.
201: * Look at the following programs:
202: * {int i; i=0;} and { int j; j=0;} these would be seen like
203: * {int decl_1; decl_1=0;} and {int decl_1; decl_1=0;} which are
204: * syntactical equal and therefore true is returned (same thing for
205: * labels). But {int i; i=0;} and {int j; i=0;} (in the second
206: * block the variable i is declared somewhere outside)
207: * would be seen as {int decl_1; decl_1=0;} for the first one but
208: * {int decl_1; i=0;} for the second one. These are not
209: * syntactical equal, therefore false is returned.
210: */
211: public boolean equalsModRenaming(SourceElement se,
212: NameAbstractionTable nat) {
213: return this == se;
214: }
215:
216: /**
217: *@return the annotations.
218: */
219: public Annotation[] getAnnotations() {
220: return new Annotation[0];
221: }
222:
223: public int getAnnotationCount() {
224: return 0;
225: }
226:
227: }
|