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: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
11: // and Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16:
17: package de.uka.ilkd.key.parser.jml;
18:
19: import de.uka.ilkd.key.logic.Namespace;
20: import de.uka.ilkd.key.logic.op.Function;
21:
22: public interface ArithOpProvider {
23:
24: public Namespace getFunctions();
25:
26: public void setFunctions(Namespace functions);
27:
28: public Function getAdd(boolean l);
29:
30: public Function getSub(boolean l);
31:
32: public Function getMinus(boolean l);
33:
34: public Function getMul(boolean l);
35:
36: public Function getDiv(boolean l);
37:
38: public Function getMod(boolean l);
39:
40: public Function getOr(boolean l);
41:
42: public Function getAnd(boolean l);
43:
44: public Function getXor(boolean l);
45:
46: public Function getNeg(boolean l);
47:
48: public Function getShiftRight(boolean l);
49:
50: public Function getShiftLeft(boolean l);
51:
52: public Function getMin(boolean l);
53:
54: public Function getMax(boolean l);
55:
56: public Function getCastToByte();
57:
58: public Function getCastToShort();
59:
60: public Function getCastToInt();
61:
62: public Function getCastToLong();
63:
64: public Function getUnsignedShiftRight(boolean l);
65:
66: }
|