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.proof.mgt;
012:
013: import de.uka.ilkd.key.casetool.ModelClass;
014: import de.uka.ilkd.key.casetool.ModelMethod;
015: import de.uka.ilkd.key.java.Comment;
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.declaration.ConstructorDeclaration;
018: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
019: import de.uka.ilkd.key.logic.op.ProgramMethod;
020: import de.uka.ilkd.key.speclang.ListOfOperationContract;
021: import de.uka.ilkd.key.speclang.SLListOfOperationContract;
022:
023: public class JavaModelMethod implements ModelMethod, Contractable {
024:
025: private ProgramMethod method;
026: private String preCond = null;
027: private String postCond = null;
028: private String modifies = null;
029: private JavaModelClass contClass;
030:
031: public JavaModelMethod(ProgramMethod pm, String rootDir,
032: Services services) {
033: this .method = pm;
034: contClass = new JavaModelClass(pm.getContainerType(), rootDir,
035: services);
036: }
037:
038: public ModelClass getContainingClass() {
039: return contClass;
040: }
041:
042: public ProgramMethod getProgramMethod() {
043: return method;
044: }
045:
046: public String getContainingClassName() {
047: return method.getContainerType().getName();
048: }
049:
050: public String getContainingPackage() {
051: return contClass.getContainingPackage();
052: }
053:
054: // return signature of form name(arg1: type1; arg2: type2 ...)
055: // and translates Java types to OCL types
056: public String getCallSignature() {
057: return getCallSignature(true);
058: }
059:
060: public int getNumParameters() {
061: return 0;//%%%
062: }
063:
064: public String getParameterNameAt(int i) {
065: return "";//%%%
066: }
067:
068: public String getParameterTypeAt(int i) {
069: return "";//%%%
070: }
071:
072: public String getResultType() {
073: return "";//%%%
074: }
075:
076: private String toOCL(String s, boolean doit) {
077: if (!doit) {
078: return s;
079: } else {
080: return transformTypeJava2OCL(s);
081: }
082: }
083:
084: public static String transformTypeJava2OCL(String aJavaType) {
085: if ("int".equals(aJavaType) || "byte".equals(aJavaType)
086: || "char".equals(aJavaType)
087: || "short".equals(aJavaType)
088: || "long".equals(aJavaType)) {
089: return "Integer";
090: } else if ("boolean".equals(aJavaType)) {
091: return "Boolean";
092: } else if (aJavaType.endsWith("[]")) {
093: String base = transformTypeJava2OCL(aJavaType.substring(0,
094: aJavaType.length() - 2));
095: return "KeYArrayOf" + base;
096:
097: } else {
098: return aJavaType;
099: }
100: }
101:
102: // return signature of form name(arg1: type1; arg2: type2 ...)
103: public String getCallSignature(boolean translateJavaType2OCLTypes) {
104: StringBuffer res = new StringBuffer(getName() + "(");
105: MethodDeclaration md = method.getMethodDeclaration();
106: for (int i = 0; i < md.getParameterDeclarationCount(); i++) {
107: de.uka.ilkd.key.java.declaration.VariableSpecification vs = md
108: .getParameterDeclarationAt(i)
109: .getVariableSpecification();
110: res.append(vs.getName());
111: res.append(": ");
112: res.append(toOCL(vs.getType().getName(),
113: translateJavaType2OCLTypes));
114: if (i < md.getParameterDeclarationCount() - 1)
115: res.append("; ");
116: }
117: res.append(")");
118: if (md.getTypeReference() != null) {
119: res.append(":"
120: + toOCL(md.getTypeReference().getName(),
121: translateJavaType2OCLTypes));
122: }
123: return res.toString();
124: }
125:
126: public String getName() {
127: return method.getMethodDeclaration().getProgramElementName()
128: .toString();
129: }
130:
131: public boolean isVoid() {
132: return method.getMethodDeclaration().getTypeReference() == null;
133: }
134:
135: public boolean isConstructor() {
136: return (method.getMethodDeclaration() instanceof ConstructorDeclaration);
137: }
138:
139: public boolean isPrivate() {
140: return method.isPrivate();
141: }
142:
143: public String getTagContent(String keyword) {
144: String res = null;
145: MethodDeclaration md = method.getMethodDeclaration();
146: Comment[] comments = md.getComments();
147: for (int i = 0; comments != null && i < comments.length; i++) {
148: String s = comments[i].getText();
149: int start = s.indexOf(keyword);
150: if (start >= 0) {
151: int end = s.indexOf("@", start + 1);
152: int end2 = s.indexOf("\n", start + 1);
153: if (end2 >= 0 && end2 < end)
154: end = end2;
155: if (end < 0) {
156: end = s.length() - 2;
157: }
158: res = s.substring(start + keyword.length(), end);
159:
160: }
161: }
162: return res == null ? null : res.trim();
163: }
164:
165: // returns precondition if any, else ""
166: public String getMyPreCond() {
167: if (preCond == null) {
168: preCond = getTagContent("@preconditions");
169: if (preCond == null)
170: preCond = "";
171: }
172: return preCond;
173: }
174:
175: public String getMyModifClause() {
176: if (modifies == null) {
177: modifies = getTagContent("@modifies");
178: }
179: return modifies;
180: }
181:
182: /**
183: * returns true if <code>method</code> is a model method.
184: */
185: public boolean isModel() {
186: return method.isModel();
187: }
188:
189: // set modifies clause
190: public void setMyModifClause(String modifClause) {
191: modifies = modifClause;
192: }
193:
194: public boolean isQuery() {
195: return "".equals(getMyModifClause());
196: }
197:
198: // set precondition
199: public void setMyPreCond(String precond) {
200: preCond = precond;
201: }
202:
203: // returns precondition of parent if any, else ""
204: public String getParentPreCond() {
205: return "";//%%
206: }
207:
208: public ModelMethod getParentMethod() {
209: return null;//%%
210: }
211:
212: public String getMyPostCond() {
213: if (postCond == null) {
214: postCond = getTagContent("@postconditions");
215: if (postCond == null)
216: postCond = "";
217: }
218: return postCond;
219: }
220:
221: public void setMyPostCond(String postcond) {
222: postCond = postcond;
223: }
224:
225: public String getParentPostCond() {
226: return "";//%%
227: }
228:
229: // set/get GF abstract syntax representation of pre-/postconditions
230: public String getMyGFAbs() {
231: return "";//%%
232: }
233:
234: public void setMyGFAbs(String abs) {
235: return;//%%
236: }
237:
238: public boolean hasOrigParent() {
239: return false;//%%
240: }
241:
242: public String getActXmifile() {
243: return null;
244: }
245:
246: public String toString() {
247: return getContainingClass().getClassName() + "::"
248: + getCallSignature();
249: }
250:
251: public int hashCode() {
252: return getProgramMethod().hashCode() * 13
253: + getContainingClass().hashCode();
254: }
255:
256: public boolean equals(Object o) {
257: if (!(o instanceof JavaModelMethod)) {
258: return false;
259: }
260: JavaModelMethod jmm = (JavaModelMethod) o;
261: return getProgramMethod().equals(jmm.getProgramMethod())
262: && getContainingClass()
263: .equals(jmm.getContainingClass());
264: }
265:
266: public ListOfOperationContract getMyOperationContracts() {
267: return SLListOfOperationContract.EMPTY_LIST;//%%
268: }
269:
270: public boolean equalContractable(Contractable c) {
271: return equals(c);
272: }
273: }
|