001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.service.logic;
017
018 import org.qedeq.kernel.se.common.ErrorCodes;
019
020 /**
021 * Error codes and messages for service package.
022 *
023 * @author Michael Meyling
024 */
025 public interface LogicErrors extends ErrorCodes {
026
027 /** Error code. */
028 public static final int IDENTITY_OPERATOR_ALREADY_EXISTS_CODE = 123476;
029
030 /** Error message. */
031 public static final String IDENTITY_OPERATOR_ALREADY_EXISTS_TEXT
032 = "identity operator already defined with";
033
034
035 /** Error code. */
036 public static final int PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_CODE = 30810;
037
038 /** Error message. */
039 public static final String PREDICATE_DEFINITION_NEEDS_EQUIVALENCE_OPERATOR_TEXT
040 = "a predicate definition needs an equivalence relation (with two parameters)";
041
042
043 /** Error code. */
044 public static final int PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_CODE = 30810;
045
046 /** Error message. */
047 public static final String PREDICATE_DEFINITION_NEEDS_PREDICATE_CONSTANT_TEXT
048 = "a predicate definition needs an predicate constant as the first parameter";
049
050
051 /** Error code. */
052 public static final int MUST_HAVE_NAME_OF_PREDICATE_CODE = 40720;
053
054 /** Error message. */
055 public static final String MUST_HAVE_NAME_OF_PREDICATE_TEXT
056 = "predicate name found is not as expected: ";
057
058
059 /** Error code. */
060 public static final int FUNCTION_ALREADY_DEFINED_CODE = 40400;
061
062 /** Error message. */
063 public static final String FUNCTION_ALREADY_DEFINED_TEXT
064 = "function was already defined for this argument number: ";
065
066
067 /** Error code. */
068 public static final int NO_DEFINITION_FORMULA_FOR_FUNCTION_CODE = 40730;
069
070 /** Error message. */
071 public static final String NO_DEFINITION_FORMULA_FOR_FUNCTION_TEXT
072 = "no definition formula for new function found";
073
074
075 /** Error code. */
076 public static final int DEFINITION_FORMULA_FOR_FUNCTION_MUST_START_WITH_EQUAL_RELATION_CODE = 40740;
077
078 /** Error message. */
079 public static final String DEFINITION_FORMULA_FOR_FUNCTION_MUST_START_WITH_EQUAL_RELATION_TEXT
080 = "definition formula for new function must start with an equal relation";
081
082
083 /** Error code. */
084 public static final int PREDICATE_ALREADY_DEFINED_CODE = 40400;
085
086 /** Error message. */
087 public static final String PREDICATE_ALREADY_DEFINED_TEXT
088 = "predicate was already defined for this argument number: ";
089
090
091 /** Error code. */
092 public static final int MUST_BE_A_SUBJECT_VARIABLE_CODE = 40500;
093
094 /** Error message. */
095 public static final String MUST_BE_A_SUBJECT_VARIABLE_TEXT
096 = "a subject variable was expected here, but we found: ";
097
098
099 /** Error code. */
100 public static final int SUBJECT_VARIABLE_OCCURS_NOT_FREE_CODE = 40510;
101
102 /** Error message. */
103 public static final String SUBJECT_VARIABLE_OCCURS_NOT_FREE_TEXT
104 = "subject variable doesn't occur free in formula or term: ";
105
106
107 /** Error code. */
108 public static final int NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_CODE = 40520;
109
110 /** Error message. */
111 public static final String NUMBER_OF_FREE_SUBJECT_VARIABLES_NOT_EQUAL_TEXT
112 = "number of subject variables in definition not equal to number of free subject variables of formula or term";
113
114
115 /** Error code. */
116 public static final int IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_CODE = 40530;
117
118 /** Error message. */
119 public static final String IDENTITY_OPERATOR_MUST_BE_DEFINED_FIRST_TEXT
120 = "the identity operator must be defined firstly before you can define a function constant";
121
122
123 /** Error code. */
124 public static final int DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_CODE = 40540;
125
126 /** Error message. */
127 public static final String DEFINITION_FORMULA_FOR_FUNCTION_MUST_BE_AN_EQUAL_RELATION_TEXT
128 = "a function definition must be an equal relation";
129
130
131 /** Error code. */
132 public static final int FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_CODE = 40550;
133
134 /** Error message. */
135 public static final String FIRST_OPERAND_MUST_BE_A_NEW_FUNCTION_CONSTANT_TEXT
136 = "first operand of equal relation must be the new function constant";
137
138
139 /** Error code. */
140 public static final int SECOND_OPERAND_MUST_BE_A_TERM_CODE = 40560;
141
142 /** Error message. */
143 public static final String SECOND_OPERAND_MUST_BE_A_TERM_TEXT
144 = "first operand of equal relation must be the new function constant";
145
146
147 /** Error code. */
148 public static final int MODULE_IMPORT_CHECK_FAILED_CODE = 11231;
149
150 /** Error message. */
151 public static final String MODULE_IMPORT_CHECK_FAILED_TEXT
152 = "import check failed: ";
153
154
155 /** Error code. */
156 public static final int PROPOSITION_FORMULA_MUST_NOT_BE_NULL_CODE = 37230;
157
158 /** Error message. */
159 public static final String PROPOSITION_FORMULA_MUST_NOT_BE_NULL_TEXT
160 = "proposition formula must not be null";
161
162
163 /** Error code. */
164 public static final int NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE = 37250;
165
166 /** Error message. */
167 public static final String NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT
168 = "only nodes with well formed formulas can be checked";
169
170
171 /** Error code. */
172 public static final int NO_FORMAL_PROOF_FOUND_CODE = 37240;
173
174 /** Error message. */
175 public static final String NO_FORMAL_PROOF_FOUND_TEXT
176 = "no correct formal proof found";
177
178
179 /** Error code. */
180 public static final int RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_CODE = 37250;
181
182 /** Error message. */
183 public static final String RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_TEXT
184 = "this rule version has still no proof checker implementation: ";
185
186
187 /** Error code. */
188 public static final int RULE_ALREADY_DEFINED_CODE = 37260;
189
190 /** Error message. */
191 public static final String RULE_ALREADY_DEFINED_TEXT
192 = "rule was already defined for this version: ";
193
194
195 /** Error code. */
196 public static final int RULE_DEFINITIONS_DONT_MIX_CODE = 37270;
197
198 /** Error message. */
199 public static final String RULE_DEFINITIONS_DONT_MIX_TEXT
200 = "rule version was defined in different modules: ";
201
202
203 /** Error code. */
204 public static final int CLASS_OPERATOR_ALREADY_DEFINED_CODE = 123478;
205
206 /** Error message. */
207 public static final String CLASS_OPERATOR_ALREADY_DEFINED_TEXT
208 = "class operator already defined within this module: ";
209
210
211 /** Error code. */
212 public static final int THIS_IS_NOT_VALID_VERSION_FORMAT_CODE = 37300;
213
214 /** Error message. */
215 public static final String THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT
216 = "a version must be formed like a.b.c with nonegative integers a, b, c; out problem is: ";
217
218
219 /** Error code. */
220 public static final int MODULE_HAS_NO_HEADER_CODE = 37310;
221
222 /** Error message. */
223 public static final String MODULE_HAS_NO_HEADER_TEXT
224 = "module has no header";
225
226
227 /** Error code. */
228 public static final int MODULE_HAS_NO_HEADER_SPECIFICATION_CODE = 37320;
229
230 /** Error message. */
231 public static final String MODULE_HAS_NO_HEADER_SPECIFICATION_TEXT
232 = "module has no header specification";
233
234
235 /** Error code. */
236 public static final int RULE_WAS_NOT_DECLARED_BEFORE_CODE = 37330;
237
238 /** Error message. */
239 public static final String RULE_WAS_NOT_DECLARED_BEFORE_TEXT
240 = "a rule with this name was not declared yet: ";
241
242
243 /** Error code. */
244 public static final int RULE_HAS_BEEN_DECLARED_BEFORE_CODE = 37340;
245
246 /** Error message. */
247 public static final String RULE_HAS_BEEN_DECLARED_BEFORE_TEXT
248 = "a rule with this version was already declared: ";
249
250
251 /** Error code. */
252 public static final int OTHER_RULE_VERSION_EXPECTED_CODE = 37350;
253
254 /** Error message. */
255 public static final String OTHER_RULE_VERSION_EXPECTED_TEXT1
256 = "we expected this rule verson: ";
257
258 /** Error message. */
259 public static final String OTHER_RULE_VERSION_EXPECTED_TEXT2
260 = " but we got: ";
261
262
263 /** Error code. */
264 public static final int NEW_RULE_HAS_LOWER_VERSION_NUMBER_CODE = 37360;
265
266 /** Error message. */
267 public static final String NEW_RULE_HAS_LOWER_VERSION_NUMBER_TEXT
268 = "the new declared rule version must be higher than the old one: ";
269
270
271 /** Error code. */
272 public static final int OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_CODE = 37370;
273
274 /** Error message. */
275 public static final String OLD_OR_NEW_RULE_HAS_INVALID_VERSION_NUMBER_PATTERN_TEXT
276 = "the version numbers have not the allowed pattern (old or new rule version): ";
277
278
279 /** Error code. */
280 public static final int RULE_HAS_NO_NAME_OR_VERSION_CODE = 37380;
281
282 /** Error message. */
283 public static final String RULE_HAS_NO_NAME_OR_VERSION_TEXT
284 = "this rule has no name or version: ";
285
286
287 /** Error code. */
288 public static final int RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_CODE = 37390;
289
290 /** Error message. */
291 public static final String RULE_DECLARED_IN_DIFFERENT_IMPORT_MODULES_TEXT
292 = "this rule is defined in two different modules: ";
293
294
295 /** Error code. */
296 public static final int FUNCTION_NAME_IN_FORMULA_MUST_SAME_CODE = 37395;
297
298 /** Error message. */
299 public static final String FUNCTION_NAME_IN_FORMULA_MUST_SAME_TEXT
300 = "function name in formula must be same as in definition, expected: ";
301
302
303 }
|