Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart10.png 0% of files have more coverage
245   637   87   14.41
104   426   0.36   17
17     5.12  
1    
 
  FormulaCheckerImpl       Line # 41 245 87 94.5% 0.9453552
 
  (69)
 
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.wf;
17   
18    import org.qedeq.base.trace.Trace;
19    import org.qedeq.kernel.bo.logic.common.ExistenceChecker;
20    import org.qedeq.kernel.bo.logic.common.FormulaChecker;
21    import org.qedeq.kernel.bo.logic.common.FormulaUtility;
22    import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
23    import org.qedeq.kernel.bo.logic.common.Operators;
24    import org.qedeq.kernel.se.base.list.Atom;
25    import org.qedeq.kernel.se.base.list.Element;
26    import org.qedeq.kernel.se.base.list.ElementList;
27    import org.qedeq.kernel.se.common.ModuleContext;
28    import org.qedeq.kernel.se.dto.list.ElementSet;
29   
30   
31    /**
32    * This class deals with {@link org.qedeq.kernel.se.base.list.Element}s which represent a
33    * formula. It has methods to check those elements for being well-formed.
34    *
35    * LATER mime 20070307: here are sometimes error messages that get concatenated with
36    * an {@link org.qedeq.kernel.se.base.list.ElementList#getOperator()} string. Perhaps these
37    * strings must be translated into the original input format and a mapping must be done.
38    *
39    * @author Michael Meyling
40    */
 
41    public class FormulaCheckerImpl implements Operators, FormulaBasicErrors, FormulaChecker {
42   
43    /** This class. */
44    private static final Class CLASS = FormulaCheckerImpl.class;
45   
46    /** Current context during creation. */
47    private ModuleContext currentContext;
48   
49    /** Existence checker for operators. */
50    private ExistenceChecker existenceChecker;
51   
52    /** All exceptions that occurred during checking. */
53    private LogicalCheckExceptionList exceptions;
54   
55   
56    /**
57    * Constructor.
58    *
59    */
 
60  18569 toggle public FormulaCheckerImpl() {
61    // nothing to do
62    }
63   
 
64  17325 toggle public final LogicalCheckExceptionList checkFormula(final Element element,
65    final ModuleContext context, final ExistenceChecker existenceChecker) {
66  17325 if (existenceChecker.identityOperatorExists()
67    && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
68  0 throw new IllegalArgumentException("identity predicate should exist, but it doesn't");
69    }
70  17325 this.existenceChecker = existenceChecker;
71  17325 currentContext = new ModuleContext(context);
72  17325 exceptions = new LogicalCheckExceptionList();
73  17325 checkFormula(element);
74  17325 return exceptions;
75    }
76   
 
77  177 toggle public final LogicalCheckExceptionList checkFormula(final Element element,
78    final ModuleContext context) {
79  177 return checkFormula(element, context, EverythingExists.getInstance());
80    }
81   
82    /**
83    * Check if {@link Element} is a term. If there are any errors the returned list
84    * (which is always not <code>null</code>) has a size greater zero.
85    *
86    * @param element Check this element.
87    * @param context For location information. Important for locating errors.
88    * @param existenceChecker Existence checker for operators.
89    * @return Collected errors if there are any. Not <code>null</code>.
90    */
 
91  1313 toggle public final LogicalCheckExceptionList checkTerm(final Element element,
92    final ModuleContext context, final ExistenceChecker existenceChecker) {
93  1313 if (existenceChecker.identityOperatorExists()
94    && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
95  0 throw new IllegalArgumentException("identity predicate should exist, but it doesn't");
96    }
97  1313 this.existenceChecker = existenceChecker;
98  1313 currentContext = new ModuleContext(context);
99  1313 exceptions = new LogicalCheckExceptionList();
100  1313 checkTerm(element);
101  1313 return exceptions;
102    }
103   
104    /**
105    * Check if {@link Element} is a term. If there are any errors the returned list
106    * (which is always not <code>null</code>) has a size greater zero.
107    * If the existence context is known you should use
108    * {@link #checkTerm(Element, ModuleContext, ExistenceChecker)}.
109    *
110    * @param element Check this element.
111    * @param context For location information. Important for locating errors.
112    * @return Collected errors if there are any. Not <code>null</code>.
113    */
 
114  21 toggle public final LogicalCheckExceptionList checkTerm(final Element element,
115    final ModuleContext context) {
116  21 return checkTerm(element, context, EverythingExists.getInstance());
117    }
118   
119    /**
120    * Is {@link Element} a formula?
121    *
122    * @param element Check this element.
123    */
 
124  141755 toggle private final void checkFormula(final Element element) {
125  141755 final String method = "checkFormula";
126  141755 Trace.begin(CLASS, this, method);
127  141755 Trace.param(CLASS, this, method, "element", element);
128  141755 final String context = getCurrentContext().getLocationWithinModule();
129  141755 Trace.param(CLASS, this, method, "context", context);
130  141755 if (!checkList(element)) {
131  7 return;
132    }
133  141748 final ElementList list = element.getList();
134  141748 final String listContext = context + ".getList()";
135  141748 setLocationWithinModule(listContext);
136  141748 final String operator = list.getOperator();
137  141748 if (operator.equals(CONJUNCTION_OPERATOR)
138    || operator.equals(DISJUNCTION_OPERATOR)
139    || operator.equals(IMPLICATION_OPERATOR)
140    || operator.equals(EQUIVALENCE_OPERATOR)) {
141  48679 Trace.trace(CLASS, this, method,
142    "one of (and, or, implication, equivalence) operator found");
143  48679 if (list.size() <= 1) {
144  9 handleFormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
145    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
146    + operator + "\"", element, getCurrentContext());
147  9 return;
148    }
149  48670 if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
150  1 handleFormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
151    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
152    + operator + "\"", element, getCurrentContext());
153  1 return;
154    }
155  153416 for (int i = 0; i < list.size(); i++) {
156  104747 setLocationWithinModule(listContext + ".getElement(" + i + ")");
157  104747 checkFormula(list.getElement(i));
158    }
159  48669 setLocationWithinModule(listContext);
160  48669 checkFreeAndBoundDisjunct(0, list);
161  93069 } else if (operator.equals(NEGATION_OPERATOR)) {
162  4259 Trace.trace(CLASS, this, method, "negation operator found");
163  4259 setLocationWithinModule(listContext);
164  4259 if (list.size() != 1) {
165  2 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
166    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
167    element, getCurrentContext());
168  2 return;
169    }
170  4257 setLocationWithinModule(listContext + ".getElement(0)");
171  4257 checkFormula(list.getElement(0));
172  88810 } else if (operator.equals(PREDICATE_VARIABLE)
173    || operator.equals(PREDICATE_CONSTANT)) {
174  76934 Trace.trace(CLASS, this, method, "predicate operator found");
175  76934 setLocationWithinModule(listContext);
176  76934 if (list.size() < 1) {
177  2 handleFormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
178    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
179    element, getCurrentContext());
180  2 return;
181    }
182    // check if first argument is an atom
183  76932 setLocationWithinModule(listContext + ".getElement(0)");
184  76932 if (!checkAtomFirst(list.getElement(0))) {
185  8 return;
186    }
187   
188    // check if rest arguments are terms
189  134432 for (int i = 1; i < list.size(); i++) {
190  57508 setLocationWithinModule(listContext + ".getElement(" + i + ")");
191  57508 checkTerm(list.getElement(i));
192    }
193   
194  76924 setLocationWithinModule(listContext);
195  76924 checkFreeAndBoundDisjunct(1, list);
196   
197    // check if predicate is known
198  76924 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
199    list.getElement(0).getAtom().getString(), list.size() - 1)) {
200  10 setLocationWithinModule(listContext + ".getElement(0)");
201  10 handleFormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
202    UNKNOWN_PREDICATE_CONSTANT_TEXT + "\""
203    + list.getElement(0).getAtom().getString() + "\" [" + (list.size() - 1) + "]",
204    element, getCurrentContext());
205    }
206   
207  11876 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
208    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
209    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
210  11870 Trace.trace(CLASS, this, method, "quantifier found");
211  11870 setLocationWithinModule(context);
212  11870 checkQuantifier(element);
213    } else {
214  6 setLocationWithinModule(listContext + ".getOperator()");
215  6 handleFormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
216    UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
217    element, getCurrentContext());
218    }
219    // restore context
220  141726 setLocationWithinModule(context);
221  141726 Trace.end(CLASS, this, method);
222    }
223   
224    /**
225    * Check quantifier element.
226    *
227    * @param element Check this element. Must be a quantifier element.
228    * @throws IllegalArgumentException <code>element.getList().getOperator()</code> is no
229    * quantifier operator.
230    */
 
231  11870 toggle private void checkQuantifier(final Element element) {
232  11870 final String method = "checkQuantifier";
233  11870 Trace.begin(CLASS, this, method);
234  11870 Trace.param(CLASS, this, method, "element", element);
235    // save context
236  11870 final String context = getCurrentContext().getLocationWithinModule();
237  11870 Trace.param(CLASS, this, method, "context", context);
238  11870 checkList(element);
239  11870 final ElementList list = element.getList();
240  11870 final String listContext = context + ".getList()";
241  11870 setLocationWithinModule(listContext);
242  11870 final String operator = list.getOperator();
243  11870 if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
244    && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
245    && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
246  0 throw new IllegalArgumentException("quantifier element expected but found: "
247    + element.toString());
248    }
249  11870 if (list.size() < 2 || list.size() > 3) {
250  0 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
251    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
252  0 return;
253    }
254   
255    // check if unique existential operator could be used
256  11870 if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
257    && !existenceChecker.identityOperatorExists()) {
258  0 setLocationWithinModule(listContext + ".getOperator()");
259  0 handleFormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
260    EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
261    }
262   
263    // check if first argument is subject variable
264  11870 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
265  11870 checkSubjectVariable(list.getElement(0));
266   
267    // check if second argument is a formula
268  11870 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
269  11870 checkFormula(list.getElement(1));
270   
271  11870 setLocationWithinModule(listContext);
272    // check if subject variable is not already bound in formula
273  11870 if (FormulaUtility.getBoundSubjectVariables(list.getElement(1)).contains(
274    list.getElement(0))) {
275  11 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
276    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
277    getCurrentContext());
278    }
279  11870 if (list.size() > 3) {
280  0 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
281    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
282    getCurrentContext());
283  0 return;
284    }
285  11870 if (list.size() > 2) {
286    // check if third argument is a formula
287  508 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
288  508 checkFormula(list.getElement(2));
289   
290    // check if subject variable is not bound in formula
291  508 setLocationWithinModule(listContext);
292  508 if (FormulaUtility.getBoundSubjectVariables(list.getElement(2)).contains(
293    list.getElement(0))) {
294  3 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
295    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
296    getCurrentContext());
297  3 return;
298    }
299  505 setLocationWithinModule(listContext);
300  505 checkFreeAndBoundDisjunct(1, list);
301    }
302    // restore context
303  11867 setLocationWithinModule(context);
304  11867 Trace.end(CLASS, this, method);
305    }
306   
307    /**
308    * Is {@link Element} a term?
309    *
310    * @param element Check this element.
311    */
 
312  80536 toggle private void checkTerm(final Element element) {
313  80536 final String method = "checkTerm";
314  80536 Trace.begin(CLASS, this, method);
315  80536 Trace.param(CLASS, this, method, "element", element);
316    // save current context
317  80536 final String context = getCurrentContext().getLocationWithinModule();
318  80536 Trace.param(CLASS, this, method, "context", context);
319  80536 if (!checkList(element)) {
320  4 return;
321    }
322  80532 final ElementList list = element.getList();
323  80532 final String listContext = context + ".getList()";
324  80532 setLocationWithinModule(listContext);
325  80532 final String operator = list.getOperator();
326  80532 if (operator.equals(SUBJECT_VARIABLE)) {
327  59333 checkSubjectVariable(element);
328  21199 } else if (operator.equals(FUNCTION_CONSTANT)
329    || operator.equals(FUNCTION_VARIABLE)) {
330   
331    // function constants must have at least a function name
332  18138 if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
333  1 handleTermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
334    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
335  1 return;
336    }
337   
338    // function variables must have at least a function name and at least one argument
339  18137 if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
340  2 handleTermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
341    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
342  2 return;
343    }
344   
345    // check if first argument is an atom
346  18135 setLocationWithinModule(listContext + ".getElement(0)");
347  18135 if (!checkAtomFirst(list.getElement(0))) {
348  7 return;
349    }
350   
351    // check if all arguments are terms
352  18128 setLocationWithinModule(listContext);
353  39843 for (int i = 1; i < list.size(); i++) {
354  21715 setLocationWithinModule(listContext + ".getElement(" + i + ")");
355  21715 checkTerm(list.getElement(i));
356    }
357   
358  18128 setLocationWithinModule(listContext);
359  18128 checkFreeAndBoundDisjunct(1, list);
360   
361    // check if function is known
362  18128 setLocationWithinModule(listContext);
363  18128 if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
364    list.getElement(0).getAtom().getString(), list.size() - 1)) {
365  2 handleFormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
366    UNKNOWN_FUNCTION_CONSTANT_TEXT + "\""
367    + list.getElement(0).getAtom().getString() + "\"", element,
368    getCurrentContext());
369    }
370   
371  3061 } else if (operator.equals(CLASS_OP)) {
372   
373  3050 if (list.size() != 2) {
374  2 handleTermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
375    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
376  2 return;
377    }
378    // check if first argument is a subject variable
379  3048 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
380  3048 if (!FormulaUtility.isSubjectVariable(list.getElement(0))) {
381  1 handleTermCheckException(SUBJECT_VARIABLE_EXPECTED,
382    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
383    }
384   
385    // check if the second argument is a formula
386  3048 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
387  3048 checkFormula(list.getElement(1));
388   
389    // check if class operator is allowed
390  3048 setLocationWithinModule(listContext);
391  3048 if (!existenceChecker.classOperatorExists()) {
392  2 handleFormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN,
393    CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext());
394    }
395   
396    // check if subject variable is not bound in formula
397  3048 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
398  3048 if (FormulaUtility.getBoundSubjectVariables(list.getElement(1)).contains(
399    list.getElement(0))) {
400  1 handleTermCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
401    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(0),
402    getCurrentContext());
403    }
404   
405    } else {
406  11 setLocationWithinModule(listContext + ".getOperator()");
407  11 handleTermCheckException(UNKNOWN_TERM_OPERATOR,
408    UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext());
409    }
410    // restore context
411  80520 setLocationWithinModule(context);
412  80520 Trace.end(CLASS, this, method);
413    }
414   
415    /**
416    * Check if no bound variables are free and vice versa.
417    * The current context must be at the list element.
418    *
419    * @param start Start check with this list position. Beginning with 0.
420    * @param list List element to check.
421    */
 
422  144226 toggle private void checkFreeAndBoundDisjunct(final int start,
423    final ElementList list) {
424    // save current context
425  144226 final String context = getCurrentContext().getLocationWithinModule();
426  144226 final ElementSet free = new ElementSet();
427  144226 final ElementSet bound = new ElementSet();
428  329206 for (int i = start; i < list.size(); i++) {
429  184980 setLocationWithinModule(context + ".getElement(" + i + ")");
430  184980 final ElementSet newFree
431    = FormulaUtility.getFreeSubjectVariables(list.getElement(i));
432  184980 final ElementSet newBound
433    = FormulaUtility.getBoundSubjectVariables(list.getElement(i));
434  184980 final ElementSet interBound = newFree.newIntersection(bound);
435  184980 if (!interBound.isEmpty()) {
436  21 handleFormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
437    FREE_VARIABLE_ALREADY_BOUND_TEXT
438    + interBound, list.getElement(i), getCurrentContext());
439    }
440  184980 final ElementSet interFree = newBound.newIntersection(free);
441  184980 if (!interFree.isEmpty()) {
442  17 handleFormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
443    BOUND_VARIABLE_ALREADY_FREE_TEXT
444    + interFree, list.getElement(i), getCurrentContext());
445    }
446  184980 bound.union(newBound);
447  184980 free.union(newFree);
448    }
449    // restore context
450  144226 setLocationWithinModule(context);
451    }
452   
453    /**
454    * Check if {@link Element} is a subject variable.
455    *
456    * @param element Check this element.
457    * @return Is it a subject variable?
458    */
 
459  71203 toggle private boolean checkSubjectVariable(final Element element) {
460    // throws LogicalCheckException {
461    // save current context
462  71203 final String context = getCurrentContext().getLocationWithinModule();
463  71203 if (!checkList(element)) {
464  0 return false;
465    }
466  71203 setLocationWithinModule(context + ".getList()");
467  71203 if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
468  71200 if (element.getList().size() != 1) {
469  2 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
470    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext());
471  2 return false;
472    }
473    // check if first argument is an atom
474  71198 setLocationWithinModule(context + ".getList().getElement(0)");
475  71198 if (checkAtomFirst(element.getList().getElement(0))) {
476  71197 return false;
477    }
478    } else {
479  3 setLocationWithinModule(context + ".getList().getOperator()");
480  3 handleFormulaCheckException(SUBJECT_VARIABLE_EXPECTED,
481    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
482  3 return false;
483    }
484    // restore context
485  1 setLocationWithinModule(context);
486  1 return true;
487    }
488   
489    /**
490    * Check common requirements for list elements that are checked for being a term or formula.
491    * That includes: is the element a true list, has the operator a non zero size.
492    *
493    * @param element List element.
494    * @return Are the requirements fulfilled?
495    */
 
496  305364 toggle private boolean checkList(final Element element) {
497    // save current context
498  305364 final String context = getCurrentContext().getLocationWithinModule();
499  305364 if (element == null) {
500  2 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
501    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
502  2 return false;
503    }
504  305362 if (!element.isList()) {
505  2 handleElementCheckException(LIST_EXPECTED,
506    LIST_EXPECTED_TEXT, element, getCurrentContext());
507  2 return false;
508    }
509  305360 final ElementList list = element.getList();
510  305360 setLocationWithinModule(context + ".getList()");
511  305360 if (list == null) {
512  2 handleElementCheckException(LIST_MUST_NOT_BE_NULL,
513    LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
514  2 return false;
515    }
516  305358 final String operator = list.getOperator();
517  305358 setLocationWithinModule(context + ".getList().getOperator()");
518  305358 if (operator == null) {
519  2 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL,
520    OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT , element,
521    getCurrentContext());
522  2 return false;
523    }
524  305356 if (operator.length() == 0) {
525  3 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY,
526    OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\""
527    + operator + "\"", element, getCurrentContext());
528  3 return false;
529    }
530    // restore context
531  305353 setLocationWithinModule(context);
532  305353 return true;
533    }
534   
535    /**
536    * Check if element is an atom and has valid content. It is assumed, that this element is the
537    * first of a list.
538    *
539    * @param element Check this for an atom.
540    * @return Is the content valid?
541    */
 
542  166265 toggle private boolean checkAtomFirst(final Element element) {
543    // save current context
544  166265 final String context = getCurrentContext().getLocationWithinModule();
545  166265 if (element == null) {
546  0 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
547    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
548  0 return false;
549    }
550  166265 if (!element.isAtom()) { // TODO mime 20061126: this is special?
551  9 handleElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM,
552    FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext());
553  9 return false;
554    }
555  166256 final Atom atom = element.getAtom();
556  166256 setLocationWithinModule(context + ".getAtom()");
557  166256 if (atom == null) {
558  2 handleElementCheckException(ATOM_MUST_NOT_BE_NULL,
559    ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
560  2 return false;
561    }
562  166254 if (atom.getString() == null) {
563  2 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL,
564    ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
565  2 return false;
566    }
567  166252 if (atom.getString().length() == 0) {
568  3 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY,
569    ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext());
570  3 return false;
571    }
572    // restore context
573  166249 setLocationWithinModule(context);
574  166249 return true;
575    }
576   
577    /**
578    * Add new {@link FormulaCheckException} to exception list.
579    *
580    * @param code Error code.
581    * @param msg Error message.
582    * @param element Element with error.
583    * @param context Error context.
584    */
 
585  91 toggle private void handleFormulaCheckException(final int code, final String msg,
586    final Element element, final ModuleContext context) {
587  91 final FormulaCheckException ex = new FormulaCheckException(code, msg, element, context);
588  91 exceptions.add(ex);
589    }
590   
591    /**
592    * Add new {@link TermCheckException} to exception list.
593    *
594    * @param code Error code.
595    * @param msg Error message.
596    * @param element Element with error.
597    * @param context Error context.
598    */
 
599  18 toggle private void handleTermCheckException(final int code, final String msg,
600    final Element element, final ModuleContext context) {
601  18 final TermCheckException ex = new TermCheckException(code, msg, element, context);
602  18 exceptions.add(ex);
603    }
604   
605    /**
606    * Add new {@link ElementCheckException} to exception list.
607    *
608    * @param code Error code.
609    * @param msg Error message.
610    * @param element Element with error.
611    * @param context Error context.
612    */
 
613  27 toggle private void handleElementCheckException(final int code, final String msg,
614    final Element element, final ModuleContext context) {
615  27 final ElementCheckException ex = new ElementCheckException(code, msg, element, context);
616  27 exceptions.add(ex);
617    }
618   
619    /**
620    * Set location information where are we within the original module.
621    *
622    * @param locationWithinModule Location within module.
623    */
 
624  2752621 toggle protected void setLocationWithinModule(final String locationWithinModule) {
625  2752621 getCurrentContext().setLocationWithinModule(locationWithinModule);
626    }
627   
628    /**
629    * Get current context within original.
630    *
631    * @return Current context.
632    */
 
633  3798515 toggle protected final ModuleContext getCurrentContext() {
634  3798515 return currentContext;
635    }
636   
637    }
 
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 .