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;
12:
13: import de.uka.ilkd.key.logic.Name;
14: import de.uka.ilkd.key.logic.Named;
15: import de.uka.ilkd.key.logic.op.Equality;
16: import de.uka.ilkd.key.logic.op.Op;
17:
18: public interface Sort extends Named {
19:
20: Sort FORMULA = new PrimitiveSort(new Name("Formula"));
21: Sort NULL = new NullSortImpl(new Name("Null"));
22: /** this sort is the mother of all sorts for java dl
23: * TODO: should OCLSorts extendTrans this sort too?
24: */
25: Sort ANY = new AbstractNonCollectionSort(new Name("any")) {
26:
27: public SetOfSort extendsSorts() {
28: return SetAsListOfSort.EMPTY_SET;
29: }
30:
31: public boolean extendsTrans(Sort s) {
32: return s == this ;
33: }
34:
35: public Equality getEqualitySymbol() {
36: return Op.EQUALS;
37: }
38:
39: };
40:
41: /** @return name of the Sort */
42: Name name();
43:
44: /**
45: * For finding out whether a certain sort is super- or subsort of another
46: * sort or not, please use <code>extendsTrans</code>.
47: * Using <code>extendsSorts()</code> for this purpose may lead to
48: * undesired results when dealing with array- and intersection sorts!
49: * @return the sorts of the predecessors of this sort
50: */
51: SetOfSort extendsSorts();
52:
53: /**
54: * returns true iff the given sort is a transitive supersort of this sort
55: * or it is the same.
56: */
57: boolean extendsTrans(Sort s);
58:
59: /** @return equality symbol of this sort */
60: Equality getEqualitySymbol();
61:
62: }
|