01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09: //
10:
11: package de.uka.ilkd.key.logic.sort.oclsort;
12:
13: import de.uka.ilkd.key.logic.Name;
14: import de.uka.ilkd.key.logic.op.Equality;
15: import de.uka.ilkd.key.logic.op.Op;
16: import de.uka.ilkd.key.logic.sort.*;
17:
18: public class OclAnySort implements OclSort {
19:
20: private Name name;
21:
22: public OclAnySort(Name name) {
23: this .name = name;
24: }
25:
26: /** @return name of the Sort */
27: public Name name() {
28: return name;
29: }
30:
31: /**
32: * For finding out whether a certain sort is super- or subsort of another
33: * sort or not, please use <code>extendsTrans</code>.
34: * Using <code>extendsSorts()</code> for this purpose may lead to
35: * undesired results when dealing with arraysorts!
36: * @return the sorts of the predecessors of this sort
37: */
38: public SetOfSort extendsSorts() {
39: return SetAsListOfSort.EMPTY_SET;
40: }
41:
42: /**
43: * returns true iff the given sort is a transitive supersort of this sort
44: * or it is the same.
45: */
46: public boolean extendsTrans(Sort s) {
47: if (s instanceof OclGenericSort) {
48: return true;
49: } else if (s instanceof GenericSort) {
50: if (((GenericSort) s).getOneOf().size() == 0) {
51: return true;
52: } else {
53: IteratorOfSort iter = ((GenericSort) s).getOneOf()
54: .iterator();
55: while (iter.hasNext()) {
56: if (this .extendsTrans(iter.next())) {
57: return true;
58: }
59: }
60: return false;
61: }
62: } else {
63: return s.getClass().isInstance(this );
64: }
65: }
66:
67: /** @return equality symbol of this sort */
68: public Equality getEqualitySymbol() {
69: return Op.EQUALS;
70: }
71:
72: public String toString() {
73: return name.toString();
74: }
75: }
|