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.proof.decproc;
12:
13: public abstract class DecisionProcedureICSOp {
14:
15: // OPERATORS
16: /** the ususal 'negation' operator '-' */
17: public static final String NOT = "~";
18: /** the ususal 'and' operator '/\' (be A, B formulae then 'A /\ B'
19: * is true if and only if A is true and B is true */
20: public static final String AND = "&";
21: /** the ususal 'or' operator '\/' (be A, B formulae then 'A \/ B'
22: * is true if and only if A is true or B is true */
23: public static final String OR = "|";
24: /** the ususal 'implication' operator '->' (be A, B formulae then
25: * 'A -> B' is true if and only if A is false or B is true */
26: public static final String IMP = "=>";
27: /** the ususal 'equivalence' operator '<->' (be A, B formulae then
28: * 'A <-> B' is true if and only if A and B have the same truth
29: * value */
30: public static final String EQV = "<=>";
31:
32: /** the usual arithmetic operations: */
33: public static final String PLUS = "+";
34: public static final String MINUS = "-";
35: public static final String MULT = "*";
36:
37: /** the ususal 'equality' operator '=' */
38: public static final String EQUALS = "=";
39: /** the ususal 'less than' operator '<' */
40: public static final String LT = "<";
41: /** the ususal 'greater than' operator '>' */
42: public static final String GT = ">";
43: /** the ususal 'less than or equal' operator '<=' */
44: public static final String LEQ = "<=";
45: /** the ususal 'greater than or equal' operator '>=' */
46: public static final String GEQ = ">=";
47:
48: /** the ususal 'forall' operator 'all' (be A a formula then
49: * 'all x.A' is true if and only if for all elements d of the
50: * universe A{x<-d} (x substitued with d) is true */
51: public static final String ALL = null;
52: /** the ususal 'exists' operator 'ex' (be A a formula then
53: * 'ex x.A' is true if and only if there is at least one elements
54: * d of the universe such that A{x<-d} (x substitued with d) is true */
55: public static final String EX = null;
56: /** the true constant */
57: public static final String TRUE = "tt";
58: /** the false constant */
59: public static final String FALSE = "ff";
60:
61: /** some facts about byte_MAX and friends */
62: public static final String LIMIT_FACTS = "";
63: /* + "assert byte_RANGE = 256."
64: + "assert short_RANGE = 65536."
65: + "assert int_RANGE = 4294967296."
66: + "assert long_RANGE = 18446744073709551616."
67: + "assert byte_HALFRANGE = 128."
68: + "assert short_HALFRANGE = 32768."
69: + "assert int_HALFRANGE = 2147483648."
70: + "assert long_HALFRANGE = 9223372036854775808."
71: + "assert byte_MIN = -128."
72: + "assert short_MIN = -32768."
73: + "assert int_MIN = -2147483648."
74: + "assert long_MIN = -9223372036854775808."
75: + "assert byte_MAX = 127."
76: + "assert short_MAX = 32767."
77: + "assert int_MAX = 2147483647."
78: + "assert long_MAX = 9223372036854775807."
79: + "\n";
80: */
81: }
|