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 de.uka.ilkd.key.casetool.Association;
021: import de.uka.ilkd.key.casetool.ListOfAssociation;
022: import de.uka.ilkd.key.casetool.UMLInfo;
023: import de.uka.ilkd.key.java.JavaInfo;
024: import de.uka.ilkd.key.java.Services;
025: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
026: import de.uka.ilkd.key.logic.Term;
027: import de.uka.ilkd.key.logic.TermFactory;
028: import de.uka.ilkd.key.logic.op.Function;
029: import de.uka.ilkd.key.logic.sort.AbstractCollectionSort;
030: import de.uka.ilkd.key.logic.sort.Sort;
031: import de.uka.ilkd.key.util.Debug;
032: import de.uka.ilkd.key.util.AssertionFailure;
033:
034: /**
035: * Resolves association accesses.
036: */
037: class AssociationResolver implements PropertyResolver {
038:
039: private static final TermFactory tf = TermFactory.DEFAULT;
040: private final Services services;
041: private final JavaInfo javaInfo;
042: private final UMLInfo umlInfo;
043:
044: public AssociationResolver(Services services) {
045: this .services = services;
046: this .javaInfo = services.getJavaInfo();
047: this .umlInfo = services.getUMLInfo();
048: assert javaInfo != null;
049: assert umlInfo != null;
050: }
051:
052: private static Function getAssociationFunction(Association assoc,
053: String name) {
054: Function assocFunction1 = assoc.getFunction1();
055: Function assocFunction2 = assoc.getFunction2();
056:
057: if (assocFunction1 != null && assocFunction2 != null) {
058: assert assocFunction1.arity() == 1
059: && assocFunction2.arity() == 1;
060:
061: return (assocFunction1.name().toString().equals(name) ? assocFunction1
062: : assocFunction2);
063: }
064:
065: return assoc.getPredicate();
066: }
067:
068: public OCLEntity resolve(OCLEntity receiver, String name,
069: OCLParameters parameters) throws OCLTranslationError {
070: if (parameters != null) {
071: return null;
072: }
073:
074: Sort containingSort = receiver.getSort();
075: KeYJavaType containingKjt = javaInfo
076: .getKeYJavaType(containingSort);
077: ListOfAssociation assocs = umlInfo.getAssociations(
078: containingKjt, name);
079:
080: if (!assocs.isEmpty()) {
081: Term recTerm = receiver.getTerm();
082: OCLCollection recCollection = receiver.getCollection();
083:
084: Association assoc = assocs.head();
085: Function assocFunc = getAssociationFunction(assoc, name);
086:
087: try {
088: if (recTerm != null) {
089: if (assocFunc.sort() instanceof AbstractCollectionSort) {
090: // we have a binary association with multiplicity greater than 1
091: OCLCollection collection = new OCLCollection(
092: recTerm, assoc, name);
093: return new OCLEntity(collection);
094: } else {
095: // either the association-end has multiplicity 1 or it is no binary association
096: Term functionTerm = tf.createFunctionTerm(
097: assocFunc, recTerm);
098: return new OCLEntity(functionTerm);
099: }
100: } else if (recCollection != null) {
101: OCLCollection newCollection = recCollection
102: .collect(services, assoc, name);
103: return new OCLEntity(newCollection);
104: }
105: } catch (Exception e) {
106: if (e instanceof OCLTranslationError) {
107: throw (OCLTranslationError) e;
108: }
109: }
110: }
111:
112: return null;
113: }
114:
115: public boolean needVarDeclaration(String propertyName) {
116: return false;
117: }
118: }
|