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: //
012:
013: package de.uka.ilkd.key.ocl;
014:
015: import java.io.File;
016: import java.io.FileWriter;
017: import java.io.IOException;
018: import java.util.HashMap;
019: import java.util.Iterator;
020: import java.util.Vector;
021:
022: import de.uka.ilkd.key.casetool.ModelMethod;
023: import de.uka.ilkd.key.casetool.UMLModelClass;
024: import de.uka.ilkd.key.casetool.together.TogetherModelMethod;
025:
026: /** Export OCL specifications to a file */
027: public class OCLExport {
028:
029: private File file;
030: private UMLModelClass cls[];
031: private FileWriter out;
032:
033: private final static String SEP = "\n";
034:
035: private boolean adHocWarningAboutQualifications;
036:
037: public OCLExport(UMLModelClass cls, FileWriter out) {
038: this .cls = new UMLModelClass[1];
039: this .cls[0] = cls;
040: this .out = out;
041: adHocWarningAboutQualifications = false;
042: }
043:
044: public OCLExport(UMLModelClass[] cls, FileWriter out) {
045: this .cls = cls;
046: this .out = out;
047: adHocWarningAboutQualifications = false;
048: }
049:
050: /** get OCL specs (invariant, pre-/posts for methods) for one class */
051: private String getOCL(UMLModelClass c) {
052: String result = "";
053:
054: String cName = c.getClassName();
055:
056: String inv = c.getMyInv();
057: if (inv != null && !inv.equals("")) {
058: result += "context " + cName + "\ninv: " + inv + "\n";
059: }
060:
061: Vector ops = c.getOps();
062: for (int i = 0; i < ops.size(); i++) {
063: ModelMethod meth = (ModelMethod) (ops.elementAt(i));
064:
065: String pre = meth.getMyPreCond();
066: String post = meth.getMyPostCond();
067:
068: if (pre != null && !pre.equals("")) {
069: pre = "pre: " + pre + "\n";
070: } else {
071: pre = "";
072: }
073:
074: if (post != null && !post.equals("")) {
075: post = "post: " + post + "\n";
076: } else {
077: pre = "";
078: }
079:
080: if (pre != "" || (post != null && !post.equals(""))) {
081: // bug:
082: // we can only qualify types correctly if we have
083: // a TogetherReprModelMethod
084: if (meth instanceof TogetherModelMethod) {
085: result += "\ncontext "
086: + cName
087: + "::"
088: + ((TogetherModelMethod) meth)
089: .getCallSignatureQualified() + "\n";
090: } else {
091: adHocWarningAboutQualifications = true;
092: result += "\ncontext " + cName + "::"
093: + meth.getCallSignature() + "\n";
094: }
095: result += pre + post;
096: }
097: }
098:
099: return result;
100: }
101:
102: public void export() throws IOException {
103: // type: key=String (package name), value = String (OCL text)
104: // used since we need to group specifications by package in output file
105: HashMap packages = new HashMap();
106:
107: // collect OCL specs from all classes in array cls:
108: for (int i = 0; i < cls.length; i++) {
109: String ocl = getOCL(cls[i]);
110: if (ocl != null && !ocl.equals("")) {
111: String pack = cls[i].getContainingPackage();
112: if (pack == null || pack.equals("")) {
113: // put everything in a package by default
114: pack = "NOPACKAGE";
115: } else {
116: // Java package notation differs from OCL
117: pack = pack.replaceAll("\\.", "::");
118: }
119:
120: String oldPackSpec = (String) packages.get(pack);
121: if (oldPackSpec == null) {
122: packages.put(pack, ocl);
123: } else {
124: packages.put(pack, oldPackSpec + "\n" + ocl);
125: }
126: }
127: }
128:
129: // print all OCL specs in the hashmap packages:
130: if (adHocWarningAboutQualifications) {
131: // add comment to OCL file with warning about qualification
132: out
133: .write("--\n-- WARNING: could not qualify parameter and return types correctly; this file might not be valid OCL.\n--\n");
134: }
135: Iterator it = packages.keySet().iterator();
136: while (it.hasNext()) {
137: String pack = (String) it.next();
138: String spec = (String) packages.get(pack);
139:
140: if (spec != null && !spec.equals("")) {
141: out.write("package " + pack + "\n" + spec
142: + "\nendpackage\n\n");
143: }
144: }
145: }
146: }
|