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.op;
12:
13: import de.uka.ilkd.key.logic.Name;
14: import de.uka.ilkd.key.logic.Named;
15: import de.uka.ilkd.key.logic.sort.Sort;
16: import de.uka.ilkd.key.logic.sort.SortDefiningSymbols;
17:
18: /**
19: * Interface for a class (function, predicate) from which instances
20: * exist for every sort (e.g. the functions/predicates of the
21: * collection sorts)
22: */
23: public interface SortDependingSymbol extends Named {
24:
25: /**
26: * @return the sort this object has been instantiated for
27: */
28: Sort getSortDependingOn();
29:
30: /**
31: * Compares "this" and "p"
32: * @param p object to compare
33: * @return true iff this and p are instances of the same kind of
34: * symbol, but possibly instantiated for different sorts
35: */
36: boolean isSimilar(SortDependingSymbol p);
37:
38: /**
39: * Assign a name to this term symbol, independant of concrete
40: * instantiations for different sorts
41: * @return the kind of term symbol this object is an instantiation
42: * for
43: */
44: Name getKind();
45:
46: /**
47: * Get the instance of this term symbol defined by the given sort
48: * "p_sort"
49: * @return a term symbol similar to this one, or null if this
50: * symbol is not defined by "p_sort"
51: *
52: * POSTCONDITION: result==null || (this.isSimilar(result) &&
53: * result.getSortDependingOn()==p_sort)
54: */
55: SortDependingSymbol getInstanceFor(SortDefiningSymbols p_sort);
56:
57: }
|