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.java.Services;
022: import de.uka.ilkd.key.logic.Term;
023: import de.uka.ilkd.key.logic.TermFactory;
024: import de.uka.ilkd.key.logic.op.Function;
025: import de.uka.ilkd.key.logic.op.LogicVariable;
026: import de.uka.ilkd.key.logic.sort.Sort;
027: import de.uka.ilkd.key.util.Debug;
028:
029: /**
030: * This class represents the CollectionType of OCL.
031: *
032: */
033: class OCLCollection {
034:
035: public static final int OCL_SET = 0;
036: public static final int OCL_BAG = 1;
037: public static final int OCL_SEQUENCE = 2;
038:
039: private final OCLPredicativeCollection predInterpretation;
040: private final OCLFunctionalCollection funcInterpretation;
041:
042: /**
043: * Creates a collection which contains all values of a sort which satisfy
044: * some restriction. Functional and predicative interpretation are explicitly given.
045: *
046: * @param var
047: * @param pRestriction predicative restriction
048: * @param fRestriction functional restriction
049: * @param collectionType type of this Collection
050: */
051: private OCLCollection(LogicVariable var, Term pRestriction,
052: Term fRestriction, int collectionType) {
053: predInterpretation = new OCLPredicativeCollection(var,
054: pRestriction);
055: funcInterpretation = new OCLFunctionalCollection(fRestriction,
056: collectionType);
057: }
058:
059: /**
060: * Creates an empty collection of type <b>collectionType</b>.
061: */
062: public OCLCollection(int collectionType) {
063: predInterpretation = new OCLPredicativeCollection();
064: funcInterpretation = new OCLFunctionalCollection(collectionType);
065: }
066:
067: /**
068: * Creates an empty set.
069: */
070: public OCLCollection() {
071: this (OCL_SET);
072: }
073:
074: /**
075: * Creates a set which contains all values of a sort which are not null.
076: */
077: public OCLCollection(Sort sort, Services services) {
078: this (sort, OCL_SET, services);
079: }
080:
081: /**
082: * Creates a collection which contains all values of a sort which are not null
083: */
084: public OCLCollection(Sort sort, int collectionType,
085: Services services) {
086: predInterpretation = new OCLPredicativeCollection(sort,
087: services);
088: funcInterpretation = new OCLFunctionalCollection(sort,
089: collectionType);
090: }
091:
092: /**
093: * Creates a collection which contains a single element.
094: * @throws OCLTranslationError
095: */
096: public OCLCollection(Term element, int collectionType)
097: throws OCLTranslationError {
098: predInterpretation = new OCLPredicativeCollection(element);
099: funcInterpretation = new OCLFunctionalCollection(
100: collectionType, element);
101: }
102:
103: /**
104: * Creates a set which contains a single element.
105: * @throws OCLTranslationError
106: */
107: public OCLCollection(Term element) throws OCLTranslationError {
108: this (element, OCL_SET);
109: }
110:
111: /**
112: * Creates a collection which contains all integers between a lower and
113: * an upper bound (described by terms of sort int).
114: * @throws OCLTranslationError
115: */
116: public OCLCollection(Term lowerBound, Term upperBound,
117: Function leq, int collectionType)
118: throws OCLTranslationError {
119: predInterpretation = new OCLPredicativeCollection(lowerBound,
120: upperBound, leq);
121: funcInterpretation = new OCLFunctionalCollection(lowerBound,
122: upperBound, leq, collectionType);
123: }
124:
125: /**
126: * Creates a set which contains all integers between a lower and
127: * an upper bound (described by terms of sort int).
128: * @throws OCLTranslationError
129: */
130: public OCLCollection(Term lowerBound, Term upperBound, Function leq)
131: throws OCLTranslationError {
132: this (lowerBound, upperBound, leq, OCL_SET);
133: }
134:
135: /**
136: * Creates a collection which contains all values reachable from a receiver
137: * term by applying an association with multiplicity > 1 (described by a
138: * predicate).
139: */
140: public OCLCollection(Term recTerm, Association assoc, String name) {
141: predInterpretation = new OCLPredicativeCollection(recTerm,
142: assoc.getPredicate());
143: funcInterpretation = new OCLFunctionalCollection(recTerm,
144: getAssociationFunction(assoc, name));
145: }
146:
147: private OCLCollection(OCLPredicativeCollection pc,
148: OCLFunctionalCollection fc) {
149: this .predInterpretation = pc;
150: this .funcInterpretation = fc;
151: }
152:
153: public LogicVariable getPredVar() {
154: return predInterpretation.getVar();
155: }
156:
157: public Term getPredVarAsTerm() {
158: return predInterpretation.getVarAsTerm();
159: }
160:
161: public Sort getElementSort() {
162: return predInterpretation.getSort();
163: }
164:
165: public int getCollectionType() {
166: return funcInterpretation.getCollectionType();
167: }
168:
169: public Term getFunctionalRestriction() {
170: return funcInterpretation.getRestriction();
171: }
172:
173: public Term getPredicativeRestriction() {
174: return predInterpretation.getRestriction();
175: }
176:
177: public boolean isSet() {
178: return funcInterpretation.isSet();
179: }
180:
181: public boolean isBag() {
182: return funcInterpretation.isBag();
183: }
184:
185: public boolean isSequence() {
186: return funcInterpretation.isSequence();
187: }
188:
189: public String toString() {
190: return "OCLCollection\npredicative: " + predInterpretation
191: + "\nfunctional: " + funcInterpretation + "\n";
192: }
193:
194: /**
195: * Creates a collection which is the union of this one and another one.
196: *
197: * @param c collection to union with
198: * @return Collection containing all the elements from <b>this</b> and <b>c</b>
199: * @throws OCLTranslationError
200: */
201: public OCLCollection union(OCLCollection c)
202: throws OCLTranslationError {
203: return new OCLCollection(getPredVar(), predInterpretation
204: .union(c).getRestriction(), funcInterpretation.union(c)
205: .getRestriction(), getCollectionType());
206: }
207:
208: /**
209: * Creates the collection which results from the call
210: * c->collect(b|e) alias c->collect(e) or c.e
211: * where c is <b>this</b>
212: *
213: * @param services global services
214: * @param collectTerm e
215: * @return the appropriate collection
216: * @throws OCLTranslationError
217: */
218: public OCLCollection collect(Services services, Term collectTerm)
219: throws OCLTranslationError {
220:
221: OCLPredicativeCollection pc = predInterpretation.navigate(
222: services, collectTerm);
223: OCLFunctionalCollection fc = funcInterpretation
224: .collect(collectTerm);
225:
226: return new OCLCollection(pc, fc);
227: }
228:
229: /**
230: * Creates the collection which results from applying an association
231: * to this collection
232: *
233: * @param services global services
234: * @param assoc the Association over which is navigated
235: * @return the appropriate collection (hopefully) :)
236: * @throws OCLTranslationError
237: */
238: public OCLCollection collect(Services services, Association assoc,
239: String name) throws OCLTranslationError {
240:
241: Function assocFunc = getAssociationFunction(assoc, name);
242:
243: // This should be allowed!
244: //if (assocFunc.sort() instanceof AbstractCollectionSort) {
245: //result would be a set of sets => not supported!
246: // Debug.fail("OCLCollection: Sets of sets are not supported!");
247: // return null;
248: //}
249:
250: OCLPredicativeCollection pc = predInterpretation.navigate(
251: services, assoc.getPredicate());
252: OCLFunctionalCollection fc = funcInterpretation
253: .collect(TermFactory.DEFAULT.createFunctionTerm(
254: assocFunc, getPredVarAsTerm()));
255:
256: return new OCLCollection(pc, fc);
257: }
258:
259: /**
260: * Creates the flattened collection which results from applying an association
261: * to this collection (described by a OCLCollection)
262: *
263: * @param services global services
264: * @param collection the applied association
265: * @return the appropriate collection (hopefully) :)
266: */
267: public OCLCollection collect(Services services,
268: OCLCollection collection) {
269: // TODO Auto-generated method stub
270: return null;
271: }
272:
273: /**
274: * Creates the collection which results from the call
275: * c->select(b|e) alias c->select(e)
276: *
277: * @param selectVar variable used in e for referring to the instances of c
278: * @param selectTerm e
279: * @return the appropriate collection
280: * @throws OCLTranslationError
281: */
282: public OCLCollection select(LogicVariable selectVar, Term selectTerm)
283: throws OCLTranslationError {
284:
285: OCLPredicativeCollection pc = predInterpretation
286: .narrow(selectTerm);
287: OCLFunctionalCollection fc = funcInterpretation.select(
288: selectVar, selectTerm);
289:
290: return new OCLCollection(pc, fc);
291: }
292:
293: private static Function getAssociationFunction(Association assoc,
294: String name) {
295: Function assocFunction1 = assoc.getFunction1();
296: Function assocFunction2 = assoc.getFunction2();
297:
298: if (assocFunction1 != null && assocFunction2 != null) {
299: assert assocFunction1.arity() == 1
300: && assocFunction2.arity() == 1;
301:
302: return (assocFunction1.name().toString().equals(name) ? assocFunction1
303: : assocFunction2);
304: }
305:
306: return assoc.getPredicate();
307: }
308: }
|