Clover Coverage Report
Coverage timestamp: Sa Aug 2 2008 13:56:27 CEST
../../../../../img/srcFileCovDistChart8.png 47% of files have more coverage
93   259   39   6,64
42   194   0,42   14
14     2,79  
1    
 
  QedeqBoFormalLogicChecker       Line # 50 93 39 79,9% 0.7986577
 
  (21)
 
1    /* $Id: QedeqBoFormalLogicChecker.java,v 1.1 2008/07/26 07:58:29 m31 Exp $
2    *
3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
4    *
5    * Copyright 2000-2008, Michael Meyling <mime@qedeq.org>.
6    *
7    * "Hilbert II" is free software; you can redistribute
8    * it and/or modify it under the terms of the GNU General Public
9    * License as published by the Free Software Foundation; either
10    * version 2 of the License, or (at your option) any later version.
11    *
12    * This program is distributed in the hope that it will be useful,
13    * but WITHOUT ANY WARRANTY; without even the implied warranty of
14    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15    * GNU General Public License for more details.
16    */
17   
18    package org.qedeq.kernel.bo.service;
19   
20    import org.qedeq.base.trace.Trace;
21    import org.qedeq.kernel.base.module.Axiom;
22    import org.qedeq.kernel.base.module.Formula;
23    import org.qedeq.kernel.base.module.FunctionDefinition;
24    import org.qedeq.kernel.base.module.PredicateDefinition;
25    import org.qedeq.kernel.base.module.Proposition;
26    import org.qedeq.kernel.base.module.Rule;
27    import org.qedeq.kernel.base.module.Term;
28    import org.qedeq.kernel.bo.logic.FormulaChecker;
29    import org.qedeq.kernel.bo.logic.wf.ExistenceChecker;
30    import org.qedeq.kernel.bo.logic.wf.Function;
31    import org.qedeq.kernel.bo.logic.wf.HigherLogicalErrors;
32    import org.qedeq.kernel.bo.logic.wf.LogicalCheckExceptionList;
33    import org.qedeq.kernel.bo.logic.wf.Predicate;
34    import org.qedeq.kernel.bo.module.ControlVisitor;
35    import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
36    import org.qedeq.kernel.bo.module.KernelQedeqBo;
37    import org.qedeq.kernel.common.DefaultSourceFileExceptionList;
38    import org.qedeq.kernel.common.IllegalModuleDataException;
39    import org.qedeq.kernel.common.LogicalState;
40    import org.qedeq.kernel.common.ModuleDataException;
41    import org.qedeq.kernel.common.SourceFileExceptionList;
42   
43   
44    /**
45    * Checks if all formulas of a QEDEQ module are well formed.
46    *
47    * @version $Revision: 1.1 $
48    * @author Michael Meyling
49    */
 
50    public final class QedeqBoFormalLogicChecker extends ControlVisitor {
51   
52    /** This class. */
53    private static final Class CLASS = QedeqBoFormalLogicChecker.class;
54   
55    /** Existence checker for predicate and function constants. */
56    private ModuleConstantsExistenceChecker existence;
57   
58    /**
59    * Constructor.
60    *
61    * @param prop QEDEQ module properties object.
62    */
 
63  62 toggle private QedeqBoFormalLogicChecker(final KernelQedeqBo prop) {
64  62 super(prop);
65    }
66   
67    /**
68    * Checks if all formulas of a QEDEQ module are well formed.
69    *
70    * @param prop QEDEQ module properties object.
71    * @throws SourceFileExceptionList Major problem occurred.
72    */
 
73  113 toggle public static void check(final DefaultKernelQedeqBo prop)
74    throws SourceFileExceptionList {
75  113 if (prop.isChecked()) {
76  51 return;
77    }
78  62 if (!prop.hasLoadedRequiredModules()) {
79  0 throw new IllegalStateException("QEDEQ module has not loaded with required files: "
80    + prop);
81    }
82  62 prop.setLogicalProgressState(LogicalState.STATE_EXTERNAL_CHECKING);
83  62 KernelModuleReferenceList list = (KernelModuleReferenceList) prop.getRequiredModules();
84  98 for (int i = 0; i < list.size(); i++) {
85  36 try {
86  36 Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label",
87    list.getLabel(i));
88  36 check((DefaultKernelQedeqBo) list.getKernelQedeqBo(i));
89    } catch (SourceFileExceptionList e) { // TODO mime 20080114: hard coded codes
90  0 ModuleDataException md = new CheckRequiredModuleException(11231,
91    "import check failed: " + list.getQedeqBo(i).getModuleAddress(),
92    list.getModuleContext(i));
93  0 final SourceFileExceptionList sfl = prop.createSourceFileExceptionList(md);
94  0 prop.setLogicalFailureState(LogicalState.STATE_EXTERNAL_CHECKING_FAILED, sfl);
95  0 throw e;
96    }
97    }
98  62 prop.setLogicalProgressState(LogicalState.STATE_INTERNAL_CHECKING);
99  62 final QedeqBoFormalLogicChecker checker = new QedeqBoFormalLogicChecker(prop);
100  62 try {
101  62 checker.traverse();
102    } catch (SourceFileExceptionList sfl) {
103  11 prop.setLogicalFailureState(LogicalState.STATE_INTERNAL_CHECKING_FAILED, sfl);
104  11 throw sfl;
105    }
106  51 prop.setChecked(checker.existence);
107    }
108   
 
109  62 toggle protected void traverse() throws DefaultSourceFileExceptionList {
110  62 try {
111  62 this.existence = new ModuleConstantsExistenceChecker(getQedeqBo());
112    } catch (ModuleDataException me) {
113  0 addModuleDataException(me);
114  0 throw getSourceFileExceptionList();
115    }
116  62 super.traverse();
117    }
118   
 
119  175 toggle public void visitEnter(final Axiom axiom) throws ModuleDataException {
120  175 if (axiom == null) {
121  0 return;
122    }
123  175 final String context = getCurrentContext().getLocationWithinModule();
124  175 if (axiom.getFormula() != null) {
125  175 setLocationWithinModule(context + ".getFormula().getElement()");
126  175 final Formula formula = axiom.getFormula();
127  175 LogicalCheckExceptionList list =
128    FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), existence);
129  184 for (int i = 0; i < list.size(); i++) {
130  9 addModuleDataException(list.get(i));
131    }
132    }
133  175 setLocationWithinModule(context);
134  175 setBlocked(true);
135    }
136   
 
137  175 toggle public void visitLeave(final Axiom axiom) {
138  175 setBlocked(false);
139    }
140   
 
141  168 toggle public void visitEnter(final PredicateDefinition definition)
142    throws ModuleDataException {
143  168 if (definition == null) {
144  0 return;
145    }
146    // FIXME mime 20080324: check that no reference (also node references) with same name exist
147   
148  168 final String context = getCurrentContext().getLocationWithinModule();
149  168 final Predicate predicate = new Predicate(definition.getName(),
150    definition.getArgumentNumber());
151  168 if (existence.predicateExists(predicate)) {
152  0 throw new IllegalModuleDataException(HigherLogicalErrors.PREDICATE_ALREADY_DEFINED,
153    HigherLogicalErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicate,
154    getCurrentContext());
155    }
156  168 if ("2".equals(predicate.getArguments())
157    && ExistenceChecker.NAME_EQUAL.equals(predicate.getName())) {
158  17 existence.setIdentityOperatorDefined(true, predicate.getName());
159    }
160  168 if (definition.getFormula() != null) {
161  131 setLocationWithinModule(context + ".getFormula().getElement()");
162  131 final Formula formula = definition.getFormula();
163  131 LogicalCheckExceptionList list =
164    FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), existence);
165  131 for (int i = 0; i < list.size(); i++) {
166  0 addModuleDataException(list.get(i));
167    }
168    }
169  168 existence.add(definition);
170  168 setLocationWithinModule(context);
171  168 setBlocked(true);
172    }
173   
 
174  168 toggle public void visitLeave(final PredicateDefinition definition) {
175  168 setBlocked(false);
176    }
177   
 
178  96 toggle public void visitEnter(final FunctionDefinition definition)
179    throws ModuleDataException {
180  96 if (definition == null) {
181  0 return;
182    }
183    // TODO mime 20080324: check that no reference (also node references) with same name exist
184  96 final String context = getCurrentContext().getLocationWithinModule();
185  96 final Function function = new Function(definition.getName(),
186    definition.getArgumentNumber());
187  96 if (existence.functionExists(function)) {
188  0 throw new IllegalModuleDataException(HigherLogicalErrors.FUNCTION_ALREADY_DEFINED,
189    HigherLogicalErrors.FUNCTION_ALREADY_DEFINED_TEXT + function,
190    getCurrentContext());
191    }
192  96 if (definition.getTerm() != null) {
193  96 setLocationWithinModule(context + ".getTerm().getElement()");
194  96 final Term term = definition.getTerm();
195  96 LogicalCheckExceptionList list =
196    FormulaChecker.checkTerm(term.getElement(), getCurrentContext(), existence);
197  96 for (int i = 0; i < list.size(); i++) {
198  0 addModuleDataException(list.get(i));
199    }
200    }
201  96 existence.add(definition);
202  96 setLocationWithinModule(context);
203  96 setBlocked(true);
204    }
205   
 
206  96 toggle public void visitLeave(final FunctionDefinition definition) {
207  96 setBlocked(false);
208    }
209   
 
210  390 toggle public void visitEnter(final Proposition proposition)
211    throws ModuleDataException {
212  390 if (proposition == null) {
213  0 return;
214    }
215  390 final String context = getCurrentContext().getLocationWithinModule();
216  390 if (proposition.getFormula() != null) {
217  390 setLocationWithinModule(context + ".getFormula().getElement()");
218  390 final Formula formula = proposition.getFormula();
219  390 LogicalCheckExceptionList list =
220    FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), existence);
221  394 for (int i = 0; i < list.size(); i++) {
222  4 addModuleDataException(list.get(i));
223    }
224    }
225  390 setLocationWithinModule(context);
226  390 setBlocked(true);
227    }
228   
 
229  390 toggle public void visitLeave(final Proposition definition) {
230  390 setBlocked(false);
231    }
232   
 
233  114 toggle public void visitEnter(final Rule rule) throws ModuleDataException {
234  114 if (rule == null) {
235  0 return;
236    }
237  114 if (rule.getName() != null) {
238  114 if ("SET_DEFINION_BY_FORMULA".equals(rule.getName())) {
239    // LATER mime 20080114: check if this rule can be proposed
240  6 existence.setClassOperatorExists(true);
241    }
242    }
243  114 setBlocked(true);
244    }
245   
 
246  114 toggle public void visitLeave(final Rule rule) {
247  114 setBlocked(false);
248    }
249   
250    /**
251    * Set location information where are we within the original module.
252    *
253    * @param locationWithinModule Location within module.
254    */
 
255  1621 toggle public void setLocationWithinModule(final String locationWithinModule) {
256  1621 getCurrentContext().setLocationWithinModule(locationWithinModule);
257    }
258   
259    }