Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart6.png 80% of files have more coverage
197   512   82   7.3
90   433   0.42   27
27     3.04  
1    
 
  FormalProofCheckerExecutor       Line # 70 197 82 57.6% 0.5764331
 
  (1)
 
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.service.logic;
17   
18   
19    import org.qedeq.base.io.Parameters;
20    import org.qedeq.base.io.Version;
21    import org.qedeq.base.trace.Trace;
22    import org.qedeq.base.utility.StringUtility;
23    import org.qedeq.kernel.bo.log.QedeqLog;
24    import org.qedeq.kernel.bo.logic.ProofCheckerFactoryImpl;
25    import org.qedeq.kernel.bo.logic.common.FormulaUtility;
26    import org.qedeq.kernel.bo.logic.common.FunctionKey;
27    import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
28    import org.qedeq.kernel.bo.logic.common.PredicateKey;
29    import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
30    import org.qedeq.kernel.bo.logic.proof.checker.ProofCheckException;
31    import org.qedeq.kernel.bo.logic.proof.common.ProofCheckerFactory;
32    import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
33    import org.qedeq.kernel.bo.module.ControlVisitor;
34    import org.qedeq.kernel.bo.module.InternalServiceCall;
35    import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
36    import org.qedeq.kernel.bo.module.KernelQedeqBo;
37    import org.qedeq.kernel.bo.module.PluginExecutor;
38    import org.qedeq.kernel.bo.module.Reference;
39    import org.qedeq.kernel.se.base.list.Element;
40    import org.qedeq.kernel.se.base.list.ElementList;
41    import org.qedeq.kernel.se.base.module.Axiom;
42    import org.qedeq.kernel.se.base.module.ChangedRule;
43    import org.qedeq.kernel.se.base.module.ChangedRuleList;
44    import org.qedeq.kernel.se.base.module.FormalProof;
45    import org.qedeq.kernel.se.base.module.FormalProofLineList;
46    import org.qedeq.kernel.se.base.module.FunctionDefinition;
47    import org.qedeq.kernel.se.base.module.Header;
48    import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
49    import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
50    import org.qedeq.kernel.se.base.module.PredicateDefinition;
51    import org.qedeq.kernel.se.base.module.Proposition;
52    import org.qedeq.kernel.se.base.module.Rule;
53    import org.qedeq.kernel.se.common.CheckLevel;
54    import org.qedeq.kernel.se.common.ModuleContext;
55    import org.qedeq.kernel.se.common.ModuleDataException;
56    import org.qedeq.kernel.se.common.Plugin;
57    import org.qedeq.kernel.se.common.RuleKey;
58    import org.qedeq.kernel.se.common.SourceFileException;
59    import org.qedeq.kernel.se.common.SourceFileExceptionList;
60    import org.qedeq.kernel.se.dto.list.DefaultAtom;
61    import org.qedeq.kernel.se.dto.list.DefaultElementList;
62    import org.qedeq.kernel.se.state.FormallyProvedState;
63   
64   
65    /**
66    * Checks if all propositions have a correct formal proof.
67    *
68    * @author Michael Meyling
69    */
 
70    public final class FormalProofCheckerExecutor extends ControlVisitor implements PluginExecutor,
71    ReferenceResolver, RuleChecker {
72   
73    /** This class. */
74    private static final Class CLASS = FormalProofCheckerExecutor.class;
75   
76    /** Factory for generating new checkers. */
77    private ProofCheckerFactory checkerFactory = null;
78   
79    /** Rule version the module claims to use at maximum. */
80    private Version ruleVersion;
81   
82    /**
83    * Constructor.
84    *
85    * @param plugin This plugin we work for.
86    * @param qedeq QEDEQ BO object.
87    * @param parameters Parameters.
88    */
 
89  10 toggle FormalProofCheckerExecutor(final Plugin plugin, final KernelQedeqBo qedeq,
90    final Parameters parameters) {
91  10 super(plugin, qedeq);
92  10 final String method = "FormalProofCheckerExecutor(Plugin, KernelQedeqBo, Map)";
93  10 final String checkerFactoryClass = parameters.getString("checkerFactory");
94  10 if (checkerFactoryClass != null && checkerFactoryClass.length() > 0) {
95  10 try {
96  10 Class cl = Class.forName(checkerFactoryClass);
97  10 checkerFactory = (ProofCheckerFactory) cl.newInstance();
98    } catch (ClassNotFoundException e) {
99  0 Trace.fatal(CLASS, this, method, "ProofCheckerFactory class not in class path: "
100    + checkerFactoryClass, e);
101    } catch (InstantiationException e) {
102  0 Trace.fatal(CLASS, this, method, "ProofCheckerFactory class could not be instanciated: "
103    + checkerFactoryClass, e);
104    } catch (IllegalAccessException e) {
105  0 Trace.fatal(CLASS, this, method,
106    "Programming error, access for instantiation failed for model: "
107    + checkerFactoryClass, e);
108    } catch (RuntimeException e) {
109  0 Trace.fatal(CLASS, this, method,
110    "Programming error, instantiation failed for model: " + checkerFactoryClass, e);
111    }
112    }
113    // fallback is the default checker factory
114  10 if (checkerFactory == null) {
115  0 checkerFactory = new ProofCheckerFactoryImpl();
116    }
117    }
118   
 
119  10 toggle public Object executePlugin(final InternalServiceCall call, final Object data) {
120    // we set this as module rule version, and hope it will be changed
121  10 ruleVersion = new Version("0.00.00");
122  10 QedeqLog.getInstance().logRequest(
123    "Check logical correctness", getQedeqBo().getUrl());
124  10 getServices().checkWellFormedness(call.getInternalServiceProcess(), getQedeqBo());
125  10 if (!getQedeqBo().isWellFormed()) {
126  0 final String msg = "Check of logical correctness failed";
127  0 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
128    "Module is not even well formed.");
129  0 return Boolean.FALSE;
130    }
131  10 getQedeqBo().setFormallyProvedProgressState(FormallyProvedState.STATE_EXTERNAL_CHECKING);
132  10 getQedeqBo().getLabels().resetNodesToProvedUnchecked();
133  10 final KernelModuleReferenceList list = getQedeqBo().getKernelRequiredModules();
134  10 for (int i = 0; i < list.size(); i++) {
135  0 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", list.getLabel(i));
136  0 getServices().checkFormallyProved(call.getInternalServiceProcess(), list.getKernelQedeqBo(i));
137  0 if (list.getKernelQedeqBo(i).hasErrors()) {
138  0 addError(new CheckRequiredModuleException(
139    LogicErrors.MODULE_IMPORT_CHECK_FAILED_CODE,
140    LogicErrors.MODULE_IMPORT_CHECK_FAILED_TEXT
141    + list.getQedeqBo(i).getModuleAddress(),
142    list.getModuleContext(i)));
143    }
144    }
145    // has at least one import errors?
146  10 if (getQedeqBo().hasErrors()) {
147  0 getQedeqBo().setFormallyProvedFailureState(FormallyProvedState.STATE_EXTERNAL_CHECKING_FAILED,
148    getErrorList());
149  0 final String msg = "Check of logical correctness failed";
150  0 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
151    StringUtility.replace(getQedeqBo().getErrors().getMessage(), "\n", "\n\t"));
152  0 return Boolean.FALSE;
153    }
154  10 getQedeqBo().setFormallyProvedProgressState(FormallyProvedState.STATE_INTERNAL_CHECKING);
155  10 try {
156  10 traverse(call.getInternalServiceProcess());
157    } catch (SourceFileExceptionList e) {
158  5 getQedeqBo().setFormallyProvedFailureState(FormallyProvedState.STATE_INTERNAL_CHECKING_FAILED,
159    getErrorList());
160  5 final String msg = "Check of logical correctness failed";
161  5 QedeqLog.getInstance().logFailureReply(msg, getQedeqBo().getUrl(),
162    StringUtility.replace(e.getMessage(), "\n", "\n\t"));
163  5 return Boolean.FALSE;
164    }
165  5 getQedeqBo().setFormallyProvedProgressState(FormallyProvedState.STATE_CHECKED);
166  5 QedeqLog.getInstance().logSuccessfulReply(
167    "Check of logical correctness successful", getQedeqBo().getUrl());
168  5 return Boolean.TRUE;
169    }
170   
 
171  10 toggle public void visitEnter(final Header header) throws ModuleDataException {
172  10 if (header.getSpecification() == null
173    || header.getSpecification().getRuleVersion() == null) {
174  0 return;
175    }
176  10 final String context = getCurrentContext().getLocationWithinModule();
177  10 setLocationWithinModule(context + ".getSpecification().getRuleVersion()");
178  10 final String version = header.getSpecification().getRuleVersion().trim();
179  10 if (!checkerFactory.isRuleVersionSupported(version)) {
180  0 addError(new ProofCheckException(
181    LogicErrors.RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_CODE,
182    LogicErrors.RULE_VERSION_HAS_STILL_NO_PROOF_CHECKER_TEXT + version,
183    getCurrentContext()));
184    } else {
185  10 try {
186  10 ruleVersion = new Version(version);
187    } catch (RuntimeException e) {
188  0 addError(new ProofCheckException(
189    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_CODE,
190    LogicErrors.THIS_IS_NOT_VALID_VERSION_FORMAT_TEXT + version,
191    getCurrentContext()));
192    }
193    }
194  10 setLocationWithinModule(context);
195    }
196   
 
197  62 toggle public void visitEnter(final Axiom axiom) throws ModuleDataException {
198  62 if (getNodeBo().isWellFormed()) {
199  62 getNodeBo().setProved(CheckLevel.SUCCESS);
200    } else {
201  0 getNodeBo().setProved(CheckLevel.FAILURE);
202  0 addError(new ProofCheckException(
203    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
204    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
205    getCurrentContext()));
206  0 return;
207    }
208  62 setBlocked(true);
209    }
210   
 
211  62 toggle public void visitLeave(final Axiom axiom) {
212  62 setBlocked(false);
213    }
214   
 
215  0 toggle public void visitEnter(final PredicateDefinition definition)
216    throws ModuleDataException {
217  0 if (getNodeBo().isWellFormed()) {
218  0 getNodeBo().setProved(CheckLevel.SUCCESS);
219    } else {
220  0 getNodeBo().setProved(CheckLevel.FAILURE);
221  0 addError(new ProofCheckException(
222    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
223    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
224    getCurrentContext()));
225  0 return;
226    }
227  0 setBlocked(true);
228    }
229   
 
230  0 toggle public void visitLeave(final PredicateDefinition definition) {
231  0 setBlocked(false);
232    }
233   
 
234  0 toggle public void visitEnter(final InitialPredicateDefinition definition)
235    throws ModuleDataException {
236  0 if (getNodeBo().isWellFormed()) {
237  0 getNodeBo().setProved(CheckLevel.SUCCESS);
238    } else {
239  0 getNodeBo().setProved(CheckLevel.FAILURE);
240  0 addError(new ProofCheckException(
241    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
242    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
243    getCurrentContext()));
244  0 return;
245    }
246  0 setBlocked(true);
247    }
248   
 
249  0 toggle public void visitLeave(final InitialPredicateDefinition definition) {
250  0 setBlocked(false);
251    }
252   
 
253  0 toggle public void visitEnter(final InitialFunctionDefinition definition)
254    throws ModuleDataException {
255  0 if (getNodeBo().isWellFormed()) {
256  0 getNodeBo().setProved(CheckLevel.SUCCESS);
257    } else {
258  0 getNodeBo().setProved(CheckLevel.FAILURE);
259  0 addError(new ProofCheckException(
260    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
261    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
262    getCurrentContext()));
263  0 return;
264    }
265  0 setBlocked(true);
266    }
267   
 
268  0 toggle public void visitLeave(final InitialFunctionDefinition definition) {
269  0 setBlocked(false);
270    }
271   
 
272  0 toggle public void visitEnter(final FunctionDefinition definition)
273    throws ModuleDataException {
274  0 if (getNodeBo().isWellFormed()) {
275  0 getNodeBo().setProved(CheckLevel.SUCCESS);
276    } else {
277  0 getNodeBo().setProved(CheckLevel.FAILURE);
278  0 addError(new ProofCheckException(
279    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
280    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
281    getCurrentContext()));
282  0 return;
283    }
284  0 setBlocked(true);
285    }
286   
 
287  0 toggle public void visitLeave(final FunctionDefinition definition) {
288  0 setBlocked(false);
289    }
290   
 
291  78 toggle public void visitEnter(final Proposition proposition)
292    throws ModuleDataException {
293    // we only check this node, if the well formed check was successful
294  78 if (!getNodeBo().isWellFormed()) {
295  0 getNodeBo().setProved(CheckLevel.FAILURE);
296  0 addError(new ProofCheckException(
297    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_CODE,
298    LogicErrors.NODE_FORMULAS_MUST_BE_WELL_FORMED_TEXT,
299    getCurrentContext()));
300  0 return;
301    }
302  78 getNodeBo().setProved(CheckLevel.UNCHECKED);
303  78 if (proposition.getFormula() == null) {
304  0 getNodeBo().setProved(CheckLevel.FAILURE);
305  0 addError(new ProofCheckException(
306    LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_CODE,
307    LogicErrors.PROPOSITION_FORMULA_MUST_NOT_BE_NULL_TEXT,
308    getCurrentContext()));
309  0 return;
310    }
311  78 final String context = getCurrentContext().getLocationWithinModule();
312  78 boolean correctProofFound = false;
313    // we start checking
314  78 if (proposition.getFormalProofList() != null) {
315  144 for (int i = 0; i < proposition.getFormalProofList().size(); i++) {
316  72 final FormalProof proof = proposition.getFormalProofList().get(i);
317  72 if (proof != null) {
318  72 final FormalProofLineList list = proof.getFormalProofLineList();
319  72 if (list != null) {
320  72 setLocationWithinModule(context + ".getFormalProofList().get("
321    + i + ").getFormalProofLineList()");
322  72 LogicalCheckExceptionList eList
323    = checkerFactory.createProofChecker(ruleVersion).checkProof(
324    proposition.getFormula().getElement(), list, this,
325    getCurrentContext(),
326    this);
327  72 if (!correctProofFound && eList.size() == 0) {
328  62 correctProofFound = true;
329    }
330  140 for (int j = 0; j < eList.size(); j++) {
331  68 addError(eList.get(j));
332    }
333    }
334    }
335    }
336    }
337  78 setLocationWithinModule(context + ".getFormula()");
338    // only if we found at least one error free formal proof
339  78 if (correctProofFound) {
340  62 getNodeBo().setProved(CheckLevel.SUCCESS);
341    } else {
342  16 getNodeBo().setProved(CheckLevel.FAILURE);
343  16 addError(new ProofCheckException(
344    LogicErrors.NO_FORMAL_PROOF_FOUND_CODE,
345    LogicErrors.NO_FORMAL_PROOF_FOUND_TEXT,
346    getCurrentContext()));
347    }
348  78 setBlocked(true);
349    }
350   
 
351  78 toggle public void visitLeave(final Proposition definition) {
352  78 setBlocked(false);
353    }
354   
 
355  81 toggle public void visitEnter(final Rule rule) throws ModuleDataException {
356  81 final String context = getCurrentContext().getLocationWithinModule();
357    // FIXME 20110618 m31: check if this is really a higher version than before?
358    // FIXME 20130413 m31: why we don't use the following method:
359    /// checkerFactory.createProofChecker(ruleVersion).checkRule
360  81 getNodeBo().setProved(CheckLevel.UNCHECKED);
361  81 final ChangedRuleList list = rule.getChangedRuleList();
362  89 for (int i = 0; list != null && i < list.size(); i++) {
363  8 setLocationWithinModule(context + ".getChangedRuleList().get(" + i + ").getVersion()");
364  8 final ChangedRule r = list.get(i);
365  8 if (!Version.equals(rule.getVersion(), r.getVersion())) {
366  0 addError(new ProofCheckException(
367    LogicErrors.OTHER_RULE_VERSION_EXPECTED_CODE,
368    LogicErrors.OTHER_RULE_VERSION_EXPECTED_TEXT1 + rule.getVersion()
369    + LogicErrors.OTHER_RULE_VERSION_EXPECTED_TEXT2 + r.getVersion(),
370    getCurrentContext()));
371    }
372    }
373   
374  81 if (getNodeBo().isNotProved()) {
375  0 getNodeBo().setProved(CheckLevel.SUCCESS);
376    } else {
377  81 getNodeBo().setProved(CheckLevel.FAILURE);
378    }
379    }
380   
 
381  84 toggle protected void addError(final ModuleDataException me) {
382  84 if (getNodeBo() != null) {
383  84 getNodeBo().setProved(CheckLevel.FAILURE);
384    }
385  84 super.addError(me);
386    }
387   
 
388  84 toggle protected void addError(final SourceFileException me) {
389  84 if (getNodeBo() != null) {
390  84 getNodeBo().setProved(CheckLevel.FAILURE);
391    }
392  84 super.addError(me);
393    }
394   
 
395  318 toggle public boolean isProvedFormula(final String reference) {
396  318 final String method = "hasProvedFormula";
397  318 final Reference ref = getReference(reference, getCurrentContext(), false, false);
398  318 if (ref == null) {
399  0 Trace.info(CLASS, method, "ref == null");
400  0 return false;
401    }
402  318 if (ref.isExternalModuleReference()) {
403  0 Trace.info(CLASS, method, "ref is external module");
404  0 return false;
405    }
406  318 if (!ref.isNodeReference()) {
407  0 Trace.info(CLASS, method, "ref is no node reference");
408  0 return false;
409    }
410  318 if (null == ref.getNode()) {
411  3 Trace.info(CLASS, method, "ref node == null");
412  3 return false;
413    }
414  315 if (ref.isSubReference()) {
415  0 return false;
416    }
417  315 if (!ref.isProofLineReference()) {
418  315 if (!ref.getNode().isProved()) {
419  1 Trace.info(CLASS, method, "ref node is not marked as proved: " + reference);
420    }
421  315 if (!ref.getNode().isProved()) {
422  1 return false;
423    }
424  314 if (!ref.getNode().hasFormula()) {
425  0 Trace.info(CLASS, method, "node has no formula: " + reference);
426  0 return false;
427    }
428  314 return ref.getNode().isProved();
429    }
430  0 Trace.info(CLASS, method, "proof line references are not ok!");
431  0 return false;
432    }
433   
 
434  157 toggle public Element getNormalizedReferenceFormula(final String reference) {
435  157 if (!isProvedFormula(reference)) {
436  0 return null;
437    }
438  157 final Reference ref = getReference(reference, getCurrentContext(), false, false);
439  157 final Element formula = ref.getNode().getFormula();
440  157 return getNormalizedFormula(ref.getNode().getQedeqBo(), formula);
441    }
442   
 
443  2017 toggle public Element getNormalizedFormula(final Element formula) {
444  2017 return getNormalizedFormula(getQedeqBo(), formula);
445    }
446   
 
447  25672 toggle private Element getNormalizedFormula(final KernelQedeqBo qedeq, final Element formula) {
448  25672 if (formula == null) {
449  3 return null;
450    }
451  25669 if (formula.isAtom()) {
452  9780 return new DefaultAtom(formula.getAtom().getString());
453    }
454  15889 return getNormalizedFormula(qedeq, formula.getList());
455    }
456   
 
457  15889 toggle private ElementList getNormalizedFormula(final KernelQedeqBo qedeq, final ElementList formula) {
458  15889 final ElementList result = new DefaultElementList(formula.getOperator());
459  15889 if (FormulaUtility.isPredicateConstant(formula)) {
460  0 final PredicateKey key = new PredicateKey(formula.getElement(0).getAtom().getString(),
461    "" + (formula.getList().size() - 1));
462  0 final DefaultAtom atom = new DefaultAtom(
463    qedeq.getExistenceChecker().get(key).getContext().getModuleLocation().getUrl()
464    + "$" + key.getName());
465  0 result.add(atom);
466  0 for (int i = 1; i < formula.size(); i++) {
467  0 result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
468    }
469  15889 } else if (FormulaUtility.isFunctionConstant(formula)) {
470  0 final FunctionKey key = new FunctionKey(formula.getElement(0).getAtom().getString(),
471    "" + (formula.getList().size() - 1));
472  0 final DefaultAtom atom = new DefaultAtom(
473    qedeq.getExistenceChecker().get(key).getContext().getModuleLocation().getUrl()
474    + "$" + key.getName());
475  0 result.add(atom);
476  0 for (int i = 1; i < formula.size(); i++) {
477  0 result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
478    }
479    } else {
480  39387 for (int i = 0; i < formula.size(); i++) {
481  23498 result.add(getNormalizedFormula(qedeq, formula.getElement(i)));
482    }
483    }
484  15889 return result;
485    }
486   
 
487  397 toggle public boolean isLocalProofLineReference(final String reference) {
488    // here we have no proof lines
489  397 return false;
490    }
491   
 
492  0 toggle public ModuleContext getReferenceContext(final String reference) {
493    // here we have no proof lines
494  0 return null;
495    }
496   
 
497  0 toggle public Element getNormalizedLocalProofLineReference(final String reference) {
498    // here we have no proof lines
499  0 return null;
500    }
501   
 
502  732 toggle public RuleKey getRule(final String ruleName) {
503  732 final RuleKey local = getLocalRuleKey(ruleName);
504  732 if (local == null) {
505  0 return getQedeqBo().getExistenceChecker().getParentRuleKey(
506    ruleName);
507    }
508  732 return local;
509    }
510   
511   
512    }
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .