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.metaconstruct;
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.expression.operator.CopyAssignment;
018: import de.uka.ilkd.key.java.reference.*;
019: import de.uka.ilkd.key.java.visitor.Visitor;
020: import de.uka.ilkd.key.logic.Name;
021: import de.uka.ilkd.key.logic.ProgramElementName;
022: import de.uka.ilkd.key.logic.op.ProgramVariable;
023: import de.uka.ilkd.key.rule.inst.SVInstantiations;
024:
025: /**
026: * Program meta constructs are used for schematic transformations that
027: * cannot be expressed in form of schematic formulas of taclets. For
028: * example:
029: * <ol>
030: * <li> transformations needing access to the java (type) model, e.g
031: * dynamic dispatch of program methods </li>
032: * <li> complex transformations that are hard (or not) to express via
033: * taclets, for example unwinding a loop (together with replacing
034: * continues or unlabeled breaks with a labeled break)</li>
035: * </ol>
036: * (Program)MetaConstructs should be used with care as they make it hard to
037: * validate (verify) rules and import nearly the complete power of Java into
038: * taclets.
039: */
040: public abstract class ProgramMetaConstruct extends
041: JavaNonTerminalProgramElement implements StatementContainer,
042: Statement, Expression, TypeReference {
043:
044: /** the name of the meta construct */
045: private Name name;
046: /** the encapsulated program element */
047: private ProgramElement body;
048:
049: /** creates a ProgramMetaConstruct
050: * @param name the Name of the meta construct
051: * @param body the ProgramElement contained by the meta construct
052: */
053: public ProgramMetaConstruct(Name name, ProgramElement body) {
054: this .name = name;
055: this .body = body;
056: }
057:
058: /** creates a ProgramMetaConstruct
059: * @param name the String with the name of the meta construct
060: * @param body the ProgramElement contained by the meta construct
061: */
062: public ProgramMetaConstruct(String name, ProgramElement body) {
063: this (new Name(name), body);
064: }
065:
066: /** performs the program transformation needed for symbolic
067: * program transformation
068: * @param pe the ProgramElement on which the execution is performed
069: * @param services the Services with all necessary information
070: * about the java programs
071: * @param svInst the instantiations of the schemavariables
072: * @return the transformated program
073: */
074: public abstract ProgramElement symbolicExecution(ProgramElement pe,
075: Services services, SVInstantiations svInst);
076:
077: /** returns the name of the meta construct
078: * @return the name of the meta construct
079: */
080: public Name name() {
081: return name;
082: }
083:
084: /** returns the body of the meta construct
085: * @return the body of the meta construct
086: */
087: public ProgramElement body() {
088: return body;
089: }
090:
091: /**
092: * Finds the source element that occurs last in the source.
093: * @return the last source element in the syntactical representation of
094: * this element, may be equals to this element.
095: */
096: public SourceElement getLastElement() {
097: return (body != null) ? body : (SourceElement) this ;
098: }
099:
100: /**
101: * Get the number of statements in this container.
102: * @return the number of statements.
103: */
104: public int getStatementCount() {
105: return (body instanceof Statement ? 1 : 0);
106: }
107:
108: /*
109: * Return the statement at the specified index in this node's
110: * "virtual" statement array.
111: * @param index an index for a statement.
112: * @return the statement with the given index.
113: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
114: * of bounds.
115: */
116: public Statement getStatementAt(int index) {
117: if (index == 0 && body instanceof Statement) {
118: return (Statement) body;
119: } else if (!(body instanceof Statement)) {
120: return null;
121: } else {
122: throw new ArrayIndexOutOfBoundsException(
123: "A ProgramMetaConstruct contains only one statement ");
124: }
125: }
126:
127: /**
128: * Returns the number of children of this node.
129: * @return an int giving the number of children of this node
130: */
131: public int getChildCount() {
132: return 1;
133: }
134:
135: /**
136: * Returns the child at the specified index in this node's "virtual"
137: * child array.
138: * @param index an index into this node's "virtual" child array
139: * @return the program element at the given position
140: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
141: * of bounds
142: */
143: public ProgramElement getChildAt(int index) {
144: return body;
145: }
146:
147: //-------------some methods to pretend being a type reference --------
148:
149: public ReferencePrefix getReferencePrefix() {
150: return null;
151: }
152:
153: public ReferencePrefix setReferencePrefix(ReferencePrefix r) {
154: return this ;
155: }
156:
157: public int getDimensions() {
158: return 0;
159: }
160:
161: public int getTypeReferenceCount() {
162: return 0;
163: }
164:
165: public TypeReference getTypeReferenceAt(int index) {
166: return this ;
167: }
168:
169: public PackageReference getPackageReference() {
170: return null;
171: }
172:
173: public int getExpressionCount() {
174: return 0;
175: }
176:
177: public Expression getExpressionAt(int index) {
178: return null;
179: }
180:
181: public ProgramElementName getProgramElementName() {
182: return new ProgramElementName(toString());
183: }
184:
185: public String getName() {
186: return toString();
187: }
188:
189: /** calls the corresponding method of a visitor in order to
190: * perform some action/transformation on this element
191: * @param v the Visitor
192: */
193: public void visit(Visitor v) {
194: v.performActionOnProgramMetaConstruct(this );
195: }
196:
197: public void prettyPrint(PrettyPrinter p) throws IOException {
198: p.printProgramMetaConstruct(this );
199: }
200:
201: /** to String */
202: public String toString() {
203: return name + "( " + body + ");";
204: }
205:
206: public KeYJavaType getKeYJavaType() {
207: return null;
208: }
209:
210: public KeYJavaType getKeYJavaType(Services javaServ) {
211: return getKeYJavaType();
212: }
213:
214: public KeYJavaType getKeYJavaType(Services javaServ,
215: ExecutionContext ec) {
216: return getKeYJavaType();
217: }
218:
219: // helpers
220:
221: /**
222: * creates an assignment <code> lhs:=rhs </code>
223: */
224: protected final Statement assign(Expression lhs, Expression rhs) {
225: return new CopyAssignment(lhs, rhs);
226: }
227:
228: /**
229: * creates an attribute access
230: */
231: protected final Expression attribute(ReferencePrefix prefix,
232: ProgramVariable field) {
233: return new FieldReference(field, prefix);
234: }
235:
236: }
|