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.SetAsListOfSort;
17: import de.uka.ilkd.key.logic.sort.SetOfSort;
18: import de.uka.ilkd.key.logic.sort.Sort;
19:
20: public class OclGenericSort implements OclSort {
21:
22: private Name name;
23:
24: public OclGenericSort(Name name) {
25: this .name = name;
26: }
27:
28: /** @return name of the Sort */
29: public Name name() {
30: return name;
31: }
32:
33: /**
34: * For finding out whether a certain sort is super- or subsort of another
35: * sort or not, please use <code>extendsTrans</code>.
36: * Using <code>extendsSorts()</code> for this purpose may lead to
37: * undesired results when dealing with arraysorts!
38: * @return the sorts of the predecessors of this sort
39: */
40: public SetOfSort extendsSorts() {
41: return SetAsListOfSort.EMPTY_SET;
42: }
43:
44: /**
45: * returns true iff the given sort is a transitive supersort of this sort
46: * or it is the same.
47: */
48: public boolean extendsTrans(Sort s) {
49: return true;
50: }
51:
52: /** @return equality symbol of this sort */
53: public Equality getEqualitySymbol() {
54: return Op.EQUALS;
55: }
56:
57: public String toString() {
58: return name.toString();
59: }
60: }
|