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: /** @author Daniel Larsson */package de.uka.ilkd.key.proof.init;
012:
013: import java.io.*;
014: import java.util.Iterator;
015:
016: import javax.swing.JFrame;
017: import javax.swing.JOptionPane;
018:
019: import tudresden.ocl.check.types.Basic;
020: import tudresden.ocl.check.types.Type;
021: import de.uka.ilkd.key.casetool.*;
022: import de.uka.ilkd.key.casetool.together.UMLOCLTogetherModel;
023: import de.uka.ilkd.key.logic.Name;
024: import de.uka.ilkd.key.logic.NamespaceSet;
025: import de.uka.ilkd.key.logic.Term;
026: import de.uka.ilkd.key.logic.TermFactory;
027: import de.uka.ilkd.key.logic.op.Function;
028: import de.uka.ilkd.key.logic.op.NonRigidFunction;
029: import de.uka.ilkd.key.logic.op.RigidFunction;
030: import de.uka.ilkd.key.logic.op.TermSymbol;
031: import de.uka.ilkd.key.logic.op.oclop.OclOp;
032: import de.uka.ilkd.key.logic.sort.Sort;
033: import de.uka.ilkd.key.logic.sort.oclsort.OclSort;
034: import de.uka.ilkd.key.parser.DefaultTermParser;
035: import de.uka.ilkd.key.parser.SimpleTermParser;
036: import de.uka.ilkd.key.pp.AbbrevMap;
037: import de.uka.ilkd.key.proof.Proof;
038: import de.uka.ilkd.key.proof.ProofAggregate;
039: import de.uka.ilkd.key.proof.RuleSource;
040: import de.uka.ilkd.key.proof.mgt.Contract;
041: import de.uka.ilkd.key.proof.mgt.Contractable;
042:
043: /**
044: * Used for OCL Simplification.
045: * Consists of two separate parts (and should probably be divided
046: * into two classes):
047: * <ol>
048: * <li> One part is responsible for adding the needed sorts and functions
049: * to the namespaces (InitConfig) used by the prover.
050: * </li>
051: * <li> The other part creates, given a model representation of
052: * a class, a proof obligation of its invariant in the form
053: * of a term.
054: * The first step is to translate the OCL syntax to a representation
055: * expressed in the taclet language. This is done using the external
056: * program "ocl2taclet". The next step is then to apply the taclet
057: * parser to this representation, and the result is a Term
058: * representation of the invariant. This term becomes a proof
059: * obligation and can be handled by the prover.
060: * </li>
061: * </ol>
062: */
063: public class OCLInvSimplPO extends OCLProofOblInput implements
064: OCLSimplificationPO {
065:
066: /** The "ocl2taclet" command */
067: private static final String OCL2TACLET_COMMAND = "ocl2taclet";
068:
069: /** The name of the key file containing the OCL simplification rules */
070: private static final String RULE_SOURCE = "oclSimplificationRules.key";
071:
072: protected ModelClass aClass;
073:
074: /** The proof obligation */
075: private Term proofObl;
076:
077: public OCLInvSimplPO(ModelClass aClass) {
078: super ("Simplifying invariant of " + aClass.getClassName());
079: this .aClass = aClass;
080: }
081:
082: public Includes readIncludes() throws ProofInputException {
083: RuleSource standard = RuleSource.initRuleFile(RULE_SOURCE);
084: Includes includes = new Includes();
085: includes.put("oclSimplificationRules", standard);
086: return includes;
087: }
088:
089: protected void setProofObligation(Term po) {
090: proofObl = po;
091: }
092:
093: public boolean initContract(Contract contract) {
094: return false; // was true, but this seemed to be strange /AR
095: }
096:
097: public Contractable[] getObjectOfContract() {
098: return new Contractable[0];
099: }
100:
101: public ModelClass getModelClass() {
102: return aClass;
103: }
104:
105: public ProofAggregate getPO() {
106: if (proofObl == null)
107: throw new IllegalStateException("No proofObl term");
108: String s = getProofHeader(aClass.getRootDirectory());
109: return ProofAggregate.createProofAggregate(new Proof(name(),
110: proofObl, s, initConfig.createTacletIndex(), initConfig
111: .createBuiltInRuleIndex(), initConfig
112: .getServices()), name());
113: }
114:
115: /**
116: * Creates and sets the proof obligation term.
117: */
118: public void readProblem(ModStrategy mod) {
119: setProofObligation(generateInvSimplPO());
120: }
121:
122: /**
123: * Extracts the String invariant from the class representation
124: * and rewrites it into a format accepted by the "ocl2taclet"
125: * parser program.
126: */
127: protected String prepareInv(ModelClass aClass) {
128: StringBuffer str = new StringBuffer(aClass.getMyInv());
129: String pack = aClass.getContainingPackage();
130: if (pack == null) {
131: pack = "NOPACKAGE";
132: }
133: String className = aClass.getClassName();
134: str.insert(0, "package " + pack + "\ncontext " + className
135: + " inv:\n ");
136: str.append("\nendpackage");
137: return str.toString();
138: }
139:
140: /**
141: * Extracts the String invariant of the class representation,
142: * turns it into a corresponding Term, and wraps it in some
143: * other operators so that it can be handled by the prover.
144: * @return Resulting Term.
145: */
146: protected Term generateInvSimplPO() {
147: String preparedInv = prepareInv(aClass);
148: String tacletInv = ordinaryOcl2tacletOcl(preparedInv, aClass
149: .getRootDirectory());
150:
151: addNumeralLiterals(getInitConfig());
152: NamespaceSet nss = getInitConfig().namespaces();
153:
154: //Parse the taclified OCL constraint into a Term
155: Reader inReader = new StringReader(tacletInv);
156: SimpleTermParser parser = new DefaultTermParser();
157: Term term = null;
158: try {
159: term = parser
160: .parse(inReader, OclSort.OCLANY, getInitConfig()
161: .getServices(), nss, new AbbrevMap());
162: } catch (Exception ee) {
163: ee.printStackTrace();
164: }
165:
166: //Wrap the resulting term in a predicate called "OclWrapper"
167: TermFactory tf = new TermFactory();
168: TermSymbol oclWrapper = (Function) nss.functions().lookup(
169: new Name("$OclWrapper"));
170:
171: /*
172: TermSymbol insertSet
173: = (TermSymbol)nss.functions().lookup(new Name("$insert_set"));
174: TermSymbol emptySet
175: = (TermSymbol)nss.functions().lookup(new Name("$empty_set"));
176: */
177: TermSymbol consInv = (TermSymbol) nss.functions().lookup(
178: new Name("$cons_inv"));
179: TermSymbol nilInv = (TermSymbol) nss.functions().lookup(
180: new Name("$nil_inv"));
181: TermSymbol invariant = (Function) nss.functions().lookup(
182: new Name("$invariant"));
183: String className = aClass.getFullClassName();
184: String uniqueClassName = className.replace('.', '~');
185: TermSymbol classOp = (Function) nss.functions().lookup(
186: new Name(uniqueClassName));
187: Term classTerm = tf.createFunctionTerm(classOp);
188: //Term emptySetTerm = tf.createFunctionTerm(emptySet);
189: Term emptySetTerm = tf.createFunctionTerm(nilInv);
190: Term invariantTerm = tf.createFunctionTerm(invariant,
191: new Term[] { classTerm, term });
192: /*
193: Term setOfInvariantTerm
194: = tf.createFunctionTerm(insertSet, new Term[]{invariantTerm,
195: emptySetTerm});
196: */
197: Term setOfInvariantTerm = tf.createFunctionTerm(consInv,
198: new Term[] { invariantTerm, emptySetTerm });
199:
200: //Term formula = tf.createFunctionTerm(oclWrapper, term);
201: Term formula = tf.createFunctionTerm(oclWrapper,
202: setOfInvariantTerm);
203: return formula;
204: }
205:
206: /**
207: * Applies the binary "ocl2taclet" to the String invariant.
208: * @param preparedInv String invariant.
209: * @param rootDir Directory where the file with model information,
210: * "modelinfo.umltypes", is stored (needed by "ocl2taclet").
211: * @return Invariant expressed in the taclet language.
212: */
213: private String ordinaryOcl2tacletOcl(String preparedInv,
214: String rootDir) {
215: //Invokes the "ocl2taclet" parser
216: Process p = null;
217: try {
218: //Runs "ocl2taclet modelinfo.umltypes"
219: p = Runtime.getRuntime().exec(
220: new String[] { OCL2TACLET_COMMAND,
221: rootDir + "/modelinfo.umltypes" });
222:
223: //Writes the invariant on the sub process' output stream
224: OutputStream out = p.getOutputStream();
225: OutputStreamWriter writer = new OutputStreamWriter(out);
226: writer.write(preparedInv);
227: writer.flush();
228: writer.close();
229: } catch (IOException e1) {
230: JOptionPane
231: .showMessageDialog(
232: new JFrame(),
233: "\"ocl2taclet\" execution failed:\n\n"
234: + e1
235: + "\n\n"
236: + "To make use of ocl2taclet make sure that\n\n"
237: + "1. the directory where the binary resides is in "
238: + "your $PATH variable\n"
239: + "2. the binary has executable file permissions.",
240: "Error", JOptionPane.ERROR_MESSAGE);
241: throw new RuntimeException(
242: "\"ocl2taclet\" execution failed.\n"
243: + "Is the binary in your $PATH?");
244: }
245:
246: //Wait for the sub process to terminate
247: try {
248: p.waitFor();
249: } catch (InterruptedException ie) {
250: ie.printStackTrace();
251: }
252:
253: //Reads the input stream (the parse result) into a String
254: InputStream in = p.getInputStream();
255: StringBuffer buffer = new StringBuffer();
256: try {
257: int ch = 0;
258: while ((ch = in.read()) != -1) {
259: buffer.append((char) ch);
260: }
261: } catch (IOException ioe) {
262: ioe.printStackTrace();
263: }
264: String result = new String(buffer);
265: result = result.trim();
266:
267: //If result is empty there is a syntax error in constraint
268: if (result.equals("")) {
269: JOptionPane.showMessageDialog(new JFrame(),
270: "\"ocl2taclet\" execution failed:\n\n" + "\n\n"
271: + "Syntax error in OCL constraint:\n\n"
272: + preparedInv, "Error",
273: JOptionPane.ERROR_MESSAGE);
274: throw new RuntimeException(
275: "\"ocl2taclet\" execution failed");
276: }
277: return result;
278: }
279:
280: /**
281: * Adds OCL types, OCL operations, and model properties to the
282: * name spaces of the initial configuration.
283: * Can as well be hard-coded, since they are needed for all
284: * OCL simplification. Also avoids trouble with taclet parser.
285: * @param initConf The initial configuration whose set of name
286: * spaces needs to be updated.
287: */
288: public void createNamespaceSet(InitConfig initConf) {
289: addPredefinedOCLSorts(initConf);
290: addPredefinedOCLOperations(initConf);
291: addModelProperties(initConf);
292: //addNumeralLiterals(initConf);
293: }
294:
295: private static void addPredefinedOCLSorts(InitConfig initConf) {
296: initConf.sortNS().add(OclSort.OCLINVARIANT);
297: initConf.sortNS().add(OclSort.SET_OF_OCLINVARIANT);
298:
299: initConf.sortNS().add(OclSort.OCLGENERIC);
300: initConf.sortNS().add(OclSort.OCLANY);
301: initConf.sortNS().add(OclSort.OCLTYPE);
302: initConf.sortNS().add(OclSort.REAL);
303: initConf.sortNS().add(OclSort.INTEGER);
304: initConf.sortNS().add(OclSort.STRING);
305: initConf.sortNS().add(OclSort.BOOLEAN);
306: initConf.sortNS().add(OclSort.CLASSIFIER);
307:
308: initConf.sortNS().add(OclSort.COLLECTION_OF_OCLGENERIC);
309: initConf.sortNS().add(OclSort.COLLECTION_OF_OCLANY);
310: initConf.sortNS().add(OclSort.COLLECTION_OF_OCLTYPE);
311: initConf.sortNS().add(OclSort.COLLECTION_OF_REAL);
312: initConf.sortNS().add(OclSort.COLLECTION_OF_INTEGER);
313: initConf.sortNS().add(OclSort.COLLECTION_OF_STRING);
314: initConf.sortNS().add(OclSort.COLLECTION_OF_BOOLEAN);
315: initConf.sortNS().add(OclSort.COLLECTION_OF_CLASSIFIER);
316:
317: initConf.sortNS().add(OclSort.SET_OF_OCLGENERIC);
318: initConf.sortNS().add(OclSort.SET_OF_OCLANY);
319: initConf.sortNS().add(OclSort.SET_OF_OCLTYPE);
320: initConf.sortNS().add(OclSort.SET_OF_REAL);
321: initConf.sortNS().add(OclSort.SET_OF_INTEGER);
322: initConf.sortNS().add(OclSort.SET_OF_STRING);
323: initConf.sortNS().add(OclSort.SET_OF_BOOLEAN);
324: initConf.sortNS().add(OclSort.SET_OF_CLASSIFIER);
325:
326: initConf.sortNS().add(OclSort.BAG_OF_OCLGENERIC);
327: initConf.sortNS().add(OclSort.BAG_OF_OCLANY);
328: initConf.sortNS().add(OclSort.BAG_OF_OCLTYPE);
329: initConf.sortNS().add(OclSort.BAG_OF_REAL);
330: initConf.sortNS().add(OclSort.BAG_OF_INTEGER);
331: initConf.sortNS().add(OclSort.BAG_OF_STRING);
332: initConf.sortNS().add(OclSort.BAG_OF_BOOLEAN);
333: initConf.sortNS().add(OclSort.BAG_OF_CLASSIFIER);
334:
335: initConf.sortNS().add(OclSort.SEQUENCE_OF_OCLGENERIC);
336: initConf.sortNS().add(OclSort.SEQUENCE_OF_OCLANY);
337: initConf.sortNS().add(OclSort.SEQUENCE_OF_OCLTYPE);
338: initConf.sortNS().add(OclSort.SEQUENCE_OF_REAL);
339: initConf.sortNS().add(OclSort.SEQUENCE_OF_INTEGER);
340: initConf.sortNS().add(OclSort.SEQUENCE_OF_STRING);
341: initConf.sortNS().add(OclSort.SEQUENCE_OF_BOOLEAN);
342: initConf.sortNS().add(OclSort.SEQUENCE_OF_CLASSIFIER);
343: }
344:
345: private static void addPredefinedOCLOperations(InitConfig initConf) {
346: initConf.funcNS().add(OclOp.INVARIANT);
347: initConf.funcNS().add(OclOp.CONS_INV);
348: initConf.funcNS().add(OclOp.NIL_INV);
349:
350: initConf.funcNS().add(
351: new RigidFunction(new Name("OclAny"), OclSort.OCLTYPE,
352: new Sort[0]));
353: initConf.funcNS().add(
354: new RigidFunction(new Name("OclType"), OclSort.OCLTYPE,
355: new Sort[0]));
356: initConf.funcNS().add(
357: new RigidFunction(new Name("OclBoolean"),
358: OclSort.OCLTYPE, new Sort[0]));
359: initConf.funcNS().add(
360: new RigidFunction(new Name("OclReal"), OclSort.OCLTYPE,
361: new Sort[0]));
362: initConf.funcNS().add(
363: new RigidFunction(new Name("OclInteger"),
364: OclSort.OCLTYPE, new Sort[0]));
365: initConf.funcNS().add(
366: new RigidFunction(new Name("OclString"),
367: OclSort.OCLTYPE, new Sort[0]));
368: initConf.funcNS().add(
369: new RigidFunction(new Name("OclClassifier"),
370: OclSort.OCLTYPE, new Sort[0]));
371:
372: initConf.funcNS().add(OclOp.ITERATE);
373: initConf.funcNS().add(OclOp.FOR_ALL);
374: initConf.funcNS().add(OclOp.EXISTS);
375: initConf.funcNS().add(OclOp.IF);
376: initConf.funcNS().add(OclOp.ALL_SUBTYPES);
377: initConf.funcNS().add(OclOp.ALL_INSTANCES);
378: initConf.funcNS().add(OclOp.INSERT_SET);
379: initConf.funcNS().add(OclOp.INSERT_BAG);
380: initConf.funcNS().add(OclOp.INSERT_SEQUENCE);
381: initConf.funcNS().add(OclOp.EMPTY_SET);
382: initConf.funcNS().add(OclOp.EMPTY_BAG);
383: initConf.funcNS().add(OclOp.EMPTY_SEQUENCE);
384: initConf.funcNS().add(OclOp.UNION);
385: initConf.funcNS().add(OclOp.INTERSECTION);
386: initConf.funcNS().add(OclOp.DIFFERENCE);
387: initConf.funcNS().add(OclOp.SYMMETRIC_DIFFERENCE);
388: initConf.funcNS().add(OclOp.SELECT);
389: initConf.funcNS().add(OclOp.REJECT);
390: initConf.funcNS().add(OclOp.COLLECT);
391: initConf.funcNS().add(OclOp.TRUE);
392: initConf.funcNS().add(OclOp.FALSE);
393: initConf.funcNS().add(OclOp.AND);
394: initConf.funcNS().add(OclOp.EQUALS);
395: initConf.funcNS().add(OclOp.OCL_WRAPPER);
396: initConf.funcNS().add(OclOp.SELF);
397: initConf.funcNS().add(OclOp.SIZE);
398: initConf.funcNS().add(OclOp.INCLUDES);
399: initConf.funcNS().add(OclOp.EXCLUDES);
400: initConf.funcNS().add(OclOp.COUNT);
401: initConf.funcNS().add(OclOp.INCLUDES_ALL);
402: initConf.funcNS().add(OclOp.EXCLUDES_ALL);
403: initConf.funcNS().add(OclOp.IS_EMPTY);
404: initConf.funcNS().add(OclOp.NOT_EMPTY);
405: initConf.funcNS().add(OclOp.SUM);
406: initConf.funcNS().add(OclOp.IS_UNIQUE);
407: initConf.funcNS().add(OclOp.SORTED_BY);
408: initConf.funcNS().add(OclOp.ANY);
409: initConf.funcNS().add(OclOp.ONE);
410: initConf.funcNS().add(OclOp.INCLUDING);
411: initConf.funcNS().add(OclOp.EXCLUDING);
412: initConf.funcNS().add(OclOp.AS_SET);
413: initConf.funcNS().add(OclOp.AS_BAG);
414: initConf.funcNS().add(OclOp.AS_SEQUENCE);
415: initConf.funcNS().add(OclOp.APPEND);
416: initConf.funcNS().add(OclOp.PREPEND);
417: initConf.funcNS().add(OclOp.SUB_SEQUENCE);
418: initConf.funcNS().add(OclOp.AT);
419: initConf.funcNS().add(OclOp.FIRST);
420: initConf.funcNS().add(OclOp.LAST);
421: initConf.funcNS().add(OclOp.NOT_EQUALS);
422: initConf.funcNS().add(OclOp.OCL_IS_NEW);
423: initConf.funcNS().add(OclOp.OR);
424: initConf.funcNS().add(OclOp.XOR);
425: initConf.funcNS().add(OclOp.NOT);
426: initConf.funcNS().add(OclOp.IMPLIES);
427: initConf.funcNS().add(OclOp.LESS_THAN);
428: initConf.funcNS().add(OclOp.LESS_THAN_EQ);
429: initConf.funcNS().add(OclOp.GREATER_THAN);
430: initConf.funcNS().add(OclOp.GREATER_THAN_EQ);
431: initConf.funcNS().add(OclOp.PLUS);
432: initConf.funcNS().add(OclOp.MINUS);
433: initConf.funcNS().add(OclOp.TIMES);
434: initConf.funcNS().add(OclOp.DIV_INFIX);
435: initConf.funcNS().add(OclOp.DIV);
436: initConf.funcNS().add(OclOp.MOD);
437: initConf.funcNS().add(OclOp.MIN);
438: initConf.funcNS().add(OclOp.MAX);
439: initConf.funcNS().add(OclOp.MINUS_PREFIX);
440: initConf.funcNS().add(OclOp.ABS);
441:
442: /*
443: IteratorOfNamed it = initConf.sortNS().allElements().iterator();
444: while (it.hasNext()) {
445: Sort sort = (Sort)it.next();
446: if (sort instanceof ClassInstanceSortImpl) {
447: initConf.sortNS().add(new OclObject(sort.name()));
448: }
449: }
450: */
451: }
452:
453: /**
454: * Uses ".../casetool/together/UMLOCLTogetherModel" together with
455: * the classes in ".../casetool/" to extract classifiers, attributes,
456: * (query) methods, and associations and add them to the function
457: * namespace.
458: */
459: private static void addModelProperties(InitConfig initConf) {
460: //Add all classifiers and properties from the UML model
461: //to the namespace
462: UMLOCLTogetherModel umlModel = new UMLOCLTogetherModel(null);
463: Iterator iter = umlModel.getUMLOCLClassifiers().values()
464: .iterator();
465: while (iter.hasNext()) {
466: UMLOCLClassifier classifier = (UMLOCLClassifier) iter
467: .next();
468: String cName = classifier.getFullName();
469: String uniqueClassName = cName.replace('.', '~');
470: Name className = new Name(uniqueClassName);
471: initConf.funcNS().add(
472: new NonRigidFunction(className, OclSort.OCLTYPE,
473: new Sort[0]));
474: Iterator featureIter = classifier.features().values()
475: .iterator();
476: while (featureIter.hasNext()) {
477: UMLOCLFeature feature = (UMLOCLFeature) featureIter
478: .next();
479: String fName = feature.getName();
480: Type type = feature.getType();
481: Sort featureSort = null;
482: if (type instanceof Basic) {
483: if (type == Basic.BOOLEAN) {
484: featureSort = OclSort.BOOLEAN;
485: } else if (type == Basic.INTEGER) {
486: featureSort = OclSort.INTEGER;
487: } else if (type == Basic.REAL) {
488: featureSort = OclSort.REAL;
489: } else if (type == Basic.STRING) {
490: featureSort = OclSort.STRING;
491: }
492: } else if (type instanceof tudresden.ocl.check.types.OclType) {
493: featureSort = OclSort.OCLTYPE;
494: } else if (type instanceof tudresden.ocl.check.types.Collection) {
495: /*
496: Type elementType = type.getElementType();
497: if (type.getCollectionKind() == tudresden.ocl.check.types.Collection.SET) {
498: if (elementType instanceof Basic) {
499: if (elementType == Basic.BOOLEAN) {
500: featureSort = OclSort.SET_OF_BOOLEAN;
501: } else if (elementType == Basic.INTEGER) {
502: featureSort = OclSort.SET_OF_INTEGER;
503: } else if (elementType == Basic.REAL) {
504: featureSort = OclSort.SET_OF_REAL;
505: } else if (elementType == Basic.STRING) {
506: featureSort = OclSort.SET_OF_STRING;
507: }
508: } else if (elementType instanceof tudresden.ocl.check.types.OclType) {
509: featureSort = OclSort.SET_OF_OCLTYPE;
510: }
511: } else if (type.getCollectionKind() == tudresden.ocl.check.types.Collection.BAG) {
512: if (elementType instanceof Basic) {
513: if (elementType == Basic.BOOLEAN) {
514: featureSort = OclSort.BAG_OF_BOOLEAN;
515: } else if (elementType == Basic.INTEGER) {
516: featureSort = OclSort.BAG_OF_INTEGER;
517: } else if (elementType == Basic.REAL) {
518: featureSort = OclSort.BAG_OF_REAL;
519: } else if (elementType == Basic.STRING) {
520: featureSort = OclSort.BAG_OF_STRING;
521: }
522: } else if (elementType instanceof tudresden.ocl.check.types.OclType) {
523: featureSort = OclSort.BAG_OF_OCLTYPE;
524: }
525: } else {
526: if (elementType instanceof Basic) {
527: if (elementType == Basic.BOOLEAN) {
528: featureSort = OclSort.SEQUENCE_OF_BOOLEAN;
529: } else if (elementType == Basic.INTEGER) {
530: featureSort = OclSort.SEQUENCE_OF_INTEGER;
531: } else if (elementType == Basic.REAL) {
532: featureSort = OclSort.SEQUENCE_OF_REAL;
533: } else if (elementType == Basic.STRING) {
534: featureSort = OclSort.SEQUENCE_OF_STRING;
535: }
536: } else if (elementType instanceof tudresden.ocl.check.types.OclType) {
537: featureSort = OclSort.SEQUENCE_OF_OCLTYPE;
538: }
539: }
540: */
541: featureSort = OclSort.COLLECTION_OF_OCLANY;
542: } else {
543: featureSort = OclSort.CLASSIFIER;
544: }
545: String uniqueFeatureName = uniqueClassName + "~"
546: + fName.replace(',', '+').replace('.', '~');
547: int leftParIndex = uniqueFeatureName.indexOf("(");
548: if (leftParIndex > -1) {
549: int rightParIndex = uniqueFeatureName.indexOf(")");
550: StringBuffer buffer = new StringBuffer(
551: uniqueFeatureName);
552: buffer = buffer.replace(leftParIndex,
553: leftParIndex + 1, "+~");
554: buffer = buffer.replace(rightParIndex,
555: rightParIndex + 1, "~+");
556: uniqueFeatureName = buffer.toString();
557: }
558: Name featureName = new Name(uniqueFeatureName);
559: if (feature instanceof UMLOCLStructuralFeature) {
560: initConf.funcNS().add(
561: new NonRigidFunction(featureName,
562: featureSort,
563: new Sort[] { OclSort.CLASSIFIER }));
564: } else {
565: int numOfArgs = ((UMLOCLBehaviouralFeature) feature)
566: .getParameters().length + 1;
567: Sort[] argSorts = new Sort[numOfArgs];
568: argSorts[0] = OclSort.CLASSIFIER;
569: for (int i = 1; i < numOfArgs; i++) {
570: argSorts[i] = OclSort.OCLANY;
571: }
572: initConf.funcNS().add(
573: new NonRigidFunction(featureName,
574: featureSort, argSorts));
575: }
576: }
577: Iterator assocIter = classifier.getAssociations().values()
578: .iterator();
579: while (assocIter.hasNext()) {
580: UMLOCLAssociation assoc = (UMLOCLAssociation) assocIter
581: .next();
582: String aName = assoc.getTargetRole();
583: String uniqueAssocName = uniqueClassName + "~" + aName;
584: Name assocName = new Name(uniqueAssocName);
585: initConf.funcNS().add(
586: new NonRigidFunction(assocName,
587: OclSort.COLLECTION_OF_CLASSIFIER,
588: new Sort[] { OclSort.CLASSIFIER }));
589: }
590: }
591: }
592:
593: /**
594: * Adds the integer operations to the function namespace
595: * of the initial configuration. Gives them the proper Sort.
596: */
597: private static void addNumeralLiterals(InitConfig initConf) {
598: //Add numeral literals to the namespace
599: //(must have type/sort OclSort.INTEGER)
600: initConf.funcNS().add(
601: new RigidFunction(new Name("#"), OclSort.INTEGER,
602: new Sort[0]));
603: initConf.funcNS().add(
604: new RigidFunction(new Name("Z"), OclSort.INTEGER,
605: new Sort[] { OclSort.INTEGER }));
606: initConf.funcNS().add(
607: new RigidFunction(new Name("0"), OclSort.INTEGER,
608: new Sort[] { OclSort.INTEGER }));
609: initConf.funcNS().add(
610: new RigidFunction(new Name("1"), OclSort.INTEGER,
611: new Sort[] { OclSort.INTEGER }));
612: initConf.funcNS().add(
613: new RigidFunction(new Name("2"), OclSort.INTEGER,
614: new Sort[] { OclSort.INTEGER }));
615: initConf.funcNS().add(
616: new RigidFunction(new Name("3"), OclSort.INTEGER,
617: new Sort[] { OclSort.INTEGER }));
618: initConf.funcNS().add(
619: new RigidFunction(new Name("4"), OclSort.INTEGER,
620: new Sort[] { OclSort.INTEGER }));
621: initConf.funcNS().add(
622: new RigidFunction(new Name("5"), OclSort.INTEGER,
623: new Sort[] { OclSort.INTEGER }));
624: initConf.funcNS().add(
625: new RigidFunction(new Name("6"), OclSort.INTEGER,
626: new Sort[] { OclSort.INTEGER }));
627: initConf.funcNS().add(
628: new RigidFunction(new Name("7"), OclSort.INTEGER,
629: new Sort[] { OclSort.INTEGER }));
630: initConf.funcNS().add(
631: new RigidFunction(new Name("8"), OclSort.INTEGER,
632: new Sort[] { OclSort.INTEGER }));
633: initConf.funcNS().add(
634: new RigidFunction(new Name("9"), OclSort.INTEGER,
635: new Sort[] { OclSort.INTEGER }));
636: }
637:
638: public static void createNamespaceSetForTests(InitConfig initConf) {
639: addPredefinedOCLSorts(initConf);
640: addPredefinedOCLOperations(initConf);
641: addNumeralLiterals(initConf);
642: }
643: }
|