1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
package org.qedeq.kernel.bo.logic.proof.checker; |
17 |
|
|
18 |
|
import java.util.HashMap; |
19 |
|
import java.util.Map; |
20 |
|
|
21 |
|
import org.qedeq.base.io.Version; |
22 |
|
import org.qedeq.base.io.VersionSet; |
23 |
|
import org.qedeq.base.utility.Enumerator; |
24 |
|
import org.qedeq.base.utility.EqualsUtility; |
25 |
|
import org.qedeq.base.utility.StringUtility; |
26 |
|
import org.qedeq.kernel.bo.logic.common.FormulaChecker; |
27 |
|
import org.qedeq.kernel.bo.logic.common.FormulaUtility; |
28 |
|
import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList; |
29 |
|
import org.qedeq.kernel.bo.logic.common.Operators; |
30 |
|
import org.qedeq.kernel.bo.logic.common.ReferenceResolver; |
31 |
|
import org.qedeq.kernel.bo.logic.proof.common.ProofChecker; |
32 |
|
import org.qedeq.kernel.bo.logic.proof.common.RuleChecker; |
33 |
|
import org.qedeq.kernel.bo.logic.wf.FormulaCheckerImpl; |
34 |
|
import org.qedeq.kernel.se.base.list.Element; |
35 |
|
import org.qedeq.kernel.se.base.list.ElementList; |
36 |
|
import org.qedeq.kernel.se.base.module.Add; |
37 |
|
import org.qedeq.kernel.se.base.module.ConditionalProof; |
38 |
|
import org.qedeq.kernel.se.base.module.Existential; |
39 |
|
import org.qedeq.kernel.se.base.module.FormalProofLine; |
40 |
|
import org.qedeq.kernel.se.base.module.FormalProofLineList; |
41 |
|
import org.qedeq.kernel.se.base.module.ModusPonens; |
42 |
|
import org.qedeq.kernel.se.base.module.Reason; |
43 |
|
import org.qedeq.kernel.se.base.module.Rename; |
44 |
|
import org.qedeq.kernel.se.base.module.Rule; |
45 |
|
import org.qedeq.kernel.se.base.module.SubstFree; |
46 |
|
import org.qedeq.kernel.se.base.module.SubstFunc; |
47 |
|
import org.qedeq.kernel.se.base.module.SubstPred; |
48 |
|
import org.qedeq.kernel.se.base.module.Universal; |
49 |
|
import org.qedeq.kernel.se.common.ModuleAddress; |
50 |
|
import org.qedeq.kernel.se.common.ModuleContext; |
51 |
|
import org.qedeq.kernel.se.common.RuleKey; |
52 |
|
import org.qedeq.kernel.se.dto.list.DefaultElementList; |
53 |
|
import org.qedeq.kernel.se.dto.list.ElementSet; |
54 |
|
|
55 |
|
|
56 |
|
|
57 |
|
|
58 |
|
|
59 |
|
@author |
60 |
|
|
|
|
| 44.6% |
Uncovered Elements: 444 (801) |
Complexity: 166 |
Complexity Density: 0.3 |
|
61 |
|
public class ProofChecker2Impl implements ProofChecker, ReferenceResolver { |
62 |
|
|
63 |
|
|
64 |
|
private FormalProofLineList proof; |
65 |
|
|
66 |
|
|
67 |
|
private ModuleContext moduleContext; |
68 |
|
|
69 |
|
|
70 |
|
private ModuleContext currentContext; |
71 |
|
|
72 |
|
|
73 |
|
private ReferenceResolver resolver; |
74 |
|
|
75 |
|
|
76 |
|
private LogicalCheckExceptionList exceptions; |
77 |
|
|
78 |
|
|
79 |
|
private boolean[] lineProved; |
80 |
|
|
81 |
|
|
82 |
|
private Map label2line; |
83 |
|
|
84 |
|
|
85 |
|
private final VersionSet supported; |
86 |
|
|
87 |
|
|
88 |
|
private ElementList conditions; |
89 |
|
|
90 |
|
|
91 |
|
private RuleChecker checker; |
92 |
|
|
93 |
|
|
94 |
|
|
95 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (3) |
Complexity: 1 |
Complexity Density: 0.33 |
|
96 |
87
|
public ProofChecker2Impl() {... |
97 |
87
|
supported = new VersionSet(); |
98 |
87
|
supported.add("0.01.00"); |
99 |
87
|
supported.add("0.02.00"); |
100 |
|
} |
101 |
|
|
|
|
| 0% |
Uncovered Elements: 8 (8) |
Complexity: 3 |
Complexity Density: 0.5 |
|
102 |
0
|
public LogicalCheckExceptionList checkRule(final Rule rule,... |
103 |
|
final ModuleContext context, final RuleChecker checker, |
104 |
|
final ReferenceResolver resolver) { |
105 |
0
|
exceptions = new LogicalCheckExceptionList(); |
106 |
0
|
final RuleKey ruleKey = new RuleKey(rule.getName(), rule.getVersion()); |
107 |
0
|
if (rule.getVersion() == null || !supported.contains(rule.getVersion())) { |
108 |
0
|
final ProofCheckException ex = new ProofCheckException( |
109 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
110 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + ruleKey |
111 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
112 |
|
context); |
113 |
0
|
exceptions.add(ex); |
114 |
|
} |
115 |
0
|
return exceptions; |
116 |
|
} |
117 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (2) |
Complexity: 1 |
Complexity Density: 0.5 |
|
118 |
37
|
public LogicalCheckExceptionList checkProof(final Element formula,... |
119 |
|
final FormalProofLineList proof, |
120 |
|
final RuleChecker checker, |
121 |
|
final ModuleContext moduleContext, |
122 |
|
final ReferenceResolver resolver) { |
123 |
37
|
final DefaultElementList con = new DefaultElementList( |
124 |
|
Operators.CONJUNCTION_OPERATOR); |
125 |
|
|
126 |
37
|
return checkProof(con, formula, proof, checker, moduleContext, resolver); |
127 |
|
} |
128 |
|
|
|
|
| 80.6% |
Uncovered Elements: 21 (108) |
Complexity: 23 |
Complexity Density: 0.33 |
|
129 |
87
|
private LogicalCheckExceptionList checkProof(final ElementList conditions, final Element formula,... |
130 |
|
final FormalProofLineList proof, |
131 |
|
final RuleChecker checker, |
132 |
|
final ModuleContext moduleContext, |
133 |
|
final ReferenceResolver resolver) { |
134 |
87
|
this.conditions = conditions; |
135 |
87
|
this.proof = proof; |
136 |
87
|
this.checker = checker; |
137 |
87
|
this.resolver = resolver; |
138 |
87
|
this.moduleContext = moduleContext; |
139 |
|
|
140 |
87
|
currentContext = new ModuleContext(moduleContext); |
141 |
87
|
exceptions = new LogicalCheckExceptionList(); |
142 |
87
|
final String context = moduleContext.getLocationWithinModule(); |
143 |
87
|
lineProved = new boolean[proof.size()]; |
144 |
87
|
label2line = new HashMap(); |
145 |
532
|
for (int i = 0; i < proof.size(); i++) { |
146 |
445
|
boolean ok = true; |
147 |
445
|
setLocationWithinModule(context + ".get(" + i + ")"); |
148 |
445
|
final FormalProofLine line = proof.get(i); |
149 |
445
|
if (line == null || line.getFormula() == null |
150 |
|
|| line.getFormula().getElement() == null) { |
151 |
0
|
ok = false; |
152 |
0
|
handleProofCheckException( |
153 |
|
BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE, |
154 |
|
BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT, |
155 |
|
getCurrentContext()); |
156 |
0
|
continue; |
157 |
|
} |
158 |
445
|
setLocationWithinModule(context + ".get(" + i + ").getReason()"); |
159 |
445
|
final Reason reason = line.getReason(); |
160 |
445
|
if (reason == null) { |
161 |
0
|
ok = false; |
162 |
0
|
handleProofCheckException( |
163 |
|
BasicProofErrors.REASON_MUST_NOT_BE_NULL_CODE, |
164 |
|
BasicProofErrors.REASON_MUST_NOT_BE_NULL_TEXT, |
165 |
|
getCurrentContext()); |
166 |
0
|
continue; |
167 |
|
} |
168 |
445
|
if (line.getLabel() != null && line.getLabel().length() > 0) { |
169 |
445
|
setLocationWithinModule(context + ".get(" + i + ").getLabel()"); |
170 |
445
|
addLocalLineLabel(i, line.getLabel()); |
171 |
|
} |
172 |
|
|
173 |
|
|
174 |
445
|
if (hasConditions()) { |
175 |
126
|
setLocationWithinModule(context + ".get(" + i + ").getFormula.getElement()"); |
176 |
126
|
ElementList full = new DefaultElementList(Operators.IMPLICATION_OPERATOR); |
177 |
126
|
if (conditions.size() > 1) { |
178 |
51
|
full.add(conditions); |
179 |
|
} else { |
180 |
75
|
full.add(conditions.getElement(0)); |
181 |
|
} |
182 |
126
|
full.add(line.getFormula().getElement()); |
183 |
126
|
FormulaChecker checkWf = new FormulaCheckerImpl(); |
184 |
126
|
final LogicalCheckExceptionList list = checkWf.checkFormula(full, getCurrentContext()); |
185 |
126
|
if (list.size() > 0) { |
186 |
0
|
ok = false; |
187 |
0
|
handleProofCheckException( |
188 |
|
BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_CODE, |
189 |
|
BasicProofErrors.CONDITIONS_AND_FORMULA_DONT_AGREE_TEXT |
190 |
|
+ list.get(0).getMessage(), |
191 |
|
getCurrentContext()); |
192 |
0
|
continue; |
193 |
|
} |
194 |
|
} |
195 |
|
|
196 |
|
|
197 |
|
|
198 |
|
|
199 |
445
|
String getReason = ".get" + StringUtility.getClassName(reason.getClass()); |
200 |
445
|
if (getReason.endsWith("Vo")) { |
201 |
445
|
getReason = getReason.substring(0, getReason.length() - 2) + "()"; |
202 |
445
|
setLocationWithinModule(context + ".get(" + i + ").getReason()" |
203 |
|
+ getReason); |
204 |
|
|
205 |
|
} |
206 |
445
|
if (reason instanceof Add) { |
207 |
88
|
ok = check((Add) reason, i, line.getFormula().getElement()); |
208 |
357
|
} else if (reason instanceof Rename) { |
209 |
5
|
ok = check((Rename) reason, i, line.getFormula().getElement()); |
210 |
352
|
} else if (reason instanceof ModusPonens) { |
211 |
134
|
ok = check((ModusPonens) reason, i, line.getFormula().getElement()); |
212 |
218
|
} else if (reason instanceof SubstFree) { |
213 |
4
|
ok = check((SubstFree) reason, i, line.getFormula().getElement()); |
214 |
214
|
} else if (reason instanceof SubstPred) { |
215 |
160
|
ok = check((SubstPred) reason, i, line.getFormula().getElement()); |
216 |
54
|
} else if (reason instanceof SubstFunc) { |
217 |
0
|
ok = check((SubstFunc) reason, i, line.getFormula().getElement()); |
218 |
54
|
} else if (reason instanceof Universal) { |
219 |
4
|
ok = check((Universal) reason, i, line.getFormula().getElement()); |
220 |
50
|
} else if (reason instanceof Existential) { |
221 |
0
|
ok = check((Existential) reason, i, line.getFormula().getElement()); |
222 |
50
|
} else if (reason instanceof ConditionalProof) { |
223 |
50
|
setLocationWithinModule(context + ".get(" + i + ")"); |
224 |
50
|
ok = check((ConditionalProof) reason, i, line.getFormula().getElement()); |
225 |
|
} else { |
226 |
0
|
ok = false; |
227 |
0
|
handleProofCheckException( |
228 |
|
BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_CODE, |
229 |
|
BasicProofErrors.THIS_IS_NO_ALLOWED_BASIC_REASON_TEXT |
230 |
|
+ reason.getName(), |
231 |
|
getCurrentContext()); |
232 |
|
} |
233 |
445
|
lineProved[i] = ok; |
234 |
|
|
235 |
445
|
if (i == proof.size() - 1) { |
236 |
87
|
if (!formula.equals(line.getFormula().getElement())) { |
237 |
1
|
handleProofCheckException( |
238 |
|
BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_CODE, |
239 |
|
BasicProofErrors.LAST_PROOF_LINE_MUST_BE_IDENTICAL_TO_PROPOSITION_TEXT, |
240 |
|
getModuleContextOfProofLineFormula(i)); |
241 |
|
} |
242 |
|
} |
243 |
|
} |
244 |
87
|
return exceptions; |
245 |
|
} |
246 |
|
|
|
|
| 57.1% |
Uncovered Elements: 6 (14) |
Complexity: 5 |
Complexity Density: 0.62 |
|
247 |
445
|
private void addLocalLineLabel(final int i, final String label) {... |
248 |
445
|
if (label != null && label.length() > 0) { |
249 |
445
|
final Integer n = (Integer) label2line.get(label); |
250 |
445
|
if (n != null) { |
251 |
0
|
final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(), |
252 |
|
moduleContext.getLocationWithinModule() + ".get(" |
253 |
|
+ label2line.get(label) |
254 |
|
+ ").getLabel()"); |
255 |
0
|
handleProofCheckException( |
256 |
|
BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE, |
257 |
|
BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT |
258 |
|
+ label, |
259 |
|
getCurrentContext(), |
260 |
|
lc); |
261 |
|
} else { |
262 |
445
|
if (isLocalProofLineReference(label)) { |
263 |
0
|
handleProofCheckException( |
264 |
|
BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_CODE, |
265 |
|
BasicProofErrors.LOCAL_LABEL_ALREADY_EXISTS_TEXT |
266 |
|
+ label, |
267 |
|
getCurrentContext(), |
268 |
|
resolver.getReferenceContext(label)); |
269 |
|
|
270 |
|
|
271 |
|
} |
272 |
|
} |
273 |
|
|
274 |
445
|
label2line.put(label, new Integer(i)); |
275 |
|
} |
276 |
|
} |
277 |
|
|
|
|
| 40.9% |
Uncovered Elements: 26 (44) |
Complexity: 8 |
Complexity Density: 0.25 |
|
278 |
88
|
private boolean check(final Add add, final int i, final Element element) {... |
279 |
88
|
final String context = currentContext.getLocationWithinModule(); |
280 |
88
|
boolean ok = true; |
281 |
88
|
if (add.getReference() == null) { |
282 |
0
|
ok = false; |
283 |
0
|
setLocationWithinModule(context + ".getReference()"); |
284 |
0
|
handleProofCheckException( |
285 |
|
BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_CODE, |
286 |
|
BasicProofErrors.REFERENCE_TO_PROVED_FORMULA_IS_MISSING_TEXT, |
287 |
|
getCurrentContext()); |
288 |
0
|
return ok; |
289 |
|
} |
290 |
88
|
if (!resolver.isProvedFormula(add.getReference())) { |
291 |
0
|
ok = false; |
292 |
0
|
setLocationWithinModule(context + ".getReference()"); |
293 |
0
|
handleProofCheckException( |
294 |
|
BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_CODE, |
295 |
|
BasicProofErrors.THIS_IS_NO_REFERENCE_TO_A_PROVED_FORMULA_TEXT |
296 |
|
+ add.getReference(), |
297 |
|
getCurrentContext()); |
298 |
0
|
return ok; |
299 |
|
} |
300 |
88
|
final Element expected = resolver.getNormalizedReferenceFormula(add.getReference()); |
301 |
88
|
final Element current = resolver.getNormalizedFormula(element); |
302 |
88
|
if (!EqualsUtility.equals(expected, current)) { |
303 |
0
|
ok = false; |
304 |
0
|
handleProofCheckException( |
305 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE, |
306 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT |
307 |
|
+ add.getReference(), |
308 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
309 |
0
|
return ok; |
310 |
|
} |
311 |
88
|
final RuleKey defined = checker.getRule(add.getName()); |
312 |
88
|
if (defined == null) { |
313 |
0
|
ok = false; |
314 |
0
|
handleProofCheckException( |
315 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE, |
316 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
317 |
|
+ add.getName(), |
318 |
|
getCurrentContext()); |
319 |
0
|
return ok; |
320 |
88
|
} else if (!supported.contains(defined.getVersion())) { |
321 |
0
|
ok = false; |
322 |
0
|
handleProofCheckException( |
323 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
324 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion() |
325 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
326 |
|
getCurrentContext()); |
327 |
0
|
return ok; |
328 |
88
|
} else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) { |
329 |
0
|
ok = false; |
330 |
0
|
handleProofCheckException( |
331 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE, |
332 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00" |
333 |
|
+ BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(), |
334 |
|
getCurrentContext()); |
335 |
0
|
return ok; |
336 |
|
} |
337 |
88
|
return ok; |
338 |
|
} |
339 |
|
|
|
|
| 48.6% |
Uncovered Elements: 19 (37) |
Complexity: 7 |
Complexity Density: 0.26 |
|
340 |
5
|
private boolean check(final Rename rename, final int i, final Element element) {... |
341 |
5
|
final String context = currentContext.getLocationWithinModule(); |
342 |
5
|
boolean ok = true; |
343 |
5
|
final Element f = getNormalizedLocalProofLineReference(rename.getReference()); |
344 |
5
|
if (f == null) { |
345 |
0
|
ok = false; |
346 |
0
|
setLocationWithinModule(context + ".getReference()"); |
347 |
0
|
handleProofCheckException( |
348 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE, |
349 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT |
350 |
|
+ rename.getReference(), |
351 |
|
getCurrentContext()); |
352 |
|
} else { |
353 |
5
|
final Element expected = FormulaUtility.replaceSubjectVariableQuantifier( |
354 |
|
rename.getOriginalSubjectVariable(), |
355 |
|
rename.getReplacementSubjectVariable(), f, rename.getOccurrence(), |
356 |
|
new Enumerator()); |
357 |
5
|
final Element current = resolver.getNormalizedFormula(element); |
358 |
5
|
if (!EqualsUtility.equals(expected, current)) { |
359 |
0
|
ok = false; |
360 |
0
|
handleProofCheckException( |
361 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE, |
362 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT |
363 |
|
+ rename.getReference(), |
364 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
365 |
|
} else { |
366 |
5
|
ok = true; |
367 |
|
} |
368 |
|
} |
369 |
5
|
final RuleKey defined = checker.getRule(rename.getName()); |
370 |
5
|
if (defined == null) { |
371 |
0
|
ok = false; |
372 |
0
|
handleProofCheckException( |
373 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE, |
374 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
375 |
|
+ rename.getName(), |
376 |
|
getCurrentContext()); |
377 |
0
|
return ok; |
378 |
5
|
} else if (!supported.contains(defined.getVersion())) { |
379 |
0
|
ok = false; |
380 |
0
|
handleProofCheckException( |
381 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
382 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion() |
383 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
384 |
|
getCurrentContext()); |
385 |
0
|
return ok; |
386 |
5
|
} else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) { |
387 |
0
|
ok = false; |
388 |
0
|
handleProofCheckException( |
389 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE, |
390 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00" |
391 |
|
+ BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(), |
392 |
|
getCurrentContext()); |
393 |
0
|
return ok; |
394 |
|
} |
395 |
5
|
return ok; |
396 |
|
} |
397 |
|
|
|
|
| 43.2% |
Uncovered Elements: 25 (44) |
Complexity: 8 |
Complexity Density: 0.25 |
|
398 |
4
|
private boolean check(final SubstFree substFree, final int i, final Element element) {... |
399 |
4
|
final String context = currentContext.getLocationWithinModule(); |
400 |
4
|
boolean ok = true; |
401 |
4
|
final Element f = getNormalizedLocalProofLineReference(substFree.getReference()); |
402 |
4
|
if (f == null) { |
403 |
0
|
ok = false; |
404 |
0
|
setLocationWithinModule(context + ".getReference()"); |
405 |
0
|
handleProofCheckException( |
406 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE, |
407 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT |
408 |
|
+ substFree.getReference(), |
409 |
|
getCurrentContext()); |
410 |
|
} else { |
411 |
4
|
final Element current = resolver.getNormalizedFormula(element); |
412 |
4
|
final Element expected = f.replace(substFree.getSubjectVariable(), |
413 |
|
resolver.getNormalizedFormula(substFree.getSubstituteTerm())); |
414 |
4
|
if (!EqualsUtility.equals(current, expected)) { |
415 |
0
|
ok = false; |
416 |
0
|
handleProofCheckException( |
417 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE, |
418 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT |
419 |
|
+ substFree.getReference(), |
420 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
421 |
0
|
return ok; |
422 |
|
} |
423 |
|
} |
424 |
|
|
425 |
4
|
if (FormulaUtility.containsOperatorVariable(conditions, substFree.getSubjectVariable())) { |
426 |
0
|
ok = false; |
427 |
0
|
setLocationWithinModule(context + ".getSubstituteFormula()"); |
428 |
0
|
handleProofCheckException( |
429 |
|
BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE, |
430 |
|
BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT, |
431 |
|
getCurrentContext()); |
432 |
0
|
return ok; |
433 |
|
} |
434 |
4
|
final RuleKey defined = checker.getRule(substFree.getName()); |
435 |
4
|
if (defined == null) { |
436 |
0
|
ok = false; |
437 |
0
|
handleProofCheckException( |
438 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE, |
439 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
440 |
|
+ substFree.getName(), |
441 |
|
getCurrentContext()); |
442 |
0
|
return ok; |
443 |
4
|
} else if (!supported.contains(defined.getVersion())) { |
444 |
0
|
ok = false; |
445 |
0
|
handleProofCheckException( |
446 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
447 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion() |
448 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
449 |
|
getCurrentContext()); |
450 |
0
|
return ok; |
451 |
4
|
} else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) { |
452 |
0
|
ok = false; |
453 |
0
|
handleProofCheckException( |
454 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE, |
455 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00" |
456 |
|
+ BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(), |
457 |
|
getCurrentContext()); |
458 |
0
|
return ok; |
459 |
|
} |
460 |
4
|
return ok; |
461 |
|
} |
462 |
|
|
|
|
| 43.2% |
Uncovered Elements: 50 (88) |
Complexity: 14 |
Complexity Density: 0.22 |
|
463 |
160
|
private boolean check(final SubstPred substPred, final int i, final Element element) {... |
464 |
160
|
final String context = currentContext.getLocationWithinModule(); |
465 |
160
|
boolean ok = true; |
466 |
160
|
final Element alpha = getNormalizedLocalProofLineReference(substPred.getReference()); |
467 |
160
|
if (alpha == null) { |
468 |
0
|
ok = false; |
469 |
0
|
setLocationWithinModule(context + ".getReference()"); |
470 |
0
|
handleProofCheckException( |
471 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE, |
472 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT |
473 |
|
+ substPred.getReference(), |
474 |
|
getCurrentContext()); |
475 |
0
|
return ok; |
476 |
|
} |
477 |
160
|
final Element current = resolver.getNormalizedFormula(element); |
478 |
160
|
if (substPred.getSubstituteFormula() == null) { |
479 |
0
|
ok = false; |
480 |
0
|
handleProofCheckException( |
481 |
|
BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE, |
482 |
|
BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT, |
483 |
|
getCurrentContext()); |
484 |
0
|
return ok; |
485 |
|
} |
486 |
160
|
final Element p = resolver.getNormalizedFormula(substPred.getPredicateVariable()); |
487 |
160
|
final Element beta = resolver.getNormalizedFormula(substPred.getSubstituteFormula()); |
488 |
160
|
final Element expected = FormulaUtility.replaceOperatorVariable(alpha, p, beta); |
489 |
160
|
if (!EqualsUtility.equals(current, expected)) { |
490 |
0
|
ok = false; |
491 |
0
|
handleProofCheckException( |
492 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE, |
493 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT |
494 |
|
+ substPred.getReference(), |
495 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
496 |
0
|
return ok; |
497 |
|
} |
498 |
|
|
499 |
|
|
500 |
160
|
final ElementSet predFree = FormulaUtility.getFreeSubjectVariables(p); |
501 |
160
|
if (predFree.size() != p.getList().size() - 1) { |
502 |
0
|
ok = false; |
503 |
0
|
setLocationWithinModule(context + ".getPredicateVariable()"); |
504 |
0
|
handleProofCheckException( |
505 |
|
BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE, |
506 |
|
BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT, |
507 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
508 |
0
|
return ok; |
509 |
|
} |
510 |
164
|
for (int j = 1; j < p.getList().size(); j++) { |
511 |
4
|
if (!FormulaUtility.isSubjectVariable(p.getList().getElement(j))) { |
512 |
0
|
ok = false; |
513 |
0
|
setLocationWithinModule(context + ".getPredicateVariable()"); |
514 |
0
|
handleProofCheckException( |
515 |
|
BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE, |
516 |
|
BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT, |
517 |
|
getCurrentContext()); |
518 |
0
|
return ok; |
519 |
|
} |
520 |
|
} |
521 |
|
|
522 |
|
|
523 |
160
|
final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha); |
524 |
160
|
final ElementSet betaFree = FormulaUtility.getFreeSubjectVariables(beta); |
525 |
160
|
if (!fBound.intersection(betaFree.minus(predFree)).isEmpty()) { |
526 |
0
|
ok = false; |
527 |
0
|
setLocationWithinModule(context + ".getSubstituteFormula()"); |
528 |
0
|
handleProofCheckException( |
529 |
|
BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE, |
530 |
|
BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT, |
531 |
|
getCurrentContext()); |
532 |
0
|
return ok; |
533 |
|
} |
534 |
|
|
535 |
|
|
536 |
160
|
final ElementSet betaBound = FormulaUtility.getBoundSubjectVariables(beta); |
537 |
160
|
if (!FormulaUtility.testOperatorVariable(alpha, p, betaBound)) { |
538 |
0
|
ok = false; |
539 |
0
|
setLocationWithinModule(context + ".getSubstituteFormula()"); |
540 |
0
|
handleProofCheckException( |
541 |
|
BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE, |
542 |
|
BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT, |
543 |
|
getCurrentContext()); |
544 |
0
|
return ok; |
545 |
|
} |
546 |
|
|
547 |
160
|
if (FormulaUtility.containsOperatorVariable(conditions, p)) { |
548 |
0
|
ok = false; |
549 |
0
|
setLocationWithinModule(context + ".getPredicateVariable()"); |
550 |
0
|
handleProofCheckException( |
551 |
|
BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE, |
552 |
|
BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT, |
553 |
|
getCurrentContext()); |
554 |
0
|
return ok; |
555 |
|
} |
556 |
|
|
557 |
|
|
558 |
|
|
559 |
160
|
final RuleKey defined = checker.getRule(substPred.getName()); |
560 |
160
|
if (defined == null) { |
561 |
0
|
ok = false; |
562 |
0
|
handleProofCheckException( |
563 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE, |
564 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
565 |
|
+ substPred.getName(), |
566 |
|
getCurrentContext()); |
567 |
0
|
return ok; |
568 |
160
|
} else if (!supported.contains(defined.getVersion())) { |
569 |
0
|
ok = false; |
570 |
0
|
handleProofCheckException( |
571 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
572 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion() |
573 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
574 |
|
getCurrentContext()); |
575 |
0
|
return ok; |
576 |
160
|
} else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) { |
577 |
0
|
ok = false; |
578 |
0
|
handleProofCheckException( |
579 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE, |
580 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00" |
581 |
|
+ BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(), |
582 |
|
getCurrentContext()); |
583 |
0
|
return ok; |
584 |
|
} |
585 |
160
|
return ok; |
586 |
|
} |
587 |
|
|
|
|
| 0% |
Uncovered Elements: 88 (88) |
Complexity: 14 |
Complexity Density: 0.22 |
|
588 |
0
|
private boolean check(final SubstFunc substFunc, final int i, final Element element) {... |
589 |
0
|
final String context = currentContext.getLocationWithinModule(); |
590 |
0
|
boolean ok = true; |
591 |
0
|
final Element alpha = getNormalizedLocalProofLineReference(substFunc.getReference()); |
592 |
0
|
if (alpha == null) { |
593 |
0
|
ok = false; |
594 |
0
|
setLocationWithinModule(context + ".getReference()"); |
595 |
0
|
handleProofCheckException( |
596 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE, |
597 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT |
598 |
|
+ substFunc.getReference(), |
599 |
|
getCurrentContext()); |
600 |
0
|
return ok; |
601 |
|
} |
602 |
0
|
final Element current = resolver.getNormalizedFormula(element); |
603 |
0
|
if (substFunc.getSubstituteTerm() == null) { |
604 |
0
|
ok = false; |
605 |
0
|
handleProofCheckException( |
606 |
|
BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_CODE, |
607 |
|
BasicProofErrors.SUBSTITUTION_FORMULA_IS_MISSING_TEXT, |
608 |
|
getCurrentContext()); |
609 |
0
|
return ok; |
610 |
|
} |
611 |
0
|
final Element sigma = resolver.getNormalizedFormula(substFunc.getFunctionVariable()); |
612 |
0
|
final Element tau = resolver.getNormalizedFormula(substFunc.getSubstituteTerm()); |
613 |
0
|
final Element expected = FormulaUtility.replaceOperatorVariable(alpha, sigma, tau); |
614 |
0
|
if (!EqualsUtility.equals(current, expected)) { |
615 |
0
|
ok = false; |
616 |
0
|
handleProofCheckException( |
617 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE, |
618 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT |
619 |
|
+ substFunc.getReference(), |
620 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
621 |
0
|
return ok; |
622 |
|
} |
623 |
|
|
624 |
|
|
625 |
0
|
final ElementSet funcFree = FormulaUtility.getFreeSubjectVariables(sigma); |
626 |
0
|
if (funcFree.size() != sigma.getList().size() - 1) { |
627 |
0
|
ok = false; |
628 |
0
|
setLocationWithinModule(context + ".getPredicateVariable()"); |
629 |
0
|
handleProofCheckException( |
630 |
|
BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE, |
631 |
|
BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT, |
632 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
633 |
0
|
return ok; |
634 |
|
} |
635 |
0
|
for (int j = 1; j < sigma.getList().size(); j++) { |
636 |
0
|
if (!FormulaUtility.isSubjectVariable(sigma.getList().getElement(j))) { |
637 |
0
|
ok = false; |
638 |
0
|
setLocationWithinModule(context + ".getPredicateVariable()"); |
639 |
0
|
handleProofCheckException( |
640 |
|
BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_CODE, |
641 |
|
BasicProofErrors.ONLY_FREE_SUBJECT_VARIABLES_ALLOWED_TEXT, |
642 |
|
getCurrentContext()); |
643 |
0
|
return ok; |
644 |
|
} |
645 |
|
} |
646 |
|
|
647 |
|
|
648 |
0
|
final ElementSet fBound = FormulaUtility.getBoundSubjectVariables(alpha); |
649 |
0
|
final ElementSet sigmaFree = FormulaUtility.getFreeSubjectVariables(tau); |
650 |
0
|
if (!fBound.intersection(sigmaFree.minus(funcFree)).isEmpty()) { |
651 |
0
|
ok = false; |
652 |
0
|
setLocationWithinModule(context + ".getSubstituteFormula()"); |
653 |
0
|
handleProofCheckException( |
654 |
|
BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_CODE, |
655 |
|
BasicProofErrors.FREE_SUBJECT_VARIABLES_SHOULD_NOT_GET_BOUND_TEXT, |
656 |
|
getCurrentContext()); |
657 |
0
|
return ok; |
658 |
|
} |
659 |
|
|
660 |
|
|
661 |
0
|
final ElementSet sigmaBound = FormulaUtility.getBoundSubjectVariables(tau); |
662 |
0
|
if (!FormulaUtility.testOperatorVariable(alpha, sigma, sigmaBound)) { |
663 |
0
|
ok = false; |
664 |
0
|
setLocationWithinModule(context + ".getSubstituteFormula()"); |
665 |
0
|
handleProofCheckException( |
666 |
|
BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_CODE, |
667 |
|
BasicProofErrors.SUBSTITUTION_LOCATION_CONTAINS_BOUND_SUBJECT_VARIABLE_TEXT, |
668 |
|
getCurrentContext()); |
669 |
0
|
return ok; |
670 |
|
} |
671 |
|
|
672 |
0
|
if (FormulaUtility.containsOperatorVariable(conditions, sigma)) { |
673 |
0
|
ok = false; |
674 |
0
|
setLocationWithinModule(context + ".getPredicateVariable()"); |
675 |
0
|
handleProofCheckException( |
676 |
|
BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_CODE, |
677 |
|
BasicProofErrors.SUBSTITUTION_OPERATOR_FOUND_IN_PRECONDITION_TEXT, |
678 |
|
getCurrentContext()); |
679 |
0
|
return ok; |
680 |
|
} |
681 |
|
|
682 |
|
|
683 |
|
|
684 |
0
|
final RuleKey defined = checker.getRule(substFunc.getName()); |
685 |
0
|
if (defined == null) { |
686 |
0
|
ok = false; |
687 |
0
|
handleProofCheckException( |
688 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE, |
689 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
690 |
|
+ substFunc.getName(), |
691 |
|
getCurrentContext()); |
692 |
0
|
return ok; |
693 |
0
|
} else if (!supported.contains(defined.getVersion())) { |
694 |
0
|
ok = false; |
695 |
0
|
handleProofCheckException( |
696 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
697 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion() |
698 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
699 |
|
getCurrentContext()); |
700 |
0
|
return ok; |
701 |
0
|
} else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) { |
702 |
0
|
ok = false; |
703 |
0
|
handleProofCheckException( |
704 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE, |
705 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00" |
706 |
|
+ BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(), |
707 |
|
getCurrentContext()); |
708 |
0
|
return ok; |
709 |
|
} |
710 |
0
|
return ok; |
711 |
|
} |
712 |
|
|
|
|
| 44.1% |
Uncovered Elements: 33 (59) |
Complexity: 11 |
Complexity Density: 0.27 |
|
713 |
134
|
private boolean check(final ModusPonens mp, final int i, final Element element) {... |
714 |
134
|
final String context = currentContext.getLocationWithinModule(); |
715 |
134
|
boolean ok = true; |
716 |
134
|
final Element f1 = getNormalizedLocalProofLineReference(mp.getReference1()); |
717 |
134
|
if (f1 == null) { |
718 |
0
|
ok = false; |
719 |
0
|
setLocationWithinModule(context + ".getReference1()"); |
720 |
0
|
handleProofCheckException( |
721 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE, |
722 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT |
723 |
|
+ mp.getReference1(), |
724 |
|
getCurrentContext()); |
725 |
|
} |
726 |
134
|
final Element f2 = getNormalizedLocalProofLineReference(mp.getReference2()); |
727 |
134
|
if (f2 == null) { |
728 |
0
|
ok = false; |
729 |
0
|
setLocationWithinModule(context + ".getReference2()"); |
730 |
0
|
handleProofCheckException( |
731 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE, |
732 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT |
733 |
|
+ mp.getReference2(), |
734 |
|
getCurrentContext()); |
735 |
|
} |
736 |
134
|
if (ok) { |
737 |
134
|
final Element current = getNormalizedFormula(element); |
738 |
134
|
if (!FormulaUtility.isImplication(f1)) { |
739 |
0
|
ok = false; |
740 |
0
|
setLocationWithinModule(context + ".getReference1()"); |
741 |
0
|
handleProofCheckException( |
742 |
|
BasicProofErrors.IMPLICATION_EXPECTED_CODE, |
743 |
|
BasicProofErrors.IMPLICATION_EXPECTED_TEXT |
744 |
|
+ mp.getReference1(), |
745 |
|
getCurrentContext()); |
746 |
134
|
} else if (!f2.equals(f1.getList().getElement(0))) { |
747 |
0
|
ok = false; |
748 |
0
|
setLocationWithinModule(context + ".getReference2()"); |
749 |
0
|
handleProofCheckException( |
750 |
|
BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_CODE, |
751 |
|
BasicProofErrors.MUST_BE_HYPOTHESIS_OF_FIRST_REFERENCE_TEXT |
752 |
|
+ mp.getReference2(), |
753 |
|
getCurrentContext(), |
754 |
|
resolver.getReferenceContext(mp.getReference1())); |
755 |
134
|
} else if (!current.equals(f1.getList().getElement(1))) { |
756 |
0
|
ok = false; |
757 |
0
|
setLocationWithinModule(context + ".getReference1()"); |
758 |
0
|
handleProofCheckException( |
759 |
|
BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_CODE, |
760 |
|
BasicProofErrors.CURRENT_MUST_BE_CONCLUSION_TEXT |
761 |
|
+ mp.getReference1(), |
762 |
|
getCurrentContext(), |
763 |
|
resolver.getReferenceContext(mp.getReference1())); |
764 |
|
} else { |
765 |
134
|
ok = true; |
766 |
|
} |
767 |
|
} |
768 |
134
|
final RuleKey defined = checker.getRule(mp.getName()); |
769 |
134
|
if (defined == null) { |
770 |
0
|
ok = false; |
771 |
0
|
handleProofCheckException( |
772 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE, |
773 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
774 |
|
+ mp.getName(), |
775 |
|
getCurrentContext()); |
776 |
0
|
return ok; |
777 |
134
|
} else if (!supported.contains(defined.getVersion())) { |
778 |
0
|
ok = false; |
779 |
0
|
handleProofCheckException( |
780 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
781 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion() |
782 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
783 |
|
getCurrentContext()); |
784 |
0
|
return ok; |
785 |
134
|
} else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) { |
786 |
0
|
ok = false; |
787 |
0
|
handleProofCheckException( |
788 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE, |
789 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00" |
790 |
|
+ BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(), |
791 |
|
getCurrentContext()); |
792 |
0
|
return ok; |
793 |
|
} |
794 |
134
|
return ok; |
795 |
|
} |
796 |
|
|
|
|
| 46.4% |
Uncovered Elements: 30 (56) |
Complexity: 9 |
Complexity Density: 0.21 |
|
797 |
4
|
private boolean check(final Universal universal, final int i, final Element element) {... |
798 |
4
|
final String context = currentContext.getLocationWithinModule(); |
799 |
4
|
boolean ok = true; |
800 |
4
|
final Element reference = getNormalizedLocalProofLineReference(universal.getReference()); |
801 |
4
|
if (reference == null) { |
802 |
0
|
ok = false; |
803 |
0
|
setLocationWithinModule(context + ".getReference()"); |
804 |
0
|
handleProofCheckException( |
805 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE, |
806 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT |
807 |
|
+ universal.getReference(), |
808 |
|
getCurrentContext()); |
809 |
|
|
810 |
|
|
811 |
|
|
812 |
|
|
813 |
|
|
814 |
|
|
815 |
|
|
816 |
|
|
817 |
|
} else { |
818 |
4
|
final Element current = getNormalizedFormula(element); |
819 |
4
|
if (!FormulaUtility.isImplication(current)) { |
820 |
0
|
ok = false; |
821 |
0
|
setLocationWithinModule(context + ".getReference()"); |
822 |
0
|
handleProofCheckException( |
823 |
|
BasicProofErrors.IMPLICATION_EXPECTED_CODE, |
824 |
|
BasicProofErrors.IMPLICATION_EXPECTED_TEXT |
825 |
|
+ universal.getReference(), |
826 |
|
getCurrentContext()); |
827 |
0
|
return ok; |
828 |
|
} |
829 |
4
|
if (!FormulaUtility.isSubjectVariable(universal.getSubjectVariable())) { |
830 |
0
|
ok = false; |
831 |
0
|
setLocationWithinModule(context + ".getSubjectVariable()"); |
832 |
0
|
handleProofCheckException( |
833 |
|
BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE, |
834 |
|
BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT, |
835 |
|
getCurrentContext()); |
836 |
0
|
return ok; |
837 |
|
} |
838 |
4
|
final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR); |
839 |
4
|
expected.add(reference.getList().getElement(0)); |
840 |
4
|
final ElementList uni = new DefaultElementList(Operators.UNIVERSAL_QUANTIFIER_OPERATOR); |
841 |
4
|
uni.add(universal.getSubjectVariable()); |
842 |
4
|
uni.add(reference.getList().getElement(1)); |
843 |
4
|
expected.add(uni); |
844 |
|
|
845 |
|
|
846 |
|
|
847 |
|
|
848 |
4
|
if (!EqualsUtility.equals(current, expected)) { |
849 |
0
|
ok = false; |
850 |
0
|
handleProofCheckException( |
851 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE, |
852 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT |
853 |
|
+ universal.getReference(), |
854 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
855 |
0
|
return ok; |
856 |
|
} |
857 |
|
} |
858 |
4
|
final RuleKey defined = checker.getRule(universal.getName()); |
859 |
4
|
if (defined == null) { |
860 |
0
|
ok = false; |
861 |
0
|
handleProofCheckException( |
862 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE, |
863 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
864 |
|
+ universal.getName(), |
865 |
|
getCurrentContext()); |
866 |
0
|
return ok; |
867 |
4
|
} else if (!supported.contains(defined.getVersion())) { |
868 |
0
|
ok = false; |
869 |
0
|
handleProofCheckException( |
870 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
871 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion() |
872 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
873 |
|
getCurrentContext()); |
874 |
0
|
return ok; |
875 |
4
|
} else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) { |
876 |
0
|
ok = false; |
877 |
0
|
handleProofCheckException( |
878 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE, |
879 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00" |
880 |
|
+ BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(), |
881 |
|
getCurrentContext()); |
882 |
0
|
return ok; |
883 |
|
} |
884 |
4
|
return ok; |
885 |
|
} |
886 |
|
|
|
|
| 0% |
Uncovered Elements: 56 (56) |
Complexity: 9 |
Complexity Density: 0.21 |
|
887 |
0
|
private boolean check(final Existential existential, final int i, final Element element) {... |
888 |
0
|
final String context = currentContext.getLocationWithinModule(); |
889 |
0
|
boolean ok = true; |
890 |
0
|
final Element reference = getNormalizedLocalProofLineReference(existential.getReference()); |
891 |
0
|
if (reference == null) { |
892 |
0
|
ok = false; |
893 |
0
|
setLocationWithinModule(context + ".getReference()"); |
894 |
0
|
handleProofCheckException( |
895 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_CODE, |
896 |
|
BasicProofErrors.SUCH_A_LOCAL_LABEL_DOESNT_EXIST_TEXT |
897 |
|
+ existential.getReference(), |
898 |
|
getCurrentContext()); |
899 |
|
|
900 |
|
|
901 |
|
|
902 |
|
|
903 |
|
|
904 |
|
|
905 |
|
|
906 |
|
|
907 |
|
} else { |
908 |
0
|
final Element current = getNormalizedFormula(element); |
909 |
0
|
if (!FormulaUtility.isImplication(current)) { |
910 |
0
|
ok = false; |
911 |
0
|
setLocationWithinModule(context + ".getReference()"); |
912 |
0
|
handleProofCheckException( |
913 |
|
BasicProofErrors.IMPLICATION_EXPECTED_CODE, |
914 |
|
BasicProofErrors.IMPLICATION_EXPECTED_TEXT |
915 |
|
+ existential.getReference(), |
916 |
|
getCurrentContext()); |
917 |
0
|
return ok; |
918 |
|
} |
919 |
0
|
if (!FormulaUtility.isSubjectVariable(existential.getSubjectVariable())) { |
920 |
0
|
ok = false; |
921 |
0
|
setLocationWithinModule(context + ".getSubjectVariable()"); |
922 |
0
|
handleProofCheckException( |
923 |
|
BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_CODE, |
924 |
|
BasicProofErrors.SUBJECT_VARIABLE_IS_MISSING_TEXT, |
925 |
|
getCurrentContext()); |
926 |
0
|
return ok; |
927 |
|
} |
928 |
0
|
final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR); |
929 |
0
|
final ElementList exi = new DefaultElementList( |
930 |
|
Operators.EXISTENTIAL_QUANTIFIER_OPERATOR); |
931 |
0
|
exi.add(existential.getSubjectVariable()); |
932 |
0
|
exi.add(reference.getList().getElement(0)); |
933 |
0
|
expected.add(exi); |
934 |
0
|
expected.add((reference.getList().getElement(1))); |
935 |
0
|
if (!EqualsUtility.equals(current, expected)) { |
936 |
0
|
ok = false; |
937 |
0
|
handleProofCheckException( |
938 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_CODE, |
939 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_TEXT |
940 |
|
+ existential.getReference(), |
941 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
942 |
0
|
return ok; |
943 |
|
} |
944 |
|
} |
945 |
0
|
final RuleKey defined = checker.getRule(existential.getName()); |
946 |
0
|
if (defined == null) { |
947 |
0
|
ok = false; |
948 |
0
|
handleProofCheckException( |
949 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE, |
950 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
951 |
|
+ existential.getName(), |
952 |
|
getCurrentContext()); |
953 |
0
|
return ok; |
954 |
0
|
} else if (!supported.contains(defined.getVersion())) { |
955 |
0
|
ok = false; |
956 |
0
|
handleProofCheckException( |
957 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
958 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion() |
959 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
960 |
|
getCurrentContext()); |
961 |
0
|
return ok; |
962 |
0
|
} else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) { |
963 |
0
|
ok = false; |
964 |
0
|
handleProofCheckException( |
965 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE, |
966 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00" |
967 |
|
+ BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(), |
968 |
|
getCurrentContext()); |
969 |
0
|
return ok; |
970 |
|
} |
971 |
0
|
return ok; |
972 |
|
} |
973 |
|
|
|
|
| 51.3% |
Uncovered Elements: 38 (78) |
Complexity: 18 |
Complexity Density: 0.3 |
|
974 |
50
|
private boolean check(final ConditionalProof cp, final int i, final Element element) {... |
975 |
50
|
final ModuleAddress address = currentContext.getModuleLocation(); |
976 |
50
|
final String context = currentContext.getLocationWithinModule(); |
977 |
|
|
978 |
50
|
boolean ok = true; |
979 |
50
|
if (cp.getHypothesis() == null || cp.getHypothesis().getFormula() == null |
980 |
|
|| cp.getHypothesis().getFormula().getElement() == null) { |
981 |
0
|
ok = false; |
982 |
0
|
setLocationWithinModule(context + ".getHypothesis()"); |
983 |
0
|
handleProofCheckException( |
984 |
|
BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE, |
985 |
|
BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT, |
986 |
|
getCurrentContext()); |
987 |
0
|
return ok; |
988 |
|
} |
989 |
50
|
if (cp.getFormalProofLineList() == null || cp.getFormalProofLineList().size() <= 0) { |
990 |
0
|
ok = false; |
991 |
0
|
setLocationWithinModule(context + ".getFormalProofLineList()"); |
992 |
0
|
handleProofCheckException( |
993 |
|
BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_CODE, |
994 |
|
BasicProofErrors.MISSING_PROOF_LINE_FOR_CONDITIONAL_PROOF_TEXT, |
995 |
|
getCurrentContext()); |
996 |
0
|
return ok; |
997 |
|
} |
998 |
50
|
final ReferenceResolver newResolver = new ReferenceResolver() { |
999 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
1000 |
365
|
public Element getNormalizedFormula(final Element formula) {... |
1001 |
365
|
return ProofChecker2Impl.this.getNormalizedFormula(formula); |
1002 |
|
} |
1003 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1004 |
7
|
public Element getNormalizedReferenceFormula(final String reference) {... |
1005 |
|
|
1006 |
7
|
if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) { |
1007 |
0
|
return resolver.getNormalizedFormula(cp.getHypothesis().getFormula() |
1008 |
|
.getElement()); |
1009 |
|
} |
1010 |
7
|
return ProofChecker2Impl.this.getNormalizedReferenceFormula(reference); |
1011 |
|
} |
1012 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1013 |
7
|
public boolean isProvedFormula(final String reference) {... |
1014 |
7
|
if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) { |
1015 |
0
|
return true; |
1016 |
|
} |
1017 |
7
|
return ProofChecker2Impl.this.isProvedFormula(reference); |
1018 |
|
} |
1019 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1020 |
191
|
public boolean isLocalProofLineReference(final String reference) {... |
1021 |
191
|
if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) { |
1022 |
0
|
return true; |
1023 |
|
} |
1024 |
191
|
return ProofChecker2Impl.this.isLocalProofLineReference(reference); |
1025 |
|
} |
1026 |
|
|
|
|
| 0% |
Uncovered Elements: 5 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1027 |
0
|
public ModuleContext getReferenceContext(final String reference) {... |
1028 |
0
|
if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) { |
1029 |
0
|
return new ModuleContext(address, context |
1030 |
|
+ ".getHypothesis().getLabel()"); |
1031 |
|
} |
1032 |
0
|
return ProofChecker2Impl.this.getReferenceContext(reference); |
1033 |
|
} |
1034 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1035 |
168
|
public Element getNormalizedLocalProofLineReference(final String reference) {... |
1036 |
|
|
1037 |
168
|
if (EqualsUtility.equals(reference, cp.getHypothesis().getLabel())) { |
1038 |
|
|
1039 |
62
|
return resolver.getNormalizedFormula( |
1040 |
|
cp.getHypothesis().getFormula().getElement()); |
1041 |
|
} |
1042 |
106
|
return ProofChecker2Impl.this.getNormalizedLocalProofLineReference(reference); |
1043 |
|
} |
1044 |
|
|
1045 |
|
}; |
1046 |
50
|
final int last = cp.getFormalProofLineList().size() - 1; |
1047 |
50
|
setLocationWithinModule(context + ".getFormalProofLineList().get(" + last + ")"); |
1048 |
50
|
final FormalProofLine line = cp.getFormalProofLineList().get(last); |
1049 |
50
|
if (line == null || line.getFormula() == null |
1050 |
|
|| line.getFormula().getElement() == null) { |
1051 |
0
|
ok = false; |
1052 |
0
|
handleProofCheckException( |
1053 |
|
BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE, |
1054 |
|
BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT, |
1055 |
|
getCurrentContext()); |
1056 |
0
|
return ok; |
1057 |
|
} |
1058 |
50
|
final Element lastFormula = resolver.getNormalizedFormula(line.getFormula().getElement()); |
1059 |
50
|
final ElementList newConditions = (ElementList) conditions.copy(); |
1060 |
|
|
1061 |
50
|
newConditions.add(cp.getHypothesis().getFormula().getElement()); |
1062 |
50
|
setLocationWithinModule(context + ".getFormalProofLineList()"); |
1063 |
50
|
final LogicalCheckExceptionList eList = (new ProofChecker2Impl()).checkProof( |
1064 |
|
newConditions, lastFormula, cp.getFormalProofLineList(), checker, getCurrentContext(), |
1065 |
|
newResolver); |
1066 |
50
|
exceptions.add(eList); |
1067 |
50
|
ok = eList.size() == 0; |
1068 |
50
|
setLocationWithinModule(context + ".getConclusion()"); |
1069 |
50
|
if (cp.getConclusion() == null || cp.getConclusion().getFormula() == null |
1070 |
|
|| cp.getConclusion().getFormula().getElement() == null) { |
1071 |
0
|
ok = false; |
1072 |
0
|
handleProofCheckException( |
1073 |
|
BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_CODE, |
1074 |
|
BasicProofErrors.PROOF_LINE_MUST_NOT_BE_NULL_TEXT, |
1075 |
|
getCurrentContext()); |
1076 |
0
|
return ok; |
1077 |
|
} |
1078 |
50
|
final Element c = resolver.getNormalizedFormula(cp.getConclusion().getFormula().getElement()); |
1079 |
50
|
setLocationWithinModule(context + ".getConclusion().getFormula().getElement()"); |
1080 |
50
|
if (!FormulaUtility.isImplication(c)) { |
1081 |
0
|
ok = false; |
1082 |
0
|
handleProofCheckException( |
1083 |
|
BasicProofErrors.IMPLICATION_EXPECTED_CODE, |
1084 |
|
BasicProofErrors.IMPLICATION_EXPECTED_TEXT, |
1085 |
|
getCurrentContext()); |
1086 |
0
|
return ok; |
1087 |
|
} |
1088 |
50
|
final DefaultElementList expected = new DefaultElementList(Operators.IMPLICATION_OPERATOR); |
1089 |
50
|
expected.add(cp.getHypothesis().getFormula().getElement()); |
1090 |
50
|
expected.add(lastFormula); |
1091 |
|
|
1092 |
|
|
1093 |
50
|
if (!EqualsUtility.equals(cp.getConclusion().getFormula().getElement(), expected)) { |
1094 |
|
|
1095 |
|
|
1096 |
0
|
ok = false; |
1097 |
0
|
handleProofCheckException( |
1098 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_CODE, |
1099 |
|
BasicProofErrors.EXPECTED_FORMULA_DIFFERS_2_TEXT, |
1100 |
|
getDiffModuleContextOfProofLineFormula(i, expected)); |
1101 |
0
|
return ok; |
1102 |
|
} |
1103 |
50
|
final RuleKey defined = checker.getRule(cp.getName()); |
1104 |
50
|
if (defined == null) { |
1105 |
0
|
ok = false; |
1106 |
0
|
handleProofCheckException( |
1107 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_CODE, |
1108 |
|
BasicProofErrors.PROOF_METHOD_WAS_NOT_DEFINED_YET_TEXT |
1109 |
|
+ cp.getName(), |
1110 |
|
getCurrentContext()); |
1111 |
0
|
return ok; |
1112 |
50
|
} else if (!supported.contains(defined.getVersion())) { |
1113 |
0
|
ok = false; |
1114 |
0
|
handleProofCheckException( |
1115 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_CODE, |
1116 |
|
BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT + defined.getVersion() |
1117 |
|
+ BasicProofErrors.PROOF_METHOD_IS_NOT_SUPPORTED_TEXT2 + supported, |
1118 |
|
getCurrentContext()); |
1119 |
0
|
return ok; |
1120 |
50
|
} else if (hasConditions() && !Version.equals("0.02.00", defined.getVersion())) { |
1121 |
0
|
ok = false; |
1122 |
0
|
handleProofCheckException( |
1123 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_CODE, |
1124 |
|
BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT + "0.02.00" |
1125 |
|
+ BasicProofErrors.HIGHER_PROOF_RULE_VERSION_NEEDED_TEXT2 + defined.getVersion(), |
1126 |
|
getCurrentContext()); |
1127 |
0
|
return ok; |
1128 |
|
} |
1129 |
50
|
return ok; |
1130 |
|
} |
1131 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1132 |
1
|
private ModuleContext getModuleContextOfProofLineFormula(final int i) {... |
1133 |
1
|
if (proof.get(i) instanceof ConditionalProof) { |
1134 |
0
|
return new ModuleContext(moduleContext.getModuleLocation(), |
1135 |
|
moduleContext.getLocationWithinModule() + ".get(" + i |
1136 |
|
+ ").getConclusion().getFormula().getElement()"); |
1137 |
|
} |
1138 |
1
|
return new ModuleContext(moduleContext.getModuleLocation(), |
1139 |
|
moduleContext.getLocationWithinModule() + ".get(" + i |
1140 |
|
+ ").getFormula().getElement()"); |
1141 |
|
} |
1142 |
|
|
|
|
| 0% |
Uncovered Elements: 6 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
1143 |
0
|
private ModuleContext getDiffModuleContextOfProofLineFormula(final int i,... |
1144 |
|
final Element expected) { |
1145 |
0
|
final String diff = FormulaUtility.getDifferenceLocation( |
1146 |
|
proof.get(i).getFormula().getElement(), expected); |
1147 |
0
|
if (proof.get(i) instanceof ConditionalProof) { |
1148 |
0
|
return new ModuleContext(moduleContext.getModuleLocation(), |
1149 |
|
moduleContext.getLocationWithinModule() + ".get(" + i |
1150 |
|
+ ").getConclusion().getFormula().getElement()" + diff); |
1151 |
|
} |
1152 |
0
|
return new ModuleContext(moduleContext.getModuleLocation(), |
1153 |
|
moduleContext.getLocationWithinModule() + ".get(" + i |
1154 |
|
+ ").getFormula().getElement()" + diff); |
1155 |
|
} |
1156 |
|
|
1157 |
|
|
1158 |
|
|
1159 |
|
|
1160 |
|
@return |
1161 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
1162 |
890
|
private boolean hasConditions() {... |
1163 |
890
|
return conditions.size() > 0; |
1164 |
|
} |
1165 |
|
|
|
|
| 60% |
Uncovered Elements: 4 (10) |
Complexity: 4 |
Complexity Density: 0.67 |
|
1166 |
379
|
private Element getNormalizedProofLine(final Integer n) {... |
1167 |
379
|
if (n == null) { |
1168 |
0
|
return null; |
1169 |
|
} |
1170 |
379
|
int i = n.intValue(); |
1171 |
379
|
if (i < 0 || i >= proof.size()) { |
1172 |
0
|
return null; |
1173 |
|
} |
1174 |
379
|
return resolver.getNormalizedFormula(proof.get(i).getFormula().getElement()); |
1175 |
|
} |
1176 |
|
|
1177 |
|
|
1178 |
|
@link |
1179 |
|
|
1180 |
|
@param |
1181 |
|
@param |
1182 |
|
@param |
1183 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (2) |
Complexity: 1 |
Complexity Density: 0.5 |
|
1184 |
1
|
private void handleProofCheckException(final int code, final String msg,... |
1185 |
|
final ModuleContext context) { |
1186 |
|
|
1187 |
|
|
1188 |
1
|
final ProofCheckException ex = new ProofCheckException(code, msg, context); |
1189 |
1
|
exceptions.add(ex); |
1190 |
|
} |
1191 |
|
|
1192 |
|
|
1193 |
|
@link |
1194 |
|
|
1195 |
|
@param |
1196 |
|
@param |
1197 |
|
@param |
1198 |
|
@param |
1199 |
|
|
|
|
| 0% |
Uncovered Elements: 2 (2) |
Complexity: 1 |
Complexity Density: 0.5 |
|
1200 |
0
|
private void handleProofCheckException(final int code, final String msg,... |
1201 |
|
final ModuleContext context, final ModuleContext referenceContext) { |
1202 |
|
|
1203 |
|
|
1204 |
0
|
final ProofCheckException ex = new ProofCheckException(code, msg, null, context, |
1205 |
|
referenceContext); |
1206 |
0
|
exceptions.add(ex); |
1207 |
|
} |
1208 |
|
|
1209 |
|
|
1210 |
|
|
1211 |
|
|
1212 |
|
@return |
1213 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
1214 |
4790
|
protected final ModuleContext getCurrentContext() {... |
1215 |
4790
|
return currentContext; |
1216 |
|
} |
1217 |
|
|
1218 |
|
|
1219 |
|
|
1220 |
|
|
1221 |
|
@param |
1222 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
1223 |
927
|
protected void setLocationWithinModule(final String locationWithinModule) {... |
1224 |
927
|
getCurrentContext().setLocationWithinModule(locationWithinModule); |
1225 |
|
} |
1226 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1227 |
7
|
public boolean isProvedFormula(final String reference) {... |
1228 |
7
|
if (label2line.containsKey(reference)) { |
1229 |
0
|
return lineProved[((Integer) label2line.get(reference)).intValue()]; |
1230 |
|
} |
1231 |
7
|
return resolver.isProvedFormula(reference); |
1232 |
|
} |
1233 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1234 |
7
|
public Element getNormalizedReferenceFormula(final String reference) {... |
1235 |
|
|
1236 |
7
|
if (label2line.containsKey(reference)) { |
1237 |
|
|
1238 |
0
|
return getNormalizedProofLine((Integer) label2line.get(reference)); |
1239 |
|
} |
1240 |
|
|
1241 |
7
|
return resolver.getNormalizedReferenceFormula(reference); |
1242 |
|
} |
1243 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
1244 |
503
|
public Element getNormalizedFormula(final Element element) {... |
1245 |
503
|
return resolver.getNormalizedFormula(element); |
1246 |
|
} |
1247 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0.67 |
|
1248 |
636
|
public boolean isLocalProofLineReference(final String reference) {... |
1249 |
636
|
if (label2line.containsKey(reference)) { |
1250 |
0
|
return true; |
1251 |
|
} |
1252 |
636
|
return resolver.isLocalProofLineReference(reference); |
1253 |
|
} |
1254 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
1255 |
547
|
public Element getNormalizedLocalProofLineReference(final String reference) {... |
1256 |
|
|
1257 |
547
|
if (label2line.containsKey(reference)) { |
1258 |
|
|
1259 |
379
|
return getNormalizedProofLine((Integer) label2line.get(reference)); |
1260 |
|
} |
1261 |
|
|
1262 |
168
|
final Element result = resolver.getNormalizedLocalProofLineReference(reference); |
1263 |
|
|
1264 |
|
|
1265 |
|
|
1266 |
|
|
1267 |
|
|
1268 |
168
|
return result; |
1269 |
|
} |
1270 |
|
|
|
|
| 0% |
Uncovered Elements: 6 (6) |
Complexity: 2 |
Complexity Density: 0.5 |
|
1271 |
0
|
public ModuleContext getReferenceContext(final String reference) {... |
1272 |
0
|
if (label2line.containsKey(reference)) { |
1273 |
0
|
final ModuleContext lc = new ModuleContext(moduleContext.getModuleLocation(), |
1274 |
|
moduleContext.getLocationWithinModule() + ".get(" |
1275 |
|
+ label2line.get(reference) |
1276 |
|
+ ").getLabel()"); |
1277 |
0
|
return lc; |
1278 |
|
} |
1279 |
0
|
return resolver.getReferenceContext(reference); |
1280 |
|
} |
1281 |
|
|
1282 |
|
} |