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: * Created on 15.06.2005
012: */package de.uka.ilkd.key.logic.sort;
013:
014: import java.util.Arrays;
015: import java.util.Comparator;
016: import java.util.LinkedList;
017: import java.util.List;
018:
019: import de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.logic.Name;
021: import de.uka.ilkd.key.logic.Namespace;
022: import de.uka.ilkd.key.util.Debug;
023:
024: /**
025: * <p>
026: * An intersection sort <code>I</code> is composed by exactly two sorts <code>S</code>,
027: * <code>T</code> and denotes their maximal subsort. This means, each sort being a subsort
028: * of both components extends (or is equal to) <code>I</code> as well.</p>
029: * <p>
030: * An intersection sort is always normalized during creation in order to keep consistent
031: * with the singleton property of sorts. That is to say that creation of the intersection
032: * sort (S,T) and (T,S), which denote obviously the same sort, returns the same sort object
033: * as they have the same normalform. </p>
034: * <p> The normalform is defined as follows:
035: * <ul>
036: * <li><tt>(S1,S2)</tt>,
037: * where <tt>S1</tt> must be a simple (non-intersection) sort; for
038: * <tt>S2</tt> there is no such restriction</li>
039: * <li><tt>S1</tt> is no subsort of <tt>S2</tt> and vice versa,
040: * i.e. intersection sorts are minimized</li>
041: * <li><tt>(S1,S2)</tt> are lexicographical ordered such that the name of <tt>S1</tt>
042: * is smaller than the name of sort <tt>S2</tt> (if <tt>S2</tt> is a simple sort)
043: * or otherwise smaller than any sort being a composite of sort <tt>S2</tt></li>
044: * </ul>
045: * If the normalform consists of exact one sort than the creation method of intersection
046: * sort returns the sort itself.</p>
047: * <p>An alternative definition of a normalform may use flattening, but
048: * would make matching of taclets more difficult. </p>
049: */
050: public class IntersectionSort extends AbstractSort {
051:
052: /**
053: * performs a lookup in the sort namespace and returns the
054: * intersection sort of the given sorts. If none exists a new
055: * intersection sort is created and added to the namespace.
056: * The created intersection sort is in normalform.
057: *
058: * @param sorts the SetOfSort whose intersection sort has to be determined
059: * @param services the Namespace with all known sorts to which if necessary
060: * the intersection sort of the given sorts is added
061: * @return the intersection sort of the given sorts.
062: */
063: public static Sort getIntersectionSort(SetOfSort sorts,
064: Services services) {
065: return rightAssoc(sort(flatten(minimize(sorts.toArray()))),
066: services);
067: }
068:
069: /**
070: * performs a lookup in the sort namespace and returns the
071: * intersection sort of the given sorts. If none exists a new
072: * intersection sort is created and added to the namespace.
073: * The created intersection sort is in normalform.
074: *
075: * @param components the SetOfSort whose intersection sort has to be determined
076: * @param sorts the Namespace with all known sorts to which if necessary
077: * the intersection sort of the given sorts is added
078: * @param functions the Namespace where to add the sort depending functions
079: * @return the intersection sort of the given sorts.
080: */
081: public static Sort getIntersectionSort(SetOfSort components,
082: Namespace sorts, Namespace functions) {
083: return rightAssoc(
084: sort(flatten(minimize(components.toArray()))), sorts,
085: functions);
086: }
087:
088: /**
089: * performs a lookup in the sort namespace and returns the
090: * intersection sort of the given sorts. If none exists a new
091: * intersection sort is created and added to the namespace.
092: * The created intersection sort is in normalform.
093: *
094: * @param s1 the first Sort
095: * @param s2 the second Sort
096: * @param sorts the Namespace with all known sorts to which if necessary
097: * the intersection sort of the given sorts is added
098: * @param functions the Namespace where to add sort depending functions like
099: * instance, casts etc.
100: * @return the intersection sort of the given sorts.
101: */
102: public static Sort getIntersectionSort(Sort s1, Sort s2,
103: Namespace sorts, Namespace functions) {
104:
105: Sort[] composites = flatten(minimize(new Sort[] { s1, s2 }));
106:
107: if (composites.length == 1) {
108: return composites[0];
109: } else if (composites.length > 2) {
110: return rightAssoc(composites, sorts, functions);
111: }
112:
113: final Name sortName = createSortName(composites);
114: Sort result = (Sort) sorts.lookup(sortName);
115: if (result == null) {
116: result = new IntersectionSort(sortName, composites[0],
117: composites[1]);
118: sorts.add(result);
119: ((IntersectionSort) result).addDefinedSymbols(functions,
120: sorts);
121: }
122:
123: return result;
124: }
125:
126: /**
127: * assumes all elements in <code>sorts</code> are non-intersection sorts
128: * returns the intersection sort of the given sorts
129: * @param components
130: * @return the intersection sort of the given sorts
131: */
132: private static Sort rightAssoc(Sort[] components, Services services) {
133: return rightAssoc(components, services.getNamespaces().sorts(),
134: services.getNamespaces().functions());
135: }
136:
137: /**
138: * assumes all elements in <code>sorts</code> are non-intersection sorts
139: * returns the intersection sort of the given sorts
140: * @param components
141: * @return the intersection sort of the given sorts
142: */
143: private static Sort rightAssoc(Sort[] components, Namespace sorts,
144: Namespace functions) {
145: Sort result = components[components.length - 1];
146: for (int i = components.length - 2; i >= 0; i--) {
147: result = getIntersectionSort(components[i], result, sorts,
148: functions);
149: }
150: return result;
151: }
152:
153: /**
154: * creates the sort name for the composites.
155: *
156: * @param composites2 the array of Sort with the defining
157: * composite sorts of this intersection sort
158: * @return the name of the intersection sort to be created
159: */
160: private static Name createSortName(Sort[] composites) {
161: final StringBuffer sortName = new StringBuffer("\\inter(");
162:
163: for (int i = 0; i < composites.length; i++) {
164: sortName.append(composites[i].name());
165: if (i < composites.length - 1) {
166: sortName.append(",");
167: }
168: }
169: sortName.append(")");
170:
171: return new Name(sortName.toString());
172: }
173:
174: /**
175: * To become independant of the order of the constituents we
176: * sort them in a lexicographical order.
177: * (assumes that different sorts have also different names).
178: * The used sorting algorithm is more or less a simple bubble sort
179: * as we (hopely) have only to compute the intersection of some
180: * few sorts.
181: * @param sorts ListOfSort the sorts to be sorted
182: * @return return the same array but sorted in the lexicographical
183: * order of the sorts names
184: */
185: private static Sort[] sort(Sort[] sorts) {
186: if (sorts.length <= 1)
187: return sorts;
188: Arrays.sort(sorts, LexicographicalComparator.DEFAULT);
189: return sorts;
190: }
191:
192: /**
193: * Removes all sorts of the given sorts that are a supersort
194: * of an existing one. For efficiency reasons flattening
195: * should be performed after minimizing.
196: * @param sorts the SetOfSorts to be minimized
197: * @return the minimized array of sorts
198: */
199: private static Sort[] minimize(Sort[] sorts) {
200: final List minimized = new LinkedList(Arrays.asList(sorts));
201:
202: // not optimized...
203: for (int i = 0; i < sorts.length; i++) {
204: final Sort s1 = sorts[i];
205: for (int j = i + 1; j < sorts.length; j++) {
206: final Sort s2 = sorts[j];
207: if (s2.extendsTrans(s1)) {
208: minimized.remove(s1);
209: break;
210: } else if (s1.extendsTrans(s2)) {
211: minimized.remove(s2);
212: }
213: }
214: }
215: return (Sort[]) minimized.toArray(new Sort[0]);
216: }
217:
218: /**
219: * flattens the given sorts by decomposing intersection
220: * sorts
221: * @param sorts the ListOfSort to be flattened
222: * @return the flattened list of sorts
223: * (i.e. means without subsorts)
224: */
225: private static Sort[] flatten(Sort[] sorts) {
226: List result = new LinkedList();
227: for (int i = 0; i < sorts.length; i++) {
228: if (!(sorts[i] instanceof IntersectionSort)) {
229: result.add(sorts[i]);
230: } else {
231: final IntersectionSort sortsIntersect = (IntersectionSort) sorts[i];
232: result.addAll(Arrays.asList(flatten(sortsIntersect
233: .compositesAsArray())));
234: }
235: }
236: return (Sort[]) result.toArray(new Sort[result.size()]);
237: }
238:
239: /**
240: * returns the composites as array
241: * @return the composites as array
242: */
243: private Sort[] compositesAsArray() {
244: return new Sort[] { leftComposite, rightComposite };
245: }
246:
247: /**
248: * left composite of this intersection sort. Has to be a simple sort,
249: * i.e. non composite sort
250: */
251: private final Sort leftComposite;
252: /**
253: * left composite of this intersection sort
254: * (may be simple or intersection sort)
255: */
256: private final Sort rightComposite;
257:
258: /** the non-intersection sorts this sort inherits of */
259: private SetOfSort extendsSorts = null;
260:
261: /**
262: * empty domain caches the computation if the domain of
263: * this intersection sort is empty
264: */
265: private boolean emptyDomainComputed;
266: private boolean emptyDomain;
267:
268: /**
269: * creates an intersection sort of the given name consisting of the
270: * given composite sorts. Does not perform any normalisation.
271: * @param name the Name of the intersection sort
272: * @param leftComposite the Sort to be intersected with
273: * <code>rightComposite</code> and is must not be
274: * of type intersection sort
275: * @param rightComposite an arbitrary Sort being intersected with
276: * <code>leftComposite</code>
277: */
278: private IntersectionSort(Name name, Sort leftComposite,
279: Sort rightComposite) {
280: super (name);
281: this .leftComposite = leftComposite;
282: Debug.assertFalse(leftComposite instanceof IntersectionSort);
283: this .rightComposite = rightComposite;
284:
285: }
286:
287: /**
288: * return the set of the 'real' sorts this
289: * intersection sort consists of (no intersection sorts)
290: */
291: public SetOfSort extendsSorts() {
292: if (extendsSorts == null) {
293: extendsSorts = SetAsListOfSort.EMPTY_SET.add(leftComposite);
294: if (rightComposite instanceof IntersectionSort) {
295: extendsSorts = extendsSorts.union(rightComposite
296: .extendsSorts());
297: } else {
298: extendsSorts = extendsSorts.add(rightComposite);
299: }
300: extendsSorts = asSet(minimize(extendsSorts.toArray()));
301: }
302: return extendsSorts;
303: }
304:
305: /**
306: * returns the <code>i</code>-th component of this intersection sort
307: * (where 0 is left component and 1 is the right component)
308: *
309: * @return the <code>i</code>-th component of this intersection sort
310: * @throws IndexOutOfBoundsException if <code>i</code> is greater than 1
311: */
312: public Sort getComponent(int i) {
313: if (i < 0 || i > 1) {
314: throw new IndexOutOfBoundsException(i + " is out of bound.");
315: }
316: return i == 0 ? leftComposite : rightComposite;
317: }
318:
319: /**
320: * returns the number of composites (always two)
321: */
322: public int memberCount() {
323: return 2;
324: }
325:
326: /**
327: * returns true iff the given sort is a transitive supersort of this sort
328: * or it is the same.
329: */
330: public boolean extendsTrans(Sort p_sort) {
331: if (p_sort == this || p_sort == Sort.ANY)
332: return true;
333:
334: boolean extendsTrans = true;
335:
336: /**
337: * for all s\in sort.composites
338: * exists c\in this.composites
339: * c.extendsTrans(s)
340: */
341: if (p_sort instanceof IntersectionSort) {
342: final IntersectionSort p_intersect = ((IntersectionSort) p_sort);
343: for (int i = 0, mc = p_intersect.memberCount(); i < mc; i++) {
344: final Sort p_composite = p_intersect.getComponent(i);
345: extendsTrans = extendsTrans
346: && this .extendsTransHelp(p_composite);
347: if (!extendsTrans)
348: break;
349: }
350: } else {
351: extendsTrans = extendsTransHelp(p_sort);
352: }
353:
354: return extendsTrans;
355: }
356:
357: /**
358: * tests if one of the composites is a subsort (or equal) of the given one
359: * @param sort the Sort to test to be a supersort (or equal) of one of the
360: * composites
361: * @return true if sort is a supersort of one of the composites (inclusive equal to)
362: */
363: private boolean extendsTransHelp(Sort sort) {
364: for (int i = 0, sz = memberCount(); i < sz; i++) {
365: if (getComponent(i).extendsTrans(sort)) {
366: return true;
367: }
368: }
369: return false;
370: }
371:
372: /**
373: * returns true if the represented domain is empty. If you consider other logics
374: * than JavaCardDL you will most probably have to subclass IntersectionSort and
375: * overwrite this method.
376: * @return true if other than reference types, which are siblings in the type hierarchy,
377: * intersect
378: */
379: public boolean hasEmptyDomain() {
380: if (emptyDomainComputed)
381: return emptyDomain;
382:
383: boolean nonReferenceType = false;
384: emptyDomain = false;
385:
386: for (int i = 0, sz = memberCount(); i < sz; i++) {
387: final Sort s = getComponent(i);
388: Debug.assertTrue(!(s instanceof GenSort),
389: "Cannot compute iff a domain is empty "
390: + "in case of generic sorts.");
391: if (s instanceof PrimitiveSort) {
392: nonReferenceType = true;
393: } else if (s instanceof IntersectionSort) {
394: // due to normalform and JavaCardDL type system we know
395: // intersection of
396: // * primitive sorts have an empty domain iff
397: // they do not subclass each other but intersection of
398: // sorts in a vertical line are never an IntersectionSort
399: // * intersection of primitive and object have empty domain
400: // thus we can derive from a non-empty domain that the
401: // composites are of type ObjectSort
402: final IntersectionSort s_intersect = (IntersectionSort) s;
403: if (s_intersect.hasEmptyDomain()) {
404: emptyDomainComputed = true;
405: emptyDomain = true;
406: break;
407: } else {
408: if (nonReferenceType) {
409: emptyDomainComputed = true;
410: emptyDomain = true;
411: break;
412: }
413: }
414: }
415: }
416: emptyDomainComputed = true;
417: return emptyDomain;
418: }
419:
420: /**
421: * toString
422: */
423: public String toString() {
424: return name().toString();
425: }
426:
427: // helper
428: /**
429: * converts the given array of sorts into a {@link SetOfSort}
430: */
431: private static SetOfSort asSet(Sort[] s) {
432: SetOfSort set = SetAsListOfSort.EMPTY_SET;
433: for (int i = 0; i < s.length; i++) {
434: set = set.add(s[i]);
435: }
436: return set;
437: }
438:
439: // Some comparators used for determining the minimal supersort to be created
440:
441: /**
442: * compares to sorts using the canonical lexicographical order on their names
443: */
444: private final static class LexicographicalComparator implements
445: Comparator {
446:
447: public static final LexicographicalComparator DEFAULT = new LexicographicalComparator();
448:
449: public int compare(Object o1, Object o2) {
450: final Sort s1 = (Sort) o1;
451: final Sort s2 = (Sort) o2;
452: return s1.name().toString().compareTo(s2.name().toString());
453: }
454: }
455:
456: }
|