Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: So Feb 25 2007 22:22:30 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 666   Methods: 17
NCLOC: 431   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
FormulaChecker.java 92,5% 95,9% 100% 95%
coverage coverage
 1    /* $Id: FormulaChecker.java,v 1.6 2007/02/25 20:05:35 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2007, 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.kernel.base.list.Atom;
 21    import org.qedeq.kernel.base.list.Element;
 22    import org.qedeq.kernel.base.list.ElementList;
 23    import org.qedeq.kernel.context.ModuleContext;
 24    import org.qedeq.kernel.dto.list.ElementSet;
 25    import org.qedeq.kernel.log.Trace;
 26   
 27   
 28    /**
 29    * This class deals with {@link org.qedeq.kernel.base.list.Element}s which represent a
 30    * formula. It has methods to check those elements for certain criteria.
 31    *
 32    * @version $Revision: 1.6 $
 33    * @author Michael Meyling
 34    */
 35    public final class FormulaChecker implements Operators, FormulaBasicErrors {
 36   
 37    // If you want to check if the context information within this class is correct you have to
 38    // do the following:
 39    // 1. add "private Qedeq qedeq;" as a new field of this class
 40    // 2. add DynamicGetter from test project into this package
 41    // 3. modify {@link #setLocationWithinModule(String) by calling
 42    // DynamicGetter.get(qedeq, getCurrentContext().getLocationWithinModule());
 43    // 4. modify the {@link #checkFormula(Element, ModuleContext, ExistenceChecker} by adding
 44    // a Qedeq parameter;
 45    // 5. modify {@link #checkTerm(Elment, ModuleContext, ExistenceChecker) analogous
 46   
 47    /** Current context during creation. */
 48    private final ModuleContext currentContext;
 49   
 50    /** Existence checker for operators. */
 51    private final ExistenceChecker existenceChecker;
 52   
 53    /**
 54    * Constructor.
 55    *
 56    * @param context For location information. Important for locating errors.
 57    * @param existenceChecker Existence checker for operators.
 58    * @throws IllegalArgumentException The <code>existenceChecker</code> says the equality
 59    * operator exists but the predicate is not found.
 60    */
 61  425 private FormulaChecker(final ModuleContext context,
 62    final ExistenceChecker existenceChecker) {
 63  425 this.existenceChecker = existenceChecker;
 64  425 if (existenceChecker.equalityOperatorExists()
 65    && !existenceChecker.predicateExists(existenceChecker.getEqualityOperator(), 2)) {
 66  0 throw new IllegalArgumentException("equality predicate should exist, but it doesn't");
 67    }
 68  425 currentContext = new ModuleContext(context);
 69    }
 70   
 71    /**
 72    * Is {@link Element} a formula?
 73    *
 74    * @param element Check this element.
 75    * @param context For location information. Important for locating errors.
 76    * @throws CheckException It is no formula.
 77    */
 78  51 public static final void checkFormula(final Element element, final ModuleContext context)
 79    throws CheckException {
 80  51 checkFormula(element, context, EverythingExists.getInstance());
 81    }
 82   
 83    /**
 84    * Is {@link Element} a formula?
 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    * @throws CheckException It is no formula.
 90    */
 91  330 public static final void checkFormula(final Element element, final ModuleContext context,
 92    final ExistenceChecker existenceChecker) throws CheckException {
 93  330 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 94  330 checker.checkFormula(element);
 95    }
 96   
 97    /**
 98    * Is {@link Element} a term?
 99    *
 100    * @param element Check this element.
 101    * @param context For location information. Important for locating errors.
 102    * @throws CheckException It is no term.
 103    */
 104  21 public static final void checkTerm(final Element element, final ModuleContext context)
 105    throws CheckException {
 106  21 checkTerm(element, context, EverythingExists.getInstance());
 107    }
 108   
 109    /**
 110    * Is {@link Element} a term?
 111    *
 112    * @param element Check this element.
 113    * @param context For location information. Important for locating errors.
 114    * @param existenceChecker Existence checker for operators.
 115    * @throws CheckException It is no term.
 116    */
 117  95 public static final void checkTerm(final Element element, final ModuleContext context,
 118    final ExistenceChecker existenceChecker) throws CheckException {
 119  95 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 120  95 checker.checkTerm(element);
 121    }
 122   
 123    /**
 124    * Is {@link Element} a formula?
 125    *
 126    * @param element Check this element.
 127    * @throws CheckException It is no formula.
 128    */
 129  1786 private final void checkFormula(final Element element)
 130    throws CheckException {
 131  1786 final String method = "checkFormula";
 132  1786 Trace.begin(this, method);
 133  1786 Trace.param(this, method, "element", element);
 134  1786 final String context = getCurrentContext().getLocationWithinModule();
 135  1786 Trace.param(this, method, "context", context);
 136  1786 checkList(element);
 137  1779 final ElementList list = element.getList();
 138  1779 final String listContext = context + ".getList()";
 139  1779 setLocationWithinModule(listContext);
 140  1779 final String operator = list.getOperator();
 141  1779 if (operator.equals(CONJUNCTION_OPERATOR)
 142    || operator.equals(DISJUNCTION_OPERATOR)
 143    || operator.equals(IMPLICATION_OPERATOR)
 144    || operator.equals(EQUIVALENCE_OPERATOR)) {
 145  480 Trace.trace(this, method, "one of (and, or, implication, equivalence) operator found");
 146  480 if (list.size() <= 1) {
 147  9 throw new FormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
 148    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
 149    + operator + "\"", element, getCurrentContext());
 150    }
 151  471 if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
 152  1 throw new FormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
 153    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
 154    + operator + "\"", element, getCurrentContext());
 155    }
 156  470 for (int i = 0; i < list.size(); i++) {
 157  1052 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 158  1052 checkFormula(list.getElement(i));
 159    }
 160  466 setLocationWithinModule(listContext);
 161  466 checkFreeAndBoundDisjunct(0, list);
 162  1299 } else if (operator.equals(NEGATION_OPERATOR)) {
 163  38 Trace.trace(this, method, "negation operator found");
 164  38 setLocationWithinModule(listContext);
 165  38 if (list.size() != 1) {
 166  2 throw new FormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
 167    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
 168    element, getCurrentContext());
 169    }
 170  36 setLocationWithinModule(listContext + ".getElement(0)");
 171  36 checkFormula(list.getElement(0));
 172  1261 } else if (operator.equals(PREDICATE_VARIABLE)
 173    || operator.equals(PREDICATE_CONSTANT)) {
 174  1039 Trace.trace(this, method, "predicate operator found");
 175  1039 setLocationWithinModule(listContext);
 176  1039 if (list.size() < 1) {
 177  2 throw new FormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
 178    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
 179    element, getCurrentContext());
 180    }
 181    // check if first argument is an atom
 182  1037 setLocationWithinModule(listContext + ".getElement(0)");
 183  1037 checkAtomFirst(list.getElement(0));
 184   
 185    // check if rest arguments are terms
 186  1029 for (int i = 1; i < list.size(); i++) {
 187  1431 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 188  1431 checkTerm(list.getElement(i));
 189    }
 190   
 191  1027 setLocationWithinModule(listContext);
 192  1027 checkFreeAndBoundDisjunct(1, list);
 193   
 194    // check if predicate is known
 195  1023 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
 196    list.getElement(0).getAtom().getString(), list.size() - 1)) {
 197  2 throw new FormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
 198    UNKNOWN_PREDICATE_CONSTANT_TEXT, element, getCurrentContext());
 199    }
 200   
 201  222 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 202    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 203    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 204  217 Trace.trace(this, method, "quantifier found");
 205  217 setLocationWithinModule(context);
 206  217 checkQuantifier(element);
 207    } else {
 208  5 setLocationWithinModule(listContext + ".getOperator()");
 209  5 throw new FormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
 210    UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
 211    element, getCurrentContext());
 212    }
 213    // restore context
 214  1693 setLocationWithinModule(context);
 215  1693 Trace.end(this, method);
 216    }
 217   
 218    /**
 219    * Check quantifier element.
 220    *
 221    * @param element Check this element. Must be a quantifier element.
 222    * @throws CheckException Check failed.
 223    * @throws IllegalArgumentException <code>element.getList().getOperator()</code> is no
 224    * quantifier operator.
 225    */
 226  217 private void checkQuantifier(final Element element) throws CheckException {
 227  217 final String method = "checkQuantifier";
 228  217 Trace.begin(this, method);
 229  217 Trace.param(this, method, "element", element);
 230    // save context
 231  217 final String context = getCurrentContext().getLocationWithinModule();
 232  217 Trace.param(this, method, "context", context);
 233  217 checkList(element);
 234  217 final ElementList list = element.getList();
 235  217 final String listContext = context + ".getList()";
 236  217 setLocationWithinModule(listContext);
 237  217 final String operator = list.getOperator();
 238  217 if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 239    && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 240    && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 241  0 throw new IllegalArgumentException("quantifier element expected but found: "
 242    + element.toString());
 243    }
 244  217 if (list.size() < 2 || list.size() > 3) {
 245  0 throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
 246    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
 247    }
 248   
 249    // check if unique existential operator could be used
 250  217 if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 251    && !existenceChecker.equalityOperatorExists()) {
 252  0 setLocationWithinModule(listContext + ".getOperator()");
 253  0 throw new FormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
 254    EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
 255    }
 256   
 257    // check if first argument is subject variable
 258  217 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 259  217 checkSubjectVariable(list.getElement(0));
 260   
 261    // check if second argument is a formula
 262  214 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
 263  214 checkFormula(list.getElement(1));
 264   
 265  208 setLocationWithinModule(listContext);
 266    // check if subject variable is not already bound in formula
 267  208 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
 268    list.getElement(0))) {
 269  7 throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 270    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
 271    getCurrentContext());
 272    }
 273  201 if (list.size() > 3) {
 274  0 throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
 275    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
 276    getCurrentContext());
 277    }
 278  201 if (list.size() > 2) {
 279    // check if third argument is a formula
 280  41 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
 281  41 checkFormula(list.getElement(2));
 282   
 283  41 setLocationWithinModule(listContext);
 284    // check if subject variable is not bound in formula
 285  41 if (FormulaChecker.getBoundSubjectVariables(list.getElement(2)).contains(
 286    list.getElement(0))) {
 287  3 throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 288    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
 289    getCurrentContext());
 290    }
 291    // the following check restricts the restriction formula for quantifiers
 292    // to formulas that contain the subject variable as free variable
 293  38 setLocationWithinModule(listContext);
 294  38 if (!getFreeSubjectVariables(list.getElement(1)).contains(
 295    list.getElement(0))) {
 296  4 throw new FormulaCheckException(
 297    SUBJECT_VARIABLE_OCCURS_NOT_IN_RESTRICTION_FORMULA,
 298    SUBJECT_VARIABLE_OCCURS_NOT_IN_RESTRICTION_FORMULA_TEXT,
 299    list.getElement(0), getCurrentContext());
 300    }
 301  34 checkFreeAndBoundDisjunct(1, list);
 302    }
 303    // restore context
 304  182 setLocationWithinModule(context);
 305  182 Trace.end(this, method);
 306    }
 307   
 308    /**
 309    * Is {@link Element} a term?
 310    *
 311    * @param element Check this element.
 312    * @throws CheckException It is no term.
 313    */
 314  2126 private void checkTerm(final Element element) throws CheckException {
 315  2126 final String method = "checkTerm";
 316  2126 Trace.begin(this, method);
 317  2126 Trace.param(this, method, "element", element);
 318    // save current context
 319  2126 final String context = getCurrentContext().getLocationWithinModule();
 320  2126 Trace.param(this, method, "context", context);
 321  2126 checkList(element);
 322  2122 final ElementList list = element.getList();
 323  2122 final String listContext = context + ".getList()";
 324  2122 setLocationWithinModule(listContext);
 325  2122 final String operator = list.getOperator();
 326  2122 if (operator.equals(SUBJECT_VARIABLE)) {
 327  1479 checkSubjectVariable(element);
 328  643 } else if (operator.equals(FUNCTION_CONSTANT)
 329    || operator.equals(FUNCTION_VARIABLE)) {
 330   
 331    // function constants must have at least a function name
 332  516 if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
 333  1 throw new TermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
 334    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
 335    }
 336   
 337    // function variables must have at least a function name and at least one argument
 338  515 if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
 339  2 throw new TermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
 340    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
 341    }
 342   
 343    // check if first argument is an atom
 344  513 setLocationWithinModule(listContext + ".getElement(0)");
 345  513 checkAtomFirst(list.getElement(0));
 346   
 347    // check if all arguments are terms
 348  506 setLocationWithinModule(listContext);
 349  506 for (int i = 1; i < list.size(); i++) {
 350  600 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 351  600 checkTerm(list.getElement(i));
 352    }
 353   
 354  505 setLocationWithinModule(listContext);
 355  505 checkFreeAndBoundDisjunct(1, list);
 356   
 357    // check if function is known
 358  501 setLocationWithinModule(listContext);
 359  501 if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
 360    list.getElement(0).getAtom().getString(), list.size() - 1)) {
 361  2 throw new FormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
 362    UNKNOWN_FUNCTION_CONSTANT_TEXT, element, getCurrentContext());
 363    }
 364   
 365  127 } else if (operator.equals(CLASS)) {
 366   
 367  116 if (list.size() != 2) {
 368  2 throw new TermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
 369    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
 370    }
 371    // check if first argument is a subject variable
 372  114 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 373  114 if (!isSubjectVariable(list.getElement(0))) {
 374  1 throw new TermCheckException(SUBJECT_VARIABLE_EXPECTED,
 375    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
 376    }
 377   
 378    // check if the second argument is a formula
 379  113 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
 380  113 checkFormula(list.getElement(1));
 381   
 382    // check if class operator is allowed
 383  113 setLocationWithinModule(listContext);
 384  113 if (!existenceChecker.classOperatorExists()) {
 385  2 throw new FormulaCheckException(CLASS_OPERATOR_STILL_UNKNOWN,
 386    CLASS_OPERATOR_STILL_UNKNOWN_TEXT, element, getCurrentContext());
 387    }
 388   
 389    // check if subject variable is not bound in formula
 390  111 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 391  111 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
 392    list.getElement(0))) {
 393  1 throw new TermCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 394    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(0),
 395    getCurrentContext());
 396    }
 397   
 398    } else {
 399  11 setLocationWithinModule(listContext + ".getOperator()");
 400  11 throw new TermCheckException(UNKNOWN_TERM_OPERATOR,
 401    UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext());
 402    }
 403    // restore context
 404  2085 setLocationWithinModule(context);
 405  2085 Trace.end(this, method);
 406    }
 407   
 408    /**
 409    * Check if no bound variables are free and vice versa.
 410    * The current context must be at the list element.
 411    *
 412    * @param start Start check with this list position. Beginning with 0.
 413    * @param list List element to check.
 414    * @throws CheckException At least one variable occurs free and bound in different
 415    * sub-elements.
 416    */
 417  2032 private void checkFreeAndBoundDisjunct(final int start,
 418    final ElementList list) throws CheckException {
 419    // save current context
 420  2032 final String context = getCurrentContext().getLocationWithinModule();
 421  2032 final ElementSet free = new ElementSet();
 422  2032 final ElementSet bound = new ElementSet();
 423  2032 for (int i = start; i < list.size(); i++) {
 424  3140 setLocationWithinModule(context + ".getElement(" + i + ")");
 425  3140 final ElementSet newFree
 426    = getFreeSubjectVariables(list.getElement(i));
 427  3140 final ElementSet newBound
 428    = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
 429  3140 final ElementSet interBound = newFree.newIntersection(bound);
 430  3140 if (!interBound.isEmpty()) {
 431  17 throw new FormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
 432    FREE_VARIABLE_ALREADY_BOUND_TEXT
 433    + interBound, list.getElement(i), getCurrentContext());
 434    }
 435  3123 final ElementSet interFree = newBound.newIntersection(free);
 436  3123 if (!interFree.isEmpty()) {
 437  15 throw new FormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
 438    BOUND_VARIABLE_ALREADY_FREE_TEXT
 439    + interFree, list.getElement(i), getCurrentContext());
 440    }
 441  3108 bound.union(newBound);
 442  3108