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: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.parser.ocl;
019:
020: import java.util.HashMap;
021: import java.util.Map;
022:
023: import de.uka.ilkd.key.java.Services;
024: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
025: import de.uka.ilkd.key.logic.Name;
026: import de.uka.ilkd.key.logic.Term;
027: import de.uka.ilkd.key.logic.TermBuilder;
028: import de.uka.ilkd.key.logic.TermFactory;
029: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
030: import de.uka.ilkd.key.logic.op.ArrayOp;
031: import de.uka.ilkd.key.logic.op.Function;
032: import de.uka.ilkd.key.logic.op.IteratorOfLogicVariable;
033: import de.uka.ilkd.key.logic.op.Junctor;
034: import de.uka.ilkd.key.logic.op.LogicVariable;
035: import de.uka.ilkd.key.logic.op.Op;
036: import de.uka.ilkd.key.logic.op.ParsableVariable;
037: import de.uka.ilkd.key.logic.op.Quantifier;
038: import de.uka.ilkd.key.logic.sort.AbstractCollectionSort;
039: import de.uka.ilkd.key.logic.sort.AbstractSort;
040: import de.uka.ilkd.key.logic.sort.ArraySort;
041: import de.uka.ilkd.key.logic.sort.CollectionSort;
042: import de.uka.ilkd.key.logic.sort.Sort;
043: import de.uka.ilkd.key.proof.OpReplacer;
044: import de.uka.ilkd.key.proof.init.CreatedAttributeTermFactory;
045: import de.uka.ilkd.key.util.Debug;
046:
047: /**
048: * Resolves built-in ocl property calls.
049: */
050: class BuiltInPropertyResolver implements PropertyResolver {
051:
052: private static final TermFactory tf = TermFactory.DEFAULT;
053: private static final TermBuilder tb = TermBuilder.DF;
054:
055: private static final CreatedAttributeTermFactory createdFactory = CreatedAttributeTermFactory.INSTANCE;
056: private static final Term trueTerm = tb.tt();
057: private static final Term falseTerm = tb.ff();
058:
059: private final Services services;
060:
061: private ParsableVariable excVar;
062:
063: public BuiltInPropertyResolver(Services services,
064: ParsableVariable excVar) {
065: this .services = services;
066: this .excVar = excVar;
067: }
068:
069: private Term replaceVar(LogicVariable lv1, LogicVariable lv2,
070: Term term) {
071: Map map = new HashMap();
072: map.put(lv1, lv2);
073: OpReplacer or = new OpReplacer(map);
074: return or.replace(term);
075: }
076:
077: private void raiseError(String message) throws OCLTranslationError {
078: throw new OCLTranslationError(
079: "OCL Parser Error (PropertyResolver): " + message);
080: }
081:
082: public OCLEntity resolve(OCLEntity receiver, String name,
083: OCLParameters parameters) throws OCLTranslationError {
084: //allInstances---------------------------------------------------------
085: if (name.equals("allInstances")) {
086: if (!receiver.isType() || parameters == null
087: || !parameters.getDeclaredVars().isEmpty()
088: || !parameters.getEntities().isEmpty()) {
089: return null;
090: }
091:
092: return new OCLEntity(new OCLCollection(receiver.getSort(),
093: services));
094: }
095:
096: //quantifiers----------------------------------------------------------
097: if (name.equals("forAll") || name.equals("exists")) {
098: if (!receiver.isCollection() || parameters == null
099: || parameters.getDeclaredVars().isEmpty()
100: || parameters.getEntities().size() != 1) {
101: return null;
102: }
103:
104: Quantifier q;
105: Junctor j;
106: if (name.equals("forAll")) {
107: q = Op.ALL;
108: j = Op.IMP;
109: } else {
110: q = Op.EX;
111: j = Op.AND;
112: }
113:
114: Term restrictions = trueTerm;
115: IteratorOfLogicVariable it = parameters.getDeclaredVars()
116: .iterator();
117: while (it.hasNext()) {
118: Term t = replaceVar(receiver.getCollection()
119: .getPredVar(), it.next(), receiver
120: .getCollection().getPredicativeRestriction());
121: restrictions = tf.createJunctorTermAndSimplify(Op.AND,
122: restrictions, t);
123: }
124:
125: Term subTerm = tf.createJunctorTermAndSimplify(j,
126: restrictions, parameters.getEntities().head()
127: .getTerm());
128: Term resTerm = createdFactory
129: .createCreatedNotNullQuantifierTerm(services, q,
130: parameters.getDeclaredVars().toArray(),
131: subTerm);
132:
133: return new OCLEntity(resTerm);
134: }
135:
136: //select/reject--------------------------------------------------------
137: if (name.equals("select") || name.equals("reject")) {
138: if (!receiver.isCollection() || parameters == null
139: || parameters.getDeclaredVars().size() != 1
140: || parameters.getEntities().size() != 1) {
141: return null;
142: }
143:
144: //Replace all occurrences of the new selectorVar with the
145: //appropriate collectionVar
146: Term selectTerm = replaceVar(parameters.getDeclaredVars()
147: .head(), receiver.getCollection().getPredVar(),
148: parameters.getEntities().head().getTerm());
149:
150: if (name.equals("reject")) {
151: selectTerm = tf.createJunctorTerm(Op.NOT, selectTerm);
152: }
153:
154: LogicVariable selectVar = receiver.getCollection()
155: .getPredVar();
156:
157: OCLCollection resCollection = receiver.getCollection()
158: .select(selectVar, selectTerm);
159:
160: return new OCLEntity(resCollection);
161: }
162:
163: //collect--------------------------------------------------------------
164: if (name.equals("collect")) {
165: if (!receiver.isCollection() || parameters == null
166: || parameters.getDeclaredVars().size() > 1
167: || parameters.getEntities().size() != 1) {
168: return null;
169: }
170:
171: Term collectTerm = parameters.getEntities().head()
172: .getTerm();
173:
174: if (collectTerm == null) {
175: // collectTerm was a collection
176: raiseError("Automatic flattening only supported for navigation over associations!");
177:
178: // System.out.println(parameters.getEntities().head().getCollection());
179: //OCLCollection result = receiver.getCollection().collect(services,
180: // parameters.getEntities().head().getCollection());
181: //return new OCLEntity(result);
182:
183: }
184:
185: if (!parameters.getDeclaredVars().isEmpty()) {
186: collectTerm = replaceVar(parameters.getDeclaredVars()
187: .head(), receiver.getCollection().getPredVar(),
188: collectTerm);
189: }
190:
191: OCLCollection result = receiver.getCollection().collect(
192: services, collectTerm);
193:
194: return new OCLEntity(result);
195: }
196:
197: //includes/excludes----------------------------------------------------
198: if (name.equals("includes") || name.equals("excludes")) {
199: if (!receiver.isCollection() || parameters == null
200: || !parameters.getDeclaredVars().isEmpty()
201: || parameters.getEntities().size() != 1) {
202: return null;
203: }
204:
205: Term opTerm = tf.createEqualityTerm(receiver
206: .getCollection().getPredVarAsTerm(), parameters
207: .getEntities().head().getTerm());
208:
209: Quantifier q;
210: Junctor j;
211: if (name.equals("excludes")) {
212: opTerm = tf.createJunctorTerm(Op.NOT, opTerm);
213: q = Op.ALL;
214: j = Op.IMP;
215: } else {
216: q = Op.EX;
217: j = Op.AND;
218: }
219:
220: opTerm = tf.createJunctorTermAndSimplify(j, receiver
221: .getCollection().getPredicativeRestriction(),
222: opTerm);
223:
224: LogicVariable[] vars = { receiver.getCollection()
225: .getPredVar() };
226: Term resTerm = createdFactory
227: .createCreatedNotNullQuantifierTerm(services, q,
228: vars, opTerm);
229:
230: return new OCLEntity(resTerm);
231: }
232:
233: //isEmpty/notEmpty-----------------------------------------------------
234: if (name.equals("isEmpty") || name.equals("notEmpty")) {
235: if (!receiver.isCollection() || parameters == null
236: || !parameters.getDeclaredVars().isEmpty()
237: || !parameters.getEntities().isEmpty()) {
238: return null;
239: }
240:
241: Quantifier q;
242: Junctor j;
243: Term opTerm;
244: if (name.equals("isEmpty")) {
245: q = Op.ALL;
246: j = Op.IMP;
247: opTerm = falseTerm;
248: } else {
249: q = Op.EX;
250: j = Op.AND;
251: opTerm = trueTerm;
252: }
253:
254: opTerm = tf.createJunctorTerm(j, receiver.getCollection()
255: .getPredicativeRestriction(), opTerm);
256:
257: LogicVariable[] vars = { receiver.getCollection()
258: .getPredVar() };
259: Term resTerm = createdFactory
260: .createCreatedNotNullQuantifierTerm(services, q,
261: vars, opTerm);
262:
263: return new OCLEntity(resTerm);
264: }
265:
266: //isUnique-------------------------------------------------------------
267: if (name.equals("isUnique")) {
268: if (!receiver.isCollection() || parameters == null
269: || parameters.getDeclaredVars().size() != 1
270: || parameters.getEntities().size() != 1) {
271: return null;
272: }
273:
274: Term restrictions = trueTerm;
275: LogicVariable temp = parameters.getDeclaredVars().head();
276: LogicVariable lv1 = new LogicVariable(new Name(temp.name()
277: + "_1"), temp.sort());
278: LogicVariable lv2 = new LogicVariable(new Name(temp.name()
279: + "_2"), temp.sort());
280:
281: Term t1 = replaceVar(receiver.getCollection().getPredVar(),
282: lv1, receiver.getCollection()
283: .getPredicativeRestriction());
284: Term t2 = replaceVar(receiver.getCollection().getPredVar(),
285: lv2, receiver.getCollection()
286: .getPredicativeRestriction());
287:
288: restrictions = tf.createJunctorTermAndSimplify(Op.AND, t1,
289: t2);
290:
291: t1 = replaceVar(temp, lv1, parameters.getEntities().head()
292: .getTerm());
293: t2 = replaceVar(temp, lv2, parameters.getEntities().head()
294: .getTerm());
295:
296: restrictions = tf.createJunctorTermAndSimplify(Op.AND,
297: restrictions, tf.createEqualityTerm(t1, t2));
298:
299: t1 = tf.createVariableTerm(lv1);
300: t2 = tf.createVariableTerm(lv2);
301:
302: Term subTerm = tf.createJunctorTermAndSimplify(Op.IMP,
303: restrictions, tf.createEqualityTerm(t1, t2));
304: Term resTerm = createdFactory
305: .createCreatedNotNullQuantifierTerm(services,
306: Op.ALL, new LogicVariable[] { lv1, lv2 },
307: subTerm);
308:
309: return new OCLEntity(resTerm);
310:
311: }
312:
313: //size/sum/count--------------------------------------------------------------
314: if (name.equals("size") || name.equals("sum")
315: || name.equals("count")) {
316:
317: if (!receiver.isCollection() || parameters == null
318: || parameters.getDeclaredVars().size() > 0
319: || parameters.getEntities().size() != 0) {
320: return null;
321: }
322:
323: CollectionSort ssort = FunctionFactory.getCollectionSort(
324: receiver.getSort(), receiver.getCollection()
325: .getCollectionType());
326:
327: assert ssort != null;
328:
329: Function f = (Function) services.getNamespaces()
330: .functions().lookup(
331: new Name(ssort.name().toString() + "::"
332: + name));
333:
334: return new OCLEntity(tf.createFunctionTerm(f, receiver
335: .getCollection().getFunctionalRestriction()));
336: }
337:
338: //oclIsKindOf------------------------------------------------------------
339: if (name.equals("oclIsKindOf")) {
340: if (!receiver.isTerm() || parameters == null
341: || !parameters.getDeclaredVars().isEmpty()
342: || !(parameters.getEntities().size() == 1)
343: || !(parameters.getEntities().head().isType())) {
344: return null;
345: }
346:
347: Function instance = (Function) services.getNamespaces()
348: .functions().lookup(
349: new Name(parameters.getEntities().head()
350: .getType().getFullName()
351: + "::instance"));
352:
353: Term result = tf.createFunctionTerm(instance, receiver
354: .getTerm());
355:
356: return new OCLEntity(result);
357: }
358:
359: //oclIsTypeOf------------------------------------------------------------
360: if (name.equals("oclIsTypeOf")) {
361: if (!receiver.isTerm() || parameters == null
362: || !parameters.getDeclaredVars().isEmpty()
363: || !(parameters.getEntities().size() == 1)
364: || !(parameters.getEntities().head().isType())) {
365: return null;
366: }
367:
368: Function instance = (Function) services.getNamespaces()
369: .functions().lookup(
370: new Name(parameters.getEntities().head()
371: .getType().getFullName()
372: + "::exactInstance"));
373:
374: Term result = tf.createFunctionTerm(instance, receiver
375: .getTerm());
376:
377: return new OCLEntity(result);
378: }
379:
380: //oclAsType------------------------------------------------------------
381: if (name.equals("oclAsType")) {
382: if (!receiver.isTerm() || parameters == null
383: || !parameters.getDeclaredVars().isEmpty()
384: || !(parameters.getEntities().size() == 1)
385: || !(parameters.getEntities().head().isType())) {
386: return null;
387: }
388:
389: Term result = tf
390: .createCastTerm((AbstractSort) parameters
391: .getEntities().head().getSort(), receiver
392: .getTerm());
393:
394: return new OCLEntity(result);
395: }
396:
397: //get (array access)------------------------------------------------------------
398: if (name.equals("get")) {
399: if (!receiver.isTerm() || parameters == null
400: || !parameters.getDeclaredVars().isEmpty()
401: || !(parameters.getEntities().size() == 1)
402: //|| !parameters.getEntities().head().getTerm().sort().name().toString().equals("int")
403: //|| !(receiver.getSort() instanceof ArraySort)#
404: ) {
405: return null;
406: }
407:
408: Term res = tf.createArrayTerm(ArrayOp.getArrayOp(receiver
409: .getSort()), receiver.getTerm(), parameters
410: .getEntities().head().getTerm());
411:
412: return new OCLEntity(res);
413: }
414:
415: //signals (exception-handling)--------------------------------------------------
416: if (name.equals("signals")) {
417: if (parameters == null
418: || !parameters.getDeclaredVars().isEmpty()
419: || !(parameters.getEntities().size() == 1)
420: || !parameters.getEntities().head().isType()) {
421: return null;
422: }
423:
424: Sort excSort = parameters.getEntities().head().getType()
425: .getSort();
426: Function instance = (Function) services.getNamespaces()
427: .functions().lookup(
428: new Name(excSort.name().toString()
429: + "::instance"));
430:
431: Term res = tb.and(tb.not(tb.equals(tb.var(excVar), tb
432: .NULL(services))), tb.equals(tb.func(instance, tb
433: .var(excVar)), tb.TRUE(services)));
434:
435: return new OCLEntity(res);
436:
437: }
438:
439: // modulo operation
440: if (name.equals("mod")) {
441: final IntegerLDT integerLDT = services.getTypeConverter()
442: .getIntegerLDT();
443: final Sort integerSort = integerLDT.targetSort();
444: if (!receiver.isTerm()
445: || parameters == null
446: || !(parameters.getEntities().size() == 1)
447: || !(receiver.getSort().extendsTrans(integerSort))
448: || !(parameters.getEntities().head().getSort()
449: .extendsTrans(integerSort))) {
450: return null;
451: }
452: return new OCLEntity(tb.func(integerLDT.getArithModulo(),
453: receiver.getTerm(), parameters.getEntities().head()
454: .getTerm()));
455: }
456:
457: // div operation
458: if (name.equals("div")) {
459: final IntegerLDT integerLDT = services.getTypeConverter()
460: .getIntegerLDT();
461: final Sort integerSort = integerLDT.targetSort();
462: if (!receiver.isTerm()
463: || parameters == null
464: || !(parameters.getEntities().size() == 1)
465: || !(receiver.getSort().extendsTrans(integerSort))
466: || !(parameters.getEntities().head().getSort()
467: .extendsTrans(integerSort))) {
468: return null;
469: }
470: return new OCLEntity(tb.func(integerLDT.getArithDivision(),
471: receiver.getTerm(), parameters.getEntities().head()
472: .getTerm()));
473: }
474:
475: /*
476: * TODO
477: *
478: //asSet------------------------------------------------------------
479: if(name.equals("asSet")) {
480: if(!receiver.isCollection()) {
481: return null;
482: }
483:
484: return new OCLEntity(receiver.getCollection().asSet());
485: }
486:
487:
488: //asBag------------------------------------------------------------
489: if(name.equals("asBag")) {
490: if(!receiver.isCollection()) {
491: return null;
492: }
493:
494: return new OCLEntity(receiver.getCollection().asBag());
495: }
496:
497:
498: //asSequence------------------------------------------------------------
499: if(name.equals("asSequence")) {
500: if(!receiver.isCollection()) {
501: return null;
502: }
503:
504: return new OCLEntity(receiver.getCollection().asSequence());
505: }
506: */
507:
508: return null;
509: }
510:
511: public boolean needVarDeclaration(String propertyName) {
512: return (propertyName.equals("forAll")
513: || propertyName.equals("exists")
514: || propertyName.equals("select")
515: || propertyName.equals("reject")
516: || propertyName.equals("collect") || propertyName
517: .equals("isUnique"));
518: }
519: }
|