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: * Created on 13.06.2005
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.ObjectSort;
16: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
17: import de.uka.ilkd.key.logic.sort.Sort;
18:
19: /**
20: * This function symbol is created for casts to the depending sort.
21: * An implicit restriction belongs to the arguments sorts. We will
22: * forbid side casts from reference types to primtive types as this
23: * usually indicates an error. But it should be stressed that the calculus
24: * itself would remain sound even if we would syntactically allow such kind
25: * of casts.
26: */
27: public class CastFunctionSymbol extends SortDependingFunction {
28:
29: public static final Name NAME = new Name("cast");
30:
31: /**
32: * creates an instance of a cast
33: * @param argSort the Sort of the argument (usually any)
34: * @param castSort the Sort to be casted to
35: */
36: public CastFunctionSymbol(Sort argSort, Sort castSort) {
37: super (new Name(castSort + "::" + NAME), castSort,
38: new Sort[] { argSort }, NAME, castSort);
39: }
40:
41: /**
42: * overrides method in {@link de.uka.ilkd.key.logic.op.Function} and
43: * inserts an additional check disallowing which disallows side casts
44: * between primitive and reference types
45: * @param at an int describing the planned sub term position of the given term
46: * @param possibleSub the Term designated to become the at-th sub term
47: * @return an boolean indicating if the given term is allowed at the
48: * given position
49: */
50: public boolean possibleSub(int at, Term possibleSub) {
51: final Sort castTo = getSortDependingOn();
52: return super .possibleSub(at, possibleSub)
53: && ((castTo instanceof PrimitiveSort) != (castTo instanceof ObjectSort));
54: }
55:
56: /** toString */
57: public String toString() {
58: return "(" + getSortDependingOn() + ")";
59: }
60: }
|