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.java.JavaInfo;
021: import de.uka.ilkd.key.java.Services;
022: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
023: import de.uka.ilkd.key.logic.Term;
024: import de.uka.ilkd.key.util.AssertionFailure;
025:
026: /**
027: * Resolves method (query) calls.
028: */
029: class MethodResolver implements PropertyResolver {
030:
031: private final Services services;
032: private final JavaInfo javaInfo;
033: private final FormulaBoolConverter fbc;
034:
035: public MethodResolver(Services services, FormulaBoolConverter fbc) {
036: this .services = services;
037: this .javaInfo = services.getJavaInfo();
038: this .fbc = fbc;
039: }
040:
041: private boolean isFullyQualified(String name) {
042: return name.indexOf("::") >= 0;
043: }
044:
045: private String extractTypeName(String fullyQualifiedName) {
046: return fullyQualifiedName.substring(0, fullyQualifiedName
047: .indexOf("::"));
048: }
049:
050: private String extractPropertyName(String fullyQualifiedName) {
051: return fullyQualifiedName.substring(fullyQualifiedName
052: .indexOf("::") + 2);
053: }
054:
055: public OCLEntity resolve(OCLEntity receiver, String name,
056: OCLParameters parameters) throws OCLTranslationError {
057: if (parameters == null
058: || !parameters.getDeclaredVars().isEmpty()) {
059: return null;
060: }
061:
062: String containingName;
063: if (isFullyQualified(name)) {
064: containingName = extractTypeName(name);
065: name = extractPropertyName(name);
066: } else {
067: KeYJavaType containingType = javaInfo
068: .getKeYJavaType(receiver.getSort());
069: if (containingType == null) {
070: return null;
071: }
072: containingName = containingType.getFullName();
073: }
074:
075: Term[] args = fbc.convertFormulasToBool(
076: parameters.getEntities()).toArray();
077:
078: Term recTerm = receiver.getTerm();
079: KeYJavaType recType = receiver.getType();
080: OCLCollection recCollection = receiver.getCollection();
081: try {
082: if (recTerm != null || recType != null) {
083:
084: Term methodTerm = javaInfo.getProgramMethodTerm(
085: receiver.getTerm(), name, args, containingName);
086:
087: return new OCLEntity(methodTerm);
088: } else if (recCollection != null) {
089: Term recVarTerm = recCollection.getPredVarAsTerm();
090: Term methodTerm = javaInfo.getProgramMethodTerm(
091: recVarTerm, name, args, containingName);
092: OCLCollection newCollection = recCollection.collect(
093: services, methodTerm);
094: return new OCLEntity(newCollection);
095: }
096: } catch (Exception e) {
097: if (e instanceof OCLTranslationError) {
098: throw (OCLTranslationError) e;
099: }
100: }
101:
102: return null;
103: }
104:
105: public boolean needVarDeclaration(String propertyName) {
106: return false;
107: }
108: }
|