Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
0   244   0   -
0   87   -   0
0     -  
1    
 
  BasicProofErrors       Line # 25 0 0 - -1.0
 
No Tests
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.bo.logic.proof.checker;
17   
18    import org.qedeq.kernel.se.common.ErrorCodes;
19   
20    /**
21    * Error codes and messages for proof checker.
22    *
23    * @author Michael Meyling
24    */
 
25    public interface BasicProofErrors extends ErrorCodes {
26   
27    /** Error code. */
28    public static final int PROOF_LINE_MUST_NOT_BE_NULL_CODE = 37100;
29   
30    /** Error message. */
31    public static final String PROOF_LINE_MUST_NOT_BE_NULL_TEXT
32    = "proof line must not be empty";
33   
34   
35    /** Error code. */
36    public static final int REASON_MUST_NOT_BE_NULL_CODE = 37110;
37   
38    /** Error message. */
39    public static final String REASON_MUST_NOT_BE_NULL_TEXT
40    = "reason must not be empty";
41   
42   
43    /** Error code. */
44    public static final int THIS_IS_NO_ALLOWED_BASIC_REASON_CODE = 37120;
45   
46    /** Error message. */
47    public static final String THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT
48    = "this is no allowed basic rule: ";
49   
50   
51    /** Error code. */
52    public static final int THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE = 37130;
53   
54    /** Error message. */
55    public static final String THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT
56    = "this is not a reference to a proved formula: ";
57   
58   
59    /** Error code. */
60    public static final int EXPECTED_FORMULA_DIFFERS_CODE = 37140;
61   
62    /** Error message. */
63    public static final String EXPECTED_FORMULA_DIFFERS_TEXT
64    = "this is not the expected part formula, please check with label: ";
65   
66   
67    /** Error code. */
68    public static final int EXPECTED_FORMULA_DIFFERS_2_CODE = 37142;
69   
70    /** Error message. */
71    public static final String EXPECTED_FORMULA_DIFFERS_2_TEXT
72    = "this is not the expected part formula";
73   
74   
75    /** Error code. */
76    public static final int LOCAL_LABEL_ALREADY_EXISTS_CODE = 37150;
77   
78    /** Error message. */
79    public static final String LOCAL_LABEL_ALREADY_EXISTS_TEXT
80    = "this proof line label exists already in this proof: ";
81   
82   
83    /** Error code. */
84    public static final int SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE = 37160;
85   
86    /** Error message. */
87    public static final String SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT
88    = "this proof line label dosn't (yet) exist in this proof: ";
89   
90   
91    /** Error code. */
92    public static final int IMPLICATION_EXPECTED_CODE = 37170;
93   
94    /** Error message. */
95    public static final String IMPLICATION_EXPECTED_TEXT
96    = "this proof line label must point to an implication (with two arguments): ";
97   
98   
99    /** Error code. */
100    public static final int MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE = 37180;
101   
102    /** Error message. */
103    public static final String MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT
104    = "this proof line label must be the hypothesis for the first reference: ";
105   
106   
107    /** Error code. */
108    public static final int CURRENT_MUST_BE_CONCLUSION_CODE = 37190;
109   
110    /** Error message. */
111    public static final String CURRENT_MUST_BE_CONCLUSION_TEXT
112    = "this proof line must be the conclusion of the first reference: ";
113   
114   
115    /** Error code. */
116    public static final int LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE = 37200;
117   
118    /** Error message. */
119    public static final String LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT
120    = "the last proof line must be identical to the proposition formula";
121   
122   
123    /** Error code. */
124    public static final int SUBSTITUTION_FORMULA_IS_MISSING_CODE = 37210;
125   
126    /** Error message. */
127    public static final String SUBSTITUTION_FORMULA_IS_MISSING_TEXT
128    = "the substitution formula is missing";
129   
130   
131    /** Error code. */
132    public static final int REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE = 37220;
133   
134    /** Error message. */
135    public static final String REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT
136    = "this is not a reference to a proved formula: ";
137   
138   
139    /** Error code. */
140    public static final int SUBSTITUTION_TERM_IS_MISSING_CODE = 37230;
141   
142    /** Error message. */
143    public static final String SUBSTITUTION_TERM_IS_MISSING_TEXT
144    = "the substitution term is missing";
145   
146   
147    /** Error code. */
148    public static final int ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE = 37240;
149   
150    /** Error message. */
151    public static final String ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT
152    = "only free subject variables as parameters allowed";
153   
154   
155    /** Error code. */
156    public static final int FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE = 37250;
157   
158    /** Error message. */
159    public static final String FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT
160    = "free subject variables should not get bound during substitution";
161   
162   
163    /** Error code. */
164    public static final int SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE = 37260;
165   
166    /** Error message. */
167    public static final String SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT
168    = "the substitution location contains subject variables that are bound within the "
169    + "replacement formula";
170   
171   
172    /** Error code. */
173    public static final int SUBJECT_VARIABLE_IS_MISSING_CODE = 37270;
174   
175    /** Error message. */
176    public static final String SUBJECT_VARIABLE_IS_MISSING_TEXT
177    = "subject variable is missing";
178   
179   
180    /** Error code. */
181    public static final int MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_CODE = 37370;
182   
183    /** Error message. */
184    public static final String MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_TEXT
185    = "missing proof lines for conditional proof";
186   
187   
188    /** Error code. */
189    public static final int SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE = 37380;
190   
191    /** Error message. */
192    public static final String SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT
193    = "the operator that should be substituted was found within a precondition";
194   
195   
196    /** Error code. */
197    public static final int NO_FORMAL_PROOFS_SUPORTED_CODE = 37400;
198   
199    /** Error message. */
200    public static final String NO_FORMAL_PROOFS_SUPORTED_TEXT
201    = "the module has rule version that forbids formal proofs: ";
202   
203   
204    /** Error code. */
205    public static final int CONDITIONS_AND_FORMULA_DONT_AGREE_CODE = 37410;
206   
207    /** Error message. */
208    public static final String CONDITIONS_AND_FORMULA_DONT_AGREE_TEXT
209    = "the conditions for this proof line doesn't agree with the formula ";
210   
211   
212    /** Error code. */
213    public static final int PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE = 37420;
214   
215    /** Error message. */
216    public static final String PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT
217    = "proof method was not defined yet: ";
218   
219   
220    /** Error code. */
221    public static final int PROOF_METHOD_IS_NOT_SUPPORTED_CODE = 37430;
222   
223    /** Error message. */
224    public static final String PROOF_METHOD_IS_NOT_SUPPORTED_TEXT
225    = "proof method is not supported for this proof checker: ";
226   
227    /** Error message. Part two. */
228    public static final String PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2
229    = ", we only support: ";
230   
231   
232    /** Error code. */
233    public static final int HIGHER_PROOF_RULE_VERSION_NEEDED_CODE = 37440;
234   
235    /** Error message. */
236    public static final String HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT
237    = "you need a higher rule version for applying this rule here, needed: ";
238   
239    /** Error message. Part 2. */
240    public static final String HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2
241    = ", current: ";
242   
243   
244    }