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.Term;
15: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
16: import de.uka.ilkd.key.logic.sort.Sort;
17:
18: /**
19: * Objects of this class represent the (logical) instanceof-operator;
20: * for each object sort such an operator exists
21: */
22: public class InstanceofSymbol extends SortDependingFunction {
23:
24: public static final Name NAME = new Name("instance");
25:
26: public InstanceofSymbol(Sort p_sort, Sort booleanSort) {
27: super (new Name("" + p_sort.name() + "::" + NAME), booleanSort,
28: new Sort[] { Sort.ANY }, NAME, p_sort);
29: }
30:
31: public InstanceofSymbol(Name name, Sort p_sort) {
32: super (new Name("" + p_sort.name() + "::" + name), Sort.FORMULA,
33: new Sort[] { Sort.ANY }, name, p_sort);
34: }
35:
36: /**
37: * only type tests mixing primitive and reference types are omitted
38: */
39: public boolean possibleSub(int at, Term possibleSub) {
40: if (possibleSub.op() instanceof SchemaVariable) {
41: return true;
42: }
43: return (possibleSub.sort() instanceof PrimitiveSort) == (getSortDependingOn() instanceof PrimitiveSort);
44: }
45:
46: }
|