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.casetool.together;
012:
013: import java.util.Enumeration;
014: import java.util.Iterator;
015: import java.util.Vector;
016:
017: import com.togethersoft.openapi.rwi.*;
018:
019: import de.uka.ilkd.key.casetool.ModelClass;
020: import de.uka.ilkd.key.casetool.ModelMethod;
021: import de.uka.ilkd.key.casetool.UMLModelClass;
022: import de.uka.ilkd.key.logic.op.Op;
023: import de.uka.ilkd.key.proof.mgt.Contractable;
024: import de.uka.ilkd.key.proof.mgt.JavaModelMethod;
025: import de.uka.ilkd.key.speclang.*;
026: import de.uka.ilkd.key.speclang.ocl.OCLOperationContract;
027:
028: /** represents a method of the Together model. It is backed by the
029: * corresponding Together RWI model element, but it is independent in
030: * a sense that changing the together project allows to access all
031: * methods unless they are specifically marked.
032: */
033: public class TogetherModelMethod extends TogetherReprModel implements
034: ModelMethod {
035:
036: // which element of the model do I represent
037: private final RwiMember orig;
038: private RwiModel currRwiModel;
039: private RwiDiagram currRwiDiagram;
040:
041: private RwiMember origParent;
042: private boolean origParentAlreadySet = false;
043:
044: private boolean parameterListComputed = false;
045: private Vector paraNames = new Vector();
046: private Vector paraTypes = new Vector();
047:
048: private UMLModelClass containingClass;
049: private String retTypeString;
050: private String callSig;
051: private String callSigOCL;
052: private String callSigQualif; // package qualified call signature
053: private String callSigQualifOCL;
054: private String name;
055: private String precond;
056: private String postcond;
057: private String modifies;
058: private String stereotype;
059: private boolean constr;
060: private boolean priv;
061: private int hash = 0;
062:
063: public TogetherModelMethod(RwiMember theOrig, RwiModel model,
064: RwiDiagram diag) {
065: orig = theOrig;
066: currRwiModel = model;
067: currRwiDiagram = diag;
068: this .containingClass = createContainingClassRepr();
069: retTypeString = orig.getProperty(RwiProperty.RETURN_TYPE);
070: callSigOCL = createCallSignature(true);
071: callSig = createCallSignature(false);
072: callSigQualifOCL = createCallSignatureQualified(true);
073: callSigQualif = createCallSignatureQualified(false);
074: name = orig.getProperty(RwiProperty.NAME);
075: precond = orig.getProperty("preconditions");
076: postcond = orig.getProperty("postconditions");
077: modifies = orig.getProperty("modifies");
078: stereotype = orig.getProperty("stereotype");
079: constr = orig.getProperty(RwiProperty.CONSTRUCTOR) != null;
080: priv = orig.getProperty(RwiProperty.PRIVATE) != null;
081: }
082:
083: /** returns the together original object representing this
084: * method. Could be invalidated since a new project has been
085: * loaded.
086: */
087: public RwiMember getOrig() {
088: return orig;
089: }
090:
091: public UMLModelClass createContainingClassRepr() {
092: RwiNode localContainingClass = orig.getContainingNode();
093: return new TogetherModelClass(localContainingClass,
094: currRwiModel, currRwiDiagram);
095: }
096:
097: public ModelClass getContainingClass() {
098: return containingClass;
099: }
100:
101: public String getContainingPackage() {
102: return getContainingClass().getContainingPackage();
103: }
104:
105: public String getContainingClassName() {
106: return getContainingClass().getClassName();
107: }
108:
109: public boolean isVoid() {
110: return !isConstructor()
111: && (retTypeString == null || "void"
112: .equals(retTypeString));
113: }
114:
115: public int getNumParameters() {
116: if (!parameterListComputed)
117: getCallSignature();
118: return paraNames.size();
119: }
120:
121: public String getParameterNameAt(int i) {
122: if (!parameterListComputed)
123: getCallSignature();
124: return paraNames.elementAt(i).toString();
125: }
126:
127: public String getParameterTypeAt(int i) {
128: if (!parameterListComputed)
129: getCallSignature();
130: return paraTypes.elementAt(i).toString();
131: }
132:
133: public String getResultType() {
134: if (isConstructor()) {
135: return containingClass.getFullClassName();
136: } else {
137: String s = orig.getProperty(RwiProperty.RETURN_TYPE);
138: return (s.equals("void") ? null : s);
139: }
140: }
141:
142: public String getCallSignature() {
143: return getCallSignature(true);
144: }
145:
146: public String getCallSignature(boolean translateJavaType2OCLTypes) {
147: if (translateJavaType2OCLTypes) {
148: return callSigOCL;
149: } else {
150: return callSig;
151: }
152: }
153:
154: /** as getCallSignature, but param and return types are qualified */
155: public String getCallSignatureQualified(boolean java2ocl) {
156: return java2ocl ? callSigQualifOCL : callSigQualif;
157: }
158:
159: /** as getCallSignature, but param and return types are qualified */
160: public String getCallSignatureQualified() {
161: return getCallSignatureQualified(true);
162: }
163:
164: // returnvalue is adapted to the needs of OCL-parser from dresden
165: public String createCallSignature(boolean translateJavaType2OCLTypes) {
166: String argString = orig
167: .getProperty(RwiProperty.PARAMETERS_TEXT);
168: // argString has the form type1 arg1, type2 arg2, ...
169: // parser expects of form arg1: type1; arg2: type2
170: String parserString = shuffleForParser(argString,
171: translateJavaType2OCLTypes);
172:
173: String returnTypeString = orig
174: .getProperty(RwiProperty.RETURN_TYPE);
175: String retSuffix = null;
176: if (returnTypeString == null) {
177: // We have a constructor method ...
178: // Leave it empty (because of the syntax used by the OCL parser ...
179: retSuffix = "";
180: } else if (returnTypeString.equals("void")) {
181: // Leave it empty (because of the syntax used by the OCL parser ...
182: retSuffix = "";
183: } else {
184: if (translateJavaType2OCLTypes)
185: retSuffix = ":"
186: + transformTypeJava2OCL(returnTypeString);
187: else
188: retSuffix = ":" + returnTypeString;
189: }
190: return orig.getProperty(RwiProperty.NAME) + "(" + parserString
191: + ")" + retSuffix;
192: }
193:
194: /** take a fully qualified type name, remove qualification if it is not needed.
195: * The fullName must not end in "." */
196: private String fullname2qualname(String fullName, boolean java2ocl) {
197: int ix = fullName.lastIndexOf(".");
198: if (ix == -1) {
199: return transformTypeJava2OCL(fullName);
200: } else {
201: String pkg = fullName.substring(0, ix);
202: String shortName = fullName.substring(ix + 1);
203: if (!pkg.equals(getContainingPackage())) {
204: // qualification necessary
205: if (java2ocl) {
206: return pkg.replaceAll("\\.", "::") + "::"
207: + shortName;
208: } else {
209: return fullName;
210: }
211: } else {
212: // no qualification necessary
213: return shortName;
214: }
215: }
216: }
217:
218: private String sequentialize(String keyarrayof, boolean isArray,
219: boolean java2ocl) {
220: String result;
221: if (java2ocl) {
222: if (isArray) {
223: if (keyarrayof.indexOf("KeYArrayOf") > -1) {
224: result = keyarrayof.replaceFirst("KeYArrayOf",
225: "Sequence (")
226: + ")";
227: } else {
228: result = "Sequence (" + keyarrayof + ")";
229: }
230: } else {
231: result = keyarrayof;
232: }
233: } else {
234: result = keyarrayof; //conserve a buggy behaviour %%
235: //daniels does not want to break anything
236: }
237: return result;
238: }
239:
240: /**
241: * qualify types with package
242: * @param java2ocl true: OCL notation (package::class, Sequence(Integer)),
243: * false: java notation (package.class, int[])
244: * @return a String representing the fully qualified call signature
245: */
246: public String createCallSignatureQualified(boolean java2ocl) {
247: String retTypeUnqual = orig
248: .getProperty(RwiProperty.RETURN_TYPE);
249: //hack is needed, since orig.getProperty(RwiProperty.RETURN_TYPE_REFERENCED_ELEMENT)
250: //throws away the knowledge, if the return type is a package or not.
251: boolean isArray = retTypeUnqual == null ? false
252: : (retTypeUnqual.indexOf("[") > -1);
253: if (java2ocl && retTypeUnqual != null) {
254: retTypeUnqual = transformTypeJava2OCL(retTypeUnqual);
255: retTypeUnqual = sequentialize(retTypeUnqual, isArray,
256: java2ocl);
257: }
258:
259: String retType;
260: String retRef = orig
261: .getProperty(RwiProperty.RETURN_TYPE_REFERENCED_ELEMENT);
262: if (retRef != null) {
263: RwiElement foundElem = currRwiModel.findElement(retRef);
264: if (foundElem != null) {
265: String fullName = foundElem
266: .getProperty(RwiProperty.FULL_NAME);
267: String qualName = fullname2qualname(fullName, java2ocl);
268: qualName = sequentialize(qualName, isArray, java2ocl);
269: retType = qualName;
270: } else {
271: // could not qualify
272: retType = retTypeUnqual;
273: }
274: } else {
275: // retRef == null
276: retType = retTypeUnqual;
277: }
278:
279: Enumeration rwiParamsEnum = orig
280: .properties(RwiProperty.PARAMETER);
281: Vector paramNames = new Vector(); // elemtype: String
282: Vector paramTypesUnqual = new Vector(); // elemtype: String
283: Vector paramTypes = new Vector(); // elemtype: String
284:
285: while (rwiParamsEnum.hasMoreElements()) {
286: RwiProperty param = (RwiProperty) rwiParamsEnum
287: .nextElement();
288: RwiPropertyMap subprops = param.getSubproperties();
289: paramNames.add(subprops.getProperty(RwiProperty.NAME));
290: String paramTypeUnqual = subprops
291: .getProperty(RwiProperty.TYPE);
292: isArray = (paramTypeUnqual.indexOf("[") > -1);
293: if (java2ocl) {
294: paramTypeUnqual = transformTypeJava2OCL(paramTypeUnqual);
295: paramTypeUnqual = sequentialize(paramTypeUnqual,
296: isArray, java2ocl);
297: }
298: paramTypesUnqual.add(paramTypeUnqual);
299:
300: // qualified type
301: String uniqueTypeName = subprops
302: .getProperty(RwiProperty.TYPE_REFERENCED_ELEMENT);
303: RwiElement foundElem = currRwiModel
304: .findElement(uniqueTypeName);
305: if (foundElem != null) { // success not guaranteed
306: // (Together docs says e.g. it might not be in classpath)
307: // it might be a basic type e.g. int
308: String fullName = foundElem
309: .getProperty(RwiProperty.FULL_NAME);
310: String qualName = fullname2qualname(fullName, java2ocl);
311: qualName = sequentialize(qualName, isArray, java2ocl);
312: paramTypes.add(qualName);
313: } else {
314: // qualification failed: just add unqualified type
315: // or should we raise an exception?
316: paramTypes.add(paramTypeUnqual);
317: }
318: }
319:
320: // add parameters to signature:
321: String sig = "(";
322: Iterator i = paramNames.iterator();
323: Iterator j = paramTypes.iterator();
324: while (i.hasNext() && j.hasNext()) { // Vector length should be the same
325: String pName = (String) i.next();
326: String pType = (String) j.next();
327: if (java2ocl) {
328: sig += pName + " : " + pType;
329: } else {
330: sig += pType + " " + pName;
331: }
332: if (i.hasNext() && j.hasNext()) {
333: sig += ", ";
334: }
335: }
336:
337: // add return type:
338: sig += ")";
339: if (retType != null && !retType.equals("void")) {
340: sig += " : " + retType;
341: }
342:
343: return orig.getProperty(RwiProperty.NAME) + sig;
344: }
345:
346: public String getName() {
347: return name;
348: }
349:
350: // besides shuffling the arg with the type we also
351: // transform some java-types to ocl-types
352: private String shuffleForParser(String argString,
353: boolean translateJavaType2OCLTypes) {
354: argString = argString.trim();
355: if (argString.equals("")) {
356: return "";
357: }
358: String resString = "";
359: int actPos = 0;
360: int nextSpace, nextColon;
361: boolean through = false;
362: String optColon = "";
363: String actArgument, actTypeJava, actTypeOcl;
364: while (!through) {
365: //skip "final "
366: if (argString.substring(actPos).startsWith("final ")) {
367: actPos += 6;
368: }
369:
370: nextSpace = argString.indexOf(' ', actPos);
371: nextColon = argString.indexOf(',', actPos);
372: if (nextColon == -1) {
373: // end of argString
374: through = true;
375: nextColon = argString.length();
376: }
377: if (actPos > 0) {
378: optColon = "; ";
379: }
380: actArgument = argString.substring(nextSpace + 1, nextColon);
381: actTypeJava = argString.substring(actPos, nextSpace);
382:
383: // store parameters in vector
384: if (!parameterListComputed) {
385: paraNames.addElement(actArgument);
386: paraTypes.addElement(actTypeJava);
387: }
388:
389: if (translateJavaType2OCLTypes)
390: actTypeOcl = transformTypeJava2OCL(actTypeJava);
391: else
392: actTypeOcl = actTypeJava;
393: resString = resString + optColon + actArgument + ": "
394: + actTypeOcl;
395: actPos = nextColon + 2;
396: }
397: parameterListComputed = true;
398: return resString;
399: }
400:
401: public static String transformTypeJava2OCL(String aJavaType) {
402: return JavaModelMethod.transformTypeJava2OCL(aJavaType);
403: }
404:
405: // looks if orig has a parent and set it if needed
406: // parent means for methods the next occurrence of the method
407: // in the inheritance hierarchy which has an own pre/post specification
408: private RwiMember getOrigParent() {
409: if (origParentAlreadySet) {
410: return origParent;
411: } else {
412: // we ask our containingNode to do the job
413: RwiNode localContainingClass = orig.getContainingNode();
414: TogetherModelClass contClassRepr = new TogetherModelClass(
415: localContainingClass, currRwiModel, currRwiDiagram);
416: String myUniqueName = orig.getUniqueName();
417:
418: RwiMember candParent;
419: // findParentMeth returns the next Meth-Declaration
420: // in the inheritance hierarchy above
421: candParent = contClassRepr.findParentMeth(myUniqueName);
422: if (candParent == null) {
423: return null;
424: }
425: if ((candParent.getProperty("preconditions") != null || candParent
426: .getProperty("postconditions") != null)) {
427: // candParent has its own specification
428: origParent = candParent;
429: } else {
430: // otherwise we ask candParent for its parent
431: origParent = (new TogetherModelMethod(candParent,
432: currRwiModel, currRwiDiagram)).getOrigParent();
433: }
434: origParentAlreadySet = true;
435: }
436: return origParent;
437: }
438:
439: /** relies on a valid backing RWI model element, i.e. the together
440: * project is still valid (opened)
441: *
442: */
443: public String getMyOrParentPostCond() {
444: String myPre = getMyPreCond();
445: String myPost = getMyPostCond();
446: if (myPre.equals("") && myPost.equals("")) {
447: // ask parent
448: TogetherModelMethod parentRepr = new TogetherModelMethod(
449: getOrigParent(), currRwiModel, currRwiDiagram);
450: return parentRepr.getMyPostCond();
451: } else {
452: return myPost;
453: }
454: }
455:
456: /** relies on a valid backing RWI model element, i.e. the together
457: * project is still valid (opened);
458: * we ask the parent only when method does not have neither precond
459: * nor postcond.
460: */
461: public String getMyOrParentPreCond() {
462: String myPre = getMyPreCond();
463: String myPost = getMyPostCond();
464: if (myPre.equals("") && myPost.equals("")) {
465: // ask parent
466: TogetherModelMethod parentRepr = new TogetherModelMethod(
467: getOrigParent(), currRwiModel, currRwiDiagram);
468: return parentRepr.getMyPreCond();
469: } else {
470: return myPre;
471: }
472: }
473:
474: public String getMyPreCond() {
475: return (precond == null) ? "" : precond;
476: }
477:
478: /** relies on a valid backing RWI model element, i.e. the together
479: * project is still valid (opened)
480: */
481: public void setMyPreCond(String precond) {
482: this .precond = precond;
483: orig.setProperty("preconditions", precond);
484: }
485:
486: /** relies on a valid backing RWI model element, i.e. the together
487: * project is still valid (opened)
488: */
489: public String getParentPreCond() {
490: // ask parent
491: TogetherModelMethod parentRepr = new TogetherModelMethod(
492: getOrigParent(), currRwiModel, currRwiDiagram);
493: return parentRepr.getMyPreCond();
494: }
495:
496: public String getMyPostCond() {
497: return (postcond == null) ? "" : postcond;
498: }
499:
500: /** relies on a valid backing RWI model element, i.e. the together
501: * project is still valid (opened)
502: */
503: public void setMyPostCond(String postcond) {
504: this .postcond = postcond;
505: orig.setProperty("postconditions", postcond);
506: }
507:
508: /** relies on a valid backing RWI model element, i.e. the together
509: * project is still valid (opened)
510: */
511: public String getParentPostCond() {
512: // ask parent
513: TogetherModelMethod parentRepr = new TogetherModelMethod(
514: getOrigParent(), currRwiModel, currRwiDiagram);
515: return parentRepr.getMyPostCond();
516: }
517:
518: public String getMyModifClause() {
519: return (modifies == null) ? "" : modifies;
520: }
521:
522: /** relies on a valid backing RWI model element, i.e. the together
523: * project is still valid (opened)
524: */
525: public void setMyModifClause(String modifClause) {
526: modifies = modifClause;
527: orig.setProperty("modifies", modifClause);
528: }
529:
530: public boolean isQuery() {
531: return ("query".equals(stereotype));
532: }
533:
534: public boolean isConstructor() {
535: return constr;
536: }
537:
538: public boolean isPrivate() {
539: return priv;
540: }
541:
542: public String getMyGFAbs() {
543: String result = orig.getProperty("GFAbstractSyntax");
544: if (result == null) {
545: return "";
546: } else {
547: return result;
548: }
549: }
550:
551: /** relies on a valid backing RWI model element, i.e. the together
552: * project is still valid (opened)
553: */
554: public void setMyGFAbs(String abs) {
555: orig.setProperty("GFAbstractSyntax", abs);
556: }
557:
558: public boolean hasOrigParent() {
559: return (getOrigParent() != null);
560: }
561:
562: /** relies on a valid backing RWI model element, i.e. the together
563: * project is still valid (opened);
564: * gets the overridden methods in the superclass if exists else null
565: */
566: public ModelMethod getParentMethod() {
567: if (hasOrigParent()) {
568: return new TogetherModelMethod(getOrigParent(),
569: currRwiModel, currRwiDiagram);
570: } else
571: return null;
572: }
573:
574: public String toString() {
575: return getContainingClass().getClassName() + "::"
576: + getCallSignature();
577: }
578:
579: public boolean equals(Object cmp) {
580: if (cmp == null)
581: return false;
582: if (!(cmp instanceof TogetherModelMethod))
583: return false;
584: return toString().equals(cmp.toString());
585: }
586:
587: public int hashCode() {
588: return hash == 0 ? (hash = toString().hashCode()) : hash;
589: }
590:
591: public ListOfOperationContract getMyOperationContracts() {
592: ListOfOperationContract result = SLListOfOperationContract.EMPTY_LIST;
593:
594: String myPre = getMyPreCond();
595: String myPost = getMyPostCond();
596: String myModifies = getMyModifClause();
597: if (!myPre.equals("") || !myPost.equals("")
598: || !myModifies.equals("")) {
599: OperationContract contract = new OCLOperationContract(this ,
600: true, myPre, myPost, myModifies);
601: result = result.append(contract);
602: } else {
603: OperationContract defaultContract = new OCLOperationContract(
604: this , true, "true", "true", "");
605: result = result.append(defaultContract);
606: }
607:
608: return result;
609: }
610:
611: public boolean equalContractable(Contractable c) {
612: return equals(c);
613: }
614: }
|