Clover Coverage Report
Coverage timestamp: Sa Aug 2 2008 13:56:27 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../img/srcFileCovDistChart10.png 0% of files have more coverage
279   769   114   13,95
130   492   0,41   20
20     5,7  
1    
 
  FormulaChecker       Line # 47 279 114 94,4% 0.9440559
 
  (19)
 
1    /* $Id: FormulaChecker.java,v 1.1 2008/07/26 07:58:30 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.logic;
19   
20    import org.qedeq.base.trace.Trace;
21    import org.qedeq.kernel.base.list.Atom;
22    import org.qedeq.kernel.base.list.Element;
23    import org.qedeq.kernel.base.list.ElementList;
24    import org.qedeq.kernel.bo.logic.wf.ElementCheckException;
25    import org.qedeq.kernel.bo.logic.wf.EverythingExists;
26    import org.qedeq.kernel.bo.logic.wf.ExistenceChecker;
27    import org.qedeq.kernel.bo.logic.wf.FormulaBasicErrors;
28    import org.qedeq.kernel.bo.logic.wf.FormulaCheckException;
29    import org.qedeq.kernel.bo.logic.wf.LogicalCheckExceptionList;
30    import org.qedeq.kernel.bo.logic.wf.Operators;
31    import org.qedeq.kernel.bo.logic.wf.TermCheckException;
32    import org.qedeq.kernel.common.ModuleContext;
33    import org.qedeq.kernel.dto.list.ElementSet;
34   
35   
36    /**
37    * This class deals with {@link org.qedeq.kernel.base.list.Element}s which represent a
38    * formula. It has methods to check those elements for being well-formed.
39    *
40    * LATER mime 20070307: here are sometimes error messages that get concatenated with
41    * an {@link org.qedeq.kernel.base.list.ElementList#getOperator()} string. Perhaps these
42    * strings must be translated into the original input format and a mapping must be done.
43    *
44    * @version $Revision: 1.1 $
45    * @author Michael Meyling
46    */
 
47    public final class FormulaChecker implements Operators, FormulaBasicErrors {
48   
49    // TODO mime 20080404: we should do that within a JUnit test!
50    // If you want to check if the context information within this class is correct you have to
51    // do the following:
52    // 1. add "private Qedeq qedeq;" as a new field of this class
53    // 2. add DynamicGetter from test project into this package
54    // 3. modify {@link #setLocationWithinModule(String) by calling
55    // DynamicGetter.get(qedeq, getCurrentContext().getLocationWithinModule());
56    // 4. modify the {@link #checkFormula(Element, ModuleContext, ExistenceChecker} by adding
57    // a Qedeq parameter;
58    // 5. modify {@link #checkTerm(Element, ModuleContext, ExistenceChecker) analogous
59   
60    /** This class. */
61    private static final Class CLASS = FormulaChecker.class;
62   
63    /** Current context during creation. */
64    private final ModuleContext currentContext;
65   
66    /** Existence checker for operators. */
67    private final ExistenceChecker existenceChecker;
68   
69    /** All exceptions that occurred during checking. */
70    private final LogicalCheckExceptionList exceptions;
71   
72   
73    /**
74    * Constructor.
75    *
76    * @param context For location information. Important for locating errors.
77    * @param existenceChecker Existence checker for operators.
78    * @throws IllegalArgumentException The <code>existenceChecker</code> says the equality
79    * operator exists but the predicate is not found. This should be a programming
80    * error.
81    */
 
82  1018 toggle private FormulaChecker(final ModuleContext context,
83    final ExistenceChecker existenceChecker) {
84  1018 this.existenceChecker = existenceChecker;
85  1018 if (existenceChecker.equalityOperatorExists()
86    && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
87  0 throw new IllegalArgumentException("equality predicate should exist, but it doesn't");
88    }
89  1018 currentContext = new ModuleContext(context);
90  1018 exceptions = new LogicalCheckExceptionList();
91    }
92   
93    /**
94    * Checks if an {@link Element} is a formula. If there are any errors the returned list
95    * (which is always not <code>null</code>) has a size greater zero.
96    *
97    * @param element Check this element.
98    * @param context For location information. Important for locating errors.
99    * @param existenceChecker Existence checker for operators.
100    * @return Collected errors if there are any. Not <code>null</code>.
101    */
 
102  859 toggle public static final LogicalCheckExceptionList checkFormula(final Element element,
103    final ModuleContext context, final ExistenceChecker existenceChecker) {
104  859 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
105  859 checker.checkFormula(element);
106  859 return checker.exceptions;
107    }
108   
109    /**
110    * Checks if an {@link Element} is a formula. All predicates and functions are assumed to exit.
111    * If there are any errors the returned list (which is always not <code>null</code>) has a size
112    * greater zero.
113    * If the existence context is known you should use
114    * {@link #checkFormula(Element, ModuleContext, ExistenceChecker)}.
115    *
116    * @param element Check this element.
117    * @param context For location information. Important for locating errors.
118    * @return Collected errors if there are any. Not <code>null</code>.
119    */
 
120  51 toggle public static final LogicalCheckExceptionList checkFormula(final Element element,
121    final ModuleContext context) {
122  51 return checkFormula(element, context, EverythingExists.getInstance());
123    }
124   
125    /**
126    * Check if {@link Element} is a term. If there are any errors the returned list
127    * (which is always not <code>null</code>) has a size greater zero.
128    *
129    * @param element Check this element.
130    * @param context For location information. Important for locating errors.
131    * @param existenceChecker Existence checker for operators.
132    * @return Collected errors if there are any. Not <code>null</code>.
133    */
 
134  159 toggle public static final LogicalCheckExceptionList checkTerm(final Element element,
135    final ModuleContext context, final ExistenceChecker existenceChecker) {
136  159 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
137  159 checker.checkTerm(element);
138  159 return checker.exceptions;
139    }
140   
141    /**
142    * Check if {@link Element} is a term. If there are any errors the returned list
143    * (which is always not <code>null</code>) has a size greater zero.
144    * If the existence context is known you should use
145    * {@link #checkTerm(Element, ModuleContext, ExistenceChecker)}.
146    *
147    * @param element Check this element.
148    * @param context For location information. Important for locating errors.
149    * @return Collected errors if there are any. Not <code>null</code>.
150    */
 
151  21 toggle public static final LogicalCheckExceptionList checkTerm(final Element element,
152    final ModuleContext context) {
153  21 return checkTerm(element, context, EverythingExists.getInstance());
154    }
155   
156    /**
157    * Is {@link Element} a formula?
158    *
159    * @param element Check this element.
160    */
 
161  8694 toggle private final void checkFormula(final Element element) {
162  8694 final String method = "checkFormula";
163  8694 Trace.begin(CLASS, this, method);
164  8694 Trace.param(CLASS, this, method, "element", element);
165  8694 final String context = getCurrentContext().getLocationWithinModule();
166  8694 Trace.param(CLASS, this, method, "context", context);
167  8694 if (!checkList(element)) {
168  7 return;
169    }
170  8687 final ElementList list = element.getList();
171  8687 final String listContext = context + ".getList()";
172  8687 setLocationWithinModule(listContext);
173  8687 final String operator = list.getOperator();
174  8687 if (operator.equals(CONJUNCTION_OPERATOR)
175    || operator.equals(DISJUNCTION_OPERATOR)
176    || operator.equals(IMPLICATION_OPERATOR)
177    || operator.equals(EQUIVALENCE_OPERATOR)) {
178  2807 Trace.trace(CLASS, this, method,
179    "one of (and, or, implication, equivalence) operator found");
180  2807 if (list.size() <= 1) {
181  9 handleFormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
182    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
183    + operator + "\"", element, getCurrentContext());
184  9 return;
185    }
186  2798 if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
187  1 handleFormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
188    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
189    + operator + "\"", element, getCurrentContext());
190  1 return;
191    }
192  9123 for (int i = 0; i < list.size(); i++) {
193  6326 setLocationWithinModule(listContext + ".getElement(" + i + ")");
194  6326 checkFormula(list.getElement(i));
195    }
196  2797 setLocationWithinModule(listContext);
197  2797 checkFreeAndBoundDisjunct(0, list);
198  5880 } else if (operator.equals(NEGATION_OPERATOR)) {
199  299 Trace.trace(CLASS, this, method, "negation operator found");
200  299 setLocationWithinModule(listContext);
201  299 if (list.size() != 1) {
202  2 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
203    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
204    element, getCurrentContext());
205  2 return;
206    }
207  297 setLocationWithinModule(listContext + ".getElement(0)");
208  297 checkFormula(list.getElement(0));
209  5581 } else if (operator.equals(PREDICATE_VARIABLE)
210    || operator.equals(PREDICATE_CONSTANT)) {
211  4677 Trace.trace(CLASS, this, method, "predicate operator found");
212  4677 setLocationWithinModule(listContext);
213  4677 if (list.size() < 1) {
214  2 handleFormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
215    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
216    element, getCurrentContext());
217  2 return;
218    }
219    // check if first argument is an atom
220  4675 setLocationWithinModule(listContext + ".getElement(0)");
221  4675 if (!checkAtomFirst(list.getElement(0))) {
222  8 return;
223    }
224   
225    // check if rest arguments are terms
226  9279 for (int i = 1; i < list.size(); i++) {
227  4612 setLocationWithinModule(listContext + ".getElement(" + i + ")");
228  4612 checkTerm(list.getElement(i));
229    }
230   
231  4667 setLocationWithinModule(listContext);
232  4667 checkFreeAndBoundDisjunct(1, list);
233   
234    // check if predicate is known
235  4667 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
236    list.getElement(0).getAtom().getString(), list.size() - 1)) {
237  8 handleFormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
238    UNKNOWN_PREDICATE_CONSTANT_TEXT + "\""
239    + list.getElement(0).getAtom().getString() + "\" [" + (list.size() - 1) + "]",
240    element, getCurrentContext());
241    }
242   
243  904 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
244    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
245    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
246  898 Trace.trace(CLASS, this, method, "quantifier found");
247  898 setLocationWithinModule(context);
248  898 checkQuantifier(element);
249    } else {
250  6 setLocationWithinModule(listContext + ".getOperator()");
251  6 handleFormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
252    UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
253    element, getCurrentContext());
254    }
255    // restore context
256  8665 setLocationWithinModule(context);
257  8665 Trace.end(CLASS, this, method);
258    }
259   
260    /**
261    * Check quantifier element.
262    *
263    * @param element Check this element. Must be a quantifier element.
264    * @throws IllegalArgumentException <code>element.getList().getOperator()</code> is no
265    * quantifier operator.
266    */
 
267  898 toggle private void checkQuantifier(final Element element) {
268  898 final String method = "checkQuantifier";
269  898 Trace.begin(CLASS, this, method);
270  898 Trace.param(CLASS, this, method, "element", element);
271    // save context
272  898 final String context = getCurrentContext().getLocationWithinModule();
273  898 Trace.param(CLASS, this, method, "context", context);
274  898 checkList(element);
275  898 final ElementList list = element.getList();
276  898 final String listContext = context + ".getList()";
277  898 setLocationWithinModule(listContext);
278  898 final String operator = list.getOperator();
279  898 if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
280    && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
281    && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
282  0 throw new IllegalArgumentException("quantifier element expected but found: "
283    + element.toString());
284    }
285  898 if (list.size() < 2 || list.size() > 3) {
286  0 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
287    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
288  0 return;
289    }
290   
291    // check if unique existential operator could be used
292  898 if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
293    && !existenceChecker.equalityOperatorExists()) {
294  0 setLocationWithinModule(listContext + ".getOperator()");
295  0 handleFormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
296    EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
297    }
298   
299    // check if first argument is subject variable
300  898 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
301  898 checkSubjectVariable(list.getElement(0));
302   
303    // check if second argument is a formula
304  898 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
305  898 checkFormula(list.getElement(1));
306   
307  898 setLocationWithinModule(listContext);
308    // check if subject variable is not already bound in formula
309  898 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
310    list.getElement(0))) {
311  10 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
312    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
313    getCurrentContext());
314    }
315  898 if (list.size() > 3) {
316  0 handleFormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
317    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
318    getCurrentContext());
319  0 return;
320    }
321  898 if (list.size() > 2) {
322    // check if third argument is a formula
323  72 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
324  72 checkFormula(list.getElement(2));
325   
326    // check if subject variable is not bound in formula
327  72 setLocationWithinModule(listContext);
328  72 if (FormulaChecker.getBoundSubjectVariables(list.getElement(2)).contains(
329    list.getElement(0))) {
330  3 handleFormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
331    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
332    getCurrentContext());
333  3 return;
334    }
335  69 setLocationWithinModule(listContext);
336  69 checkFreeAndBoundDisjunct(1, list);
337    }
338    // restore context
339  895 setLocationWithinModule(context);
340  895 Trace.end(CLASS, this, method);
341    }
342   
343    /**
344    * Is {@link Element} a term?
345    *
346    * @param element Check this element.
347    */
 
348  6521 toggle private void checkTerm(final Element element) {
349  6521 final String method = "checkTerm";
350  6521 Trace.begin(CLASS, this, method);
351  6521 Trace.param(CLASS, this, method, "element", element);
352    // save current context
353  6521 final String context = getCurrentContext().getLocationWithinModule();
354  6521 Trace.param(CLASS, this, method, "context", context);
355  6521 if (!checkList(element)) {
356  4 return;
357    }
358  6517 final ElementList list = element.getList();
359  6517 final String listContext = context + ".getList()";
360  6517 setLocationWithinModule(listContext);
361  6517 final String operator = list.getOperator();
362  6517 if (operator.equals(SUBJECT_VARIABLE)) {
363  4768 checkSubjectVariable(element);
364  1749 } else if (operator.equals(FUNCTION_CONSTANT)
365    || operator.equals(FUNCTION_VARIABLE)) {
366   
367    // function constants must have at least a function name
368  1494 if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
369  1 handleTermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
370    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
371  1 return;
372    }
373   
374    // function variables must have at least a function name and at least one argument
375  1493 if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
376  2 handleTermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
377    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
378  2 return;
379    }
380   
381    // check if first argument is an atom
382  1491 setLocationWithinModule(listContext + ".getElement(0)");
383  1491 if (!checkAtomFirst(list.getElement(0))) {
384  7 return;
385    }
386   
387    // check if all arguments are terms
388  1484 setLocationWithinModule(listContext);
389  3234 for (int i = 1; i < list.size(); i++) {
390  1750 setLocationWithinModule(listContext + ".getElement(" + i + ")");
391  1750 checkTerm(list.getElement(i));
392    }
393   
394  1484 setLocationWithinModule(listContext);
395  1484 checkFreeAndBoundDisjunct(1, list);
396   
397    // check if function is known
398  1484 setLocationWithinModule(listContext);
399  1484 if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
400    list.getElement(0).getAtom().getString(), list.size() - 1)) {
401  2 handleFormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
402    UNKNOWN_FUNCTION_CONSTANT_TEXT + "\""
403    + list.getElement(0).getAtom().getString() + "\"", element,
404    getCurrentContext());
405    }
406   
407  255 } else if (operator.equals(CLASS_OP)) {
408   
409  244 if (list.size() != 2) {
410  2 handleTermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
411    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
412  2 return;
413    }
414    // check if first argument is a subject variable
415  242 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
416  242 if (!isSubjectVariable(list.getElement(0))) {
417  1 handleTermCheckException(SUBJECT_VARIABLE_EXPECTED,
418    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
419    }
420   
421    // check if the second argument is a formula
422  242 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
423  242 checkFormula(list.getElement(1));
424   
425    // check if class operator is allowed
426  242 setLocationWithinModule(listContext);
427  242 if (!existenceChecker.classOperatorExists()) {
428  2 handleFormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN,
429    CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext());
430    }
431   
432    // check if subject variable is not bound in formula
433  242 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
434  242 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
435    list.getElement(0))) {
436  1 handleTermCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
437    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(0),
438    getCurrentContext());
439    }
440   
441    } else {
442  11 setLocationWithinModule(listContext + ".getOperator()");
443  11 handleTermCheckException(UNKNOWN_TERM_OPERATOR,
444    UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext());
445    }
446    // restore context
447  6505 setLocationWithinModule(context);
448  6505 Trace.end(CLASS, this, method);
449    }
450   
451    /**
452    * Check if no bound variables are free and vice versa.
453    * The current context must be at the list element.
454    *
455    * @param start Start check with this list position. Beginning with 0.
456    * @param list List element to check.
457    */
 
458  9017 toggle private void checkFreeAndBoundDisjunct(final int start,
459    final ElementList list) {
460    // save current context
461  9017 final String context = getCurrentContext().getLocationWithinModule();
462  9017 final ElementSet free = new ElementSet();
463  9017 final ElementSet bound = new ElementSet();
464  21843 for (int i = start; i < list.size(); i++) {
465  12826 setLocationWithinModule(context + ".getElement(" + i + ")");
466  12826 final ElementSet newFree
467    = getFreeSubjectVariables(list.getElement(i));
468  12826 final ElementSet newBound
469    = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
470  12826 final ElementSet interBound = newFree.newIntersection(bound);
471  12826 if (!interBound.isEmpty()) {
472  20 handleFormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
473    FREE_VARIABLE_ALREADY_BOUND_TEXT
474    + interBound, list.getElement(i), getCurrentContext());
475    }
476  12826 final ElementSet interFree = newBound.newIntersection(free);
477  12826 if (!interFree.isEmpty()) {
478  16 handleFormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
479    BOUND_VARIABLE_ALREADY_FREE_TEXT
480    + interFree, list.getElement(i), getCurrentContext());
481    }
482  12826 bound.union(newBound);
483  12826 free.union(newFree);
484    }
485    // restore context
486  9017 setLocationWithinModule(context);
487    }
488   
489   
490    /**
491    * Is {@link Element} a subject variable?
492    *
493    * @param element Element to look onto.
494    * @return Is it a subject variable?
495    */
 
496  48888 toggle private final boolean isSubjectVariable(final Element element) {
497  48888 if (element == null || !element.isList() || element.getList() == null) {
498  13964 return false;
499    }
500  34924 final ElementList list = element.getList();
501  34924 if (list.getOperator().equals(SUBJECT_VARIABLE)) {
502  15155 if (list.size() != 1) {
503  0 return false;
504    }
505  15155 final Element first = element.getList().getElement(0);
506  15155 if (first == null || !first.isAtom() || first.getAtom() == null) {
507  0 return false;
508    }
509  15155 final Atom atom = first.getAtom();
510  15155 if (atom.getString() == null || atom.getAtom().getString() == null
511    || atom.getString().length() == 0) {
512  0 return false;
513    }
514    } else {
515  19769 return false;
516    }
517  15155 return true;
518    }
519   
520   
521    /**
522    * Check if {@link Element} is a subject variable.
523    *
524    * @param element Check this element.
525    * @return Is it a subject variable?
526    */
 
527  5666 toggle private boolean checkSubjectVariable(final Element element) {
528    // throws LogicalCheckException {
529    // save current context
530  5666 final String context = getCurrentContext().getLocationWithinModule();
531  5666 if (!checkList(element)) {
532  0 return false;
533    }
534  5666 setLocationWithinModule(context + ".getList()");
535  5666 if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
536  5663 if (element.getList().size() != 1) {
537  2 handleFormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
538    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext());
539  2 return false;
540    }
541    // check if first argument is an atom
542  5661 setLocationWithinModule(context + ".getList().getElement(0)");
543  5661 if (checkAtomFirst(element.getList().getElement(0))) {
544  5660 return false;
545    }
546    } else {
547  3 setLocationWithinModule(context + ".getList().getOperator()");
548  3 handleFormulaCheckException(SUBJECT_VARIABLE_EXPECTED,
549    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
550  3 return false;
551    }
552    // restore context
553  1 setLocationWithinModule(context);
554  1 return true;
555    }
556   
557   
558    /**
559    * Return all free subject variables of an element.
560    *
561    * @param element Work on this element.
562    * @return All free subject variables.
563    */
 
564  48646 toggle private final ElementSet getFreeSubjectVariables(final Element element) {
565  48646 final ElementSet free = new ElementSet();
566  48646 if (isSubjectVariable(element)) {
567  14914 free.add(element);
568  33732 } else if (element.isList()) {
569  19768 final ElementList list = element.getList();
570  19768 final String operator = list.getOperator();
571  19768 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
572    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
573    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
574    || operator.equals(CLASS_OP)) {
575  3572 for (int i = 1; i < list.size(); i++) {
576  1810 free.union(getFreeSubjectVariables(list.getElement(i)));
577    }
578  1762 free.remove(list.getElement(0));
579    } else {
580  52016 for (int i = 0; i < list.size(); i++) {
581  34010 free.union(getFreeSubjectVariables(list.getElement(i)));
582    }
583    }
584    }
585  48646 return free;
586    }
587   
588    /**
589    * Return all bound subject variables of an element.
590    *
591    * @param element Work on this element.
592    * @return All bound subject variables.
593    */
 
594  74063 toggle public static final ElementSet getBoundSubjectVariables(final Element element) {
595  74063 final ElementSet bound = new ElementSet();
596  74063 if (element.isList()) {
597  40372 ElementList list = element.getList();
598  40372 final String operator = list.getOperator();
599    // if operator is quantifier or class term
600  40372 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
601    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
602    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
603    || operator.equals(CLASS_OP)) {
604    // add subject variable to bound list
605  2032 bound.add(list.getElement(0));
606    // add all bound variables of sub-elements
607  4128 for (int i = 1; i < list.size(); i++) {
608  2096 bound.union(FormulaChecker.getBoundSubjectVariables(
609    list.getElement(i)));
610    }
611    } else {
612    // add all bound variables of sub-elements
613  96269 for (int i = 0; i < list.size(); i++) {
614  57929 bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i)));
615    }
616    }
617    }
618  74063 return bound;
619    }
620   
621    /**
622    * Check common requirements for list elements that are checked for being a term or formula.
623    * That includes: is the element a true list, has the operator a non zero size.
624    *
625    * @param element List element.
626    * @return Are the requirements fulfilled?
627    */
 
628  21779 toggle private boolean checkList(final Element element) {
629    // save current context
630  21779 final String context = getCurrentContext().getLocationWithinModule();
631  21779 if (element == null) {
632  2 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
633    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
634  2 return false;
635    }
636  21777 if (!element.isList()) {
637  2 handleElementCheckException(LIST_EXPECTED,
638    LIST_EXPECTED_TEXT, element, getCurrentContext());
639  2 return false;
640    }
641  21775 final ElementList list = element.getList();
642  21775 setLocationWithinModule(context + ".getList()");
643  21775 if (list == null) {
644  2 handleElementCheckException(LIST_MUST_NOT_BE_NULL,
645    LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
646  2 return false;
647    }
648  21773 final String operator = list.getOperator();
649  21773 setLocationWithinModule(context + ".getList().getOperator()");
650  21773 if (operator == null) {
651  2 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL,
652    OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT + "\""
653    + operator + "\"", element, getCurrentContext());
654  2 return false;
655    }
656  21771 if (operator.length() == 0) {
657  3 handleElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY,
658    OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\""
659    + operator + "\"", element, getCurrentContext());
660  3 return false;
661    }
662    // restore context
663  21768 setLocationWithinModule(context);
664  21768 return true;
665    }
666   
667    /**
668    * Check if element is an atom and has valid content. It is assumed, that this element is the
669    * first of a list.
670    *
671    * @param element Check this for an atom.
672    * @return Is the content valid?
673    */
 
674  11827 toggle private boolean checkAtomFirst(final Element element) {
675    // save current context
676  11827 final String context = getCurrentContext().getLocationWithinModule();
677  11827 if (element == null) {
678  0 handleElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
679    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
680  0 return false;
681    }
682  11827 if (!element.isAtom()) { // TODO mime 20061126: this is special?
683  9 handleElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM,
684    FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext());
685  9 return false;
686    }
687  11818 final Atom atom = element.getAtom();
688  11818 setLocationWithinModule(context + ".getAtom()");
689  11818 if (atom == null) {
690  2 handleElementCheckException(ATOM_MUST_NOT_BE_NULL,
691    ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
692  2 return false;
693    }
694  11816 if (atom.getString() == null) {
695  2 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL,
696    ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
697  2 return false;
698    }
699  11814 if (atom.getString().length() == 0) {
700  3 handleElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY,
701    ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext());
702  3 return false;
703    }
704    // restore context
705  11811 setLocationWithinModule(context);
706  11811 return true;
707    }
708   
709    /**
710    * Add new {@link FormulaCheckException} to exception list.
711    *
712    * @param code Error code.
713    * @param msg Error message.
714    * @param element Element with error.
715    * @param context Error context.
716    */
 
717  86 toggle private void handleFormulaCheckException(final int code, final String msg,
718    final Element element, final ModuleContext context) {
719  86 final FormulaCheckException ex = new FormulaCheckException(code, msg, element, context);
720  86 exceptions.add(ex);
721    }
722   
723    /**
724    * Add new {@link TermCheckException} to exception list.
725    *
726    * @param code Error code.
727    * @param msg Error message.
728    * @param element Element with error.
729    * @param context Error context.
730    */
 
731  18 toggle private void handleTermCheckException(final int code, final String msg,
732    final Element element, final ModuleContext context) {
733  18 final TermCheckException ex = new TermCheckException(code, msg, element, context);
734  18 exceptions.add(ex);
735    }
736   
737    /**
738    * Add new {@link ElementCheckException} to exception list.
739    *
740    * @param code Error code.
741    * @param msg Error message.
742    * @param element Element with error.
743    * @param context Error context.
744    */
 
745  27 toggle private void handleElementCheckException(final int code, final String msg,
746    final Element element, final ModuleContext context) {
747  27 final ElementCheckException ex = new ElementCheckException(code, msg, element, context);
748  27 exceptions.add(ex);
749    }
750   
751    /**
752    * Set location information where are we within the original module.
753    *
754    * @param locationWithinModule Location within module.
755    */
 
756  195119 toggle protected void setLocationWithinModule(final String locationWithinModule) {
757  195119 getCurrentContext().setLocationWithinModule(locationWithinModule);
758    }
759   
760    /**
761    * Get current context within original.
762    *
763    * @return Current context.
764    */
 
765  259652 toggle protected final ModuleContext getCurrentContext() {
766  259652 return currentContext;
767    }
768   
769    }
 
CloverReport generated by Clover Code Coverage v2.3.1
Sa Aug 2 2008 13:56:32 CEST.		   Clover: Open Source License registered to qedeq.org .