Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Sa Jan 26 2008 14:11:34 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 673   Methods: 17
NCLOC: 430   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
FormulaChecker.java 92,4% 95,8% 100% 94,9%
coverage coverage
 1    /* $Id: FormulaChecker.java,v 1.9 2008/01/26 12:39:09 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.bo.module.ModuleContext;
 24    import org.qedeq.kernel.dto.list.ElementSet;
 25    import org.qedeq.kernel.trace.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    * LATER mime 20070307: here are sometimes error messages that get concatenated with
 33    * an {@link org.qedeq.kernel.base.list.ElementList#getOperator()} string. Perhaps these
 34    * strings must be translated into the original input format and a mapping must be done.
 35    *
 36    * @version $Revision: 1.9 $
 37    * @author Michael Meyling
 38    */
 39    public final class FormulaChecker implements Operators, FormulaBasicErrors {
 40   
 41    // If you want to check if the context information within this class is correct you have to
 42    // do the following:
 43    // 1. add "private Qedeq qedeq;" as a new field of this class
 44    // 2. add DynamicGetter from test project into this package
 45    // 3. modify {@link #setLocationWithinModule(String) by calling
 46    // DynamicGetter.get(qedeq, getCurrentContext().getLocationWithinModule());
 47    // 4. modify the {@link #checkFormula(Element, ModuleContext, ExistenceChecker} by adding
 48    // a Qedeq parameter;
 49    // 5. modify {@link #checkTerm(Element, ModuleContext, ExistenceChecker) analogous
 50   
 51    /** This class. */
 52    private static final Class CLASS = FormulaChecker.class;
 53   
 54    /** Current context during creation. */
 55    private final ModuleContext currentContext;
 56   
 57    /** Existence checker for operators. */
 58    private final ExistenceChecker existenceChecker;
 59   
 60    /**
 61    * Constructor.
 62    *
 63    * @param context For location information. Important for locating errors.
 64    * @param existenceChecker Existence checker for operators.
 65    * @throws IllegalArgumentException The <code>existenceChecker</code> says the equality
 66    * operator exists but the predicate is not found. This should be a programming
 67    * error.
 68    */
 69  1006 private FormulaChecker(final ModuleContext context,
 70    final ExistenceChecker existenceChecker) {
 71  1006 this.existenceChecker = existenceChecker;
 72  1006 if (existenceChecker.equalityOperatorExists()
 73    && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
 74  0 throw new IllegalArgumentException("equality predicate should exist, but it doesn't");
 75    }
 76  1006 currentContext = new ModuleContext(context);
 77    }
 78   
 79    /**
 80    * Is {@link Element} a formula?
 81    *
 82    * @param element Check this element.
 83    * @param context For location information. Important for locating errors.
 84    * @param existenceChecker Existence checker for operators.
 85    * @throws LogicalCheckException It is no formula.
 86    */
 87  847 public static final void checkFormula(final Element element, final ModuleContext context,
 88    final ExistenceChecker existenceChecker) throws LogicalCheckException {
 89  847 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 90  847 checker.checkFormula(element);
 91    }
 92   
 93    /**
 94    * Is {@link Element} a formula? All predicates and functions are assumed to exit.
 95    * If the existence context is known you should use
 96    * {@link #checkFormula(Element, ModuleContext, ExistenceChecker)}.
 97    *
 98    * @param element Check this element.
 99    * @param context For location information. Important for locating errors.
 100    * @throws LogicalCheckException It is no formula.
 101    */
 102  51 public static final void checkFormula(final Element element, final ModuleContext context)
 103    throws LogicalCheckException {
 104  51 checkFormula(element, context, EverythingExists.getInstance());
 105    }
 106   
 107    /**
 108    * Is {@link Element} a term?
 109    *
 110    * @param element Check this element.
 111    * @param context For location information. Important for locating errors.
 112    * @param existenceChecker Existence checker for operators.
 113    * @throws LogicalCheckException It is no term.
 114    */
 115  159 public static final void checkTerm(final Element element, final ModuleContext context,
 116    final ExistenceChecker existenceChecker) throws LogicalCheckException {
 117  159 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 118  159 checker.checkTerm(element);
 119    }
 120   
 121    /**
 122    * Is {@link Element} a term? If the existence context is known you should use
 123    * {@link #checkTerm(Element, ModuleContext, ExistenceChecker)}.
 124    *
 125    * @param element Check this element.
 126    * @param context For location information. Important for locating errors.
 127    * @throws LogicalCheckException It is no term.
 128    */
 129  21 public static final void checkTerm(final Element element, final ModuleContext context)
 130    throws LogicalCheckException {
 131  21 checkTerm(element, context, EverythingExists.getInstance());
 132    }
 133   
 134    /**
 135    * Is {@link Element} a formula?
 136    *
 137    * @param element Check this element.
 138    * @throws LogicalCheckException It is no formula.
 139    */
 140  8497 private final void checkFormula(final Element element)
 141    throws LogicalCheckException {
 142  8497 final String method = "checkFormula";
 143  8497 Trace.begin(CLASS, this, method);
 144  8497 Trace.param(CLASS, this, method, "element", element);
 145  8497 final String context = getCurrentContext().getLocationWithinModule();
 146  8497 Trace.param(CLASS, this, method, "context", context);
 147  8497 checkList(element);
 148  8490 final ElementList list = element.getList();
 149  8490 final String listContext = context + ".getList()";
 150  8490 setLocationWithinModule(listContext);
 151  8490 final String operator = list.getOperator();
 152  8490 if (operator.equals(CONJUNCTION_OPERATOR)
 153    || operator.equals(DISJUNCTION_OPERATOR)
 154    || operator.equals(IMPLICATION_OPERATOR)
 155    || operator.equals(EQUIVALENCE_OPERATOR)) {
 156  2742 Trace.trace(CLASS, this, method,
 157    "one of (and, or, implication, equivalence) operator found");
 158  2742 if (list.size() <= 1) {
 159  9 throw new FormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
 160    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
 161    + operator + "\"", element, getCurrentContext());
 162    }
 163  2733 if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
 164  1 throw new FormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
 165    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
 166    + operator + "\"", element, getCurrentContext());
 167    }
 168  2732 for (int i = 0; i < list.size(); i++) {
 169  6186 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 170  6186 checkFormula(list.getElement(i));
 171    }
 172  2718 setLocationWithinModule(listContext);
 173  2718 checkFreeAndBoundDisjunct(0, list);
 174  5748 } else if (operator.equals(NEGATION_OPERATOR)) {
 175  299 Trace.trace(CLASS, this, method, "negation operator found");
 176  299 setLocationWithinModule(listContext);
 177  299 if (list.size() != 1) {
 178  2 throw new FormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
 179    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
 180    element, getCurrentContext());
 181    }
 182  297 setLocationWithinModule(listContext + ".getElement(0)");
 183  297 checkFormula(list.getElement(0));
 184  5449 } else if (operator.equals(PREDICATE_VARIABLE)
 185    || operator.equals(PREDICATE_CONSTANT)) {
 186  4583 Trace.trace(CLASS, this, method, "predicate operator found");
 187  4583 setLocationWithinModule(listContext);
 188  4583 if (list.size() < 1) {
 189  2 throw new FormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
 190    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
 191    element, getCurrentContext());
 192    }
 193    // check if first argument is an atom
 194  4581 setLocationWithinModule(listContext + ".getElement(0)");
 195  4581 checkAtomFirst(list.getElement(0));
 196   
 197    // check if rest arguments are terms
 198  4573 for (int i = 1; i < list.size(); i++) {
 199  4484 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 200  4484 checkTerm(list.getElement(i));
 201    }
 202   
 203  4571 setLocationWithinModule(listContext);
 204  4571 checkFreeAndBoundDisjunct(1, list);
 205   
 206    // check if predicate is known
 207  4567 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
 208    list.getElement(0).getAtom().getString(), list.size() - 1)) {
 209  6 throw new FormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
 210    UNKNOWN_PREDICATE_CONSTANT_TEXT + "\""
 211    + list.getElement(0).getAtom().getString() + "\" [" + (list.size() - 1) + "]",
 212    element, getCurrentContext());
 213    }
 214   
 215  866 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 216    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 217    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 218  861 Trace.trace(CLASS, this, method, "quantifier found");
 219  861 setLocationWithinModule(context);
 220  861 checkQuantifier(element);
 221    } else {
 222  5 setLocationWithinModule(listContext + ".getOperator()");
 223  5 throw new FormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
 224    UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
 225    element, getCurrentContext());
 226    }
 227    // restore context
 228  8374 setLocationWithinModule(context);
 229  8374 Trace.end(CLASS, this, method);
 230    }
 231   
 232    /**
 233    * Check quantifier element.
 234    *
 235    * @param element Check this element. Must be a quantifier element.
 236    * @throws LogicalCheckException Check failed.
 237    * @throws IllegalArgumentException <code>element.getList().getOperator()</code> is no
 238    * quantifier operator.
 239    */
 240  861 private void checkQuantifier(final Element element) throws LogicalCheckException {
 241  861 final String method = "checkQuantifier";
 242  861 Trace.begin(CLASS, this, method);
 243  861 Trace.param(CLASS, this, method, "element", element);
 244    // save context
 245  861 final String context = getCurrentContext().getLocationWithinModule();
 246  861 Trace.param(CLASS, this, method, "context", context);
 247  861 checkList(element);
 248  861 final ElementList list = element.getList();
 249  861 final String listContext = context + ".getList()";
 250  861 setLocationWithinModule(listContext);
 251  861 final String operator = list.getOperator();
 252  861 if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 253    && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 254    && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 255  0 throw new IllegalArgumentException("quantifier element expected but found: "
 256    + element.toString());
 257    }
 258  861 if (list.size() < 2 || list.size() > 3) {
 259  0 throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
 260    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
 261    }
 262   
 263    // check if unique existential operator could be used
 264  861 if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 265    && !existenceChecker.equalityOperatorExists()) {
 266  0 setLocationWithinModule(listContext + ".getOperator()");
 267  0 throw new FormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
 268    EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
 269    }
 270   
 271    // check if first argument is subject variable
 272  861 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 273  861 checkSubjectVariable(list.getElement(0));
 274   
 275    // check if second argument is a formula
 276  858 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
 277  858 checkFormula(list.getElement(1));
 278   
 279  853 setLocationWithinModule(listContext);
 280    // check if subject variable is not already bound in formula
 281  853 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
 282    list.getElement(0))) {
 283  14 throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 284    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
 285    getCurrentContext());
 286    }
 287  839 if (list.size() > 3) {
 288  0 throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
 289    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
 290    getCurrentContext());
 291    }
 292  839 if (list.size() > 2) {
 293    // check if third argument is a formula
 294  68 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
 295  68 checkFormula(list.getElement(2));
 296   
 297    // check if subject variable is not bound in formula
 298  64 setLocationWithinModule(listContext);
 299  64 if (FormulaChecker.getBoundSubjectVariables(list.getElement(2)).contains(
 300    list.getElement(0))) {
 301  3 throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 302    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
 303    getCurrentContext());
 304    }
 305  61 setLocationWithinModule(listContext);
 306  61 checkFreeAndBoundDisjunct(1, list);
 307    }
 308    // restore context
 309  820 setLocationWithinModule(context);
 310  820 Trace.end(CLASS, this, method);
 311    }
 312   
 313    /**
 314    * Is {@link Element} a term?
 315    *
 316    * @param element Check this element.
 317    * @throws LogicalCheckException It is no term.
 318    */
 319  6393 private void checkTerm(final Element element) throws LogicalCheckException {
 320  6393 final String method = "checkTerm";
 321  6393 Trace.begin(CLASS, this, method);
 322  6393 Trace.param(CLASS, this, method, "element", element);
 323    // save current context
 324  6393 final String context = getCurrentContext().getLocationWithinModule();
 325  6393 Trace.param(CLASS, this, method, "context", context);
 326  6393 checkList(element);
 327  6389 final ElementList list = element.getList();
 328  6389 final String listContext = context + ".getList()";
 329  6389 setLocationWithinModule(listContext);
 330  6389 final String operator = list.getOperator();
 331  6389 if (operator.equals(SUBJECT_VARIABLE)) {
 332  4640 checkSubjectVariable(element);
 333  1749 } else if (operator.equals(FUNCTION_CONSTANT)
 334    || operator.equals(FUNCTION_VARIABLE)) {
 335   
 336    // function constants must have at least a function name
 337  1494 if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
 338  1 throw new TermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
 339    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
 340    }
 341   
 342    // function variables must have at least a function name and at least one argument
 343  1493 if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
 344  2 throw new TermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
 345    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
 346    }
 347   
 348    // check if first argument is an atom
 349  1491 setLocationWithinModule(listContext + ".getElement(0)");
 350  1491 checkAtomFirst(list.getElement(0));
 351   
 352    // check if all arguments are terms
 353  1484 setLocationWithinModule(listContext);
 354  1484 for (int i = 1; i < list.size(); i++) {
 355  1750 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 356  1750 checkTerm(list.getElement(i));
 357    }
 358   
 359  1483 setLocationWithinModule(listContext);
 360  1483 checkFreeAndBoundDisjunct(1, list);
 361   
 362    // check if function is known
 363  1479 setLocationWithinModule(listContext);
 364  1479 if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
 365    list.getElement(0).getAtom().getString(), list.size() - 1)) {
 366  2 throw new FormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
 367    UNKNOWN_FUNCTION_CONSTANT_TEXT + "\""
 368    + list.getElement(0).getAtom().getString() + "\"", element,
 369    getCurrentContext());
 370    }
 371   
 372  255 } else if (operator.equals(CLASS_OP)) {
 373   
 374  244 if (list.size() != 2) {
 375  2 throw new TermCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
 376    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
 377    }
 378    // check if first argument is a subject variable
 379  242 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 380  242 if (!isSubjectVariable(list.getElement(0))) {
 381  1 throw new TermCheckException(SUBJECT_VARIABLE_EXPECTED,
 382    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
 383    }
 384   
 385    // check if the second argument is a formula
 386  241 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
 387  241 checkFormula(list.getElement(1));
 388   
 389    // check if class operator is allowed
 390  241 setLocationWithinModule(listContext);
 391  241 if (!existenceChecker.classOperatorExists()) {
 392  2 throw new FormulaCheckException(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  239 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 398  239 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
 399    list.getElement(0))) {
 400  1 throw new TermCheckException(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 throw new TermCheckException(UNKNOWN_TERM_OPERATOR,
 408    UNKNOWN_TERM_OPERATOR_TEXT + "\"" + operator + "\"", element, getCurrentContext());
 409    }
 410    // restore context
 411  6352 setLocationWithinModule(context);
 412  6352 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    * @throws LogicalCheckException At least one variable occurs free and bound in different
 422    * sub-elements.
 423    */
 424  8833 private void checkFreeAndBoundDisjunct(final int start,
 425    final ElementList list) throws LogicalCheckException {
 426    // save current context
 427  8833 final String context = getCurrentContext().getLocationWithinModule();
 428  8833 final ElementSet free = new ElementSet();
 429  8833 final ElementSet bound = new ElementSet();
 430  8833 for (int i = start; i < list.size(); i++) {
 431  12518 setLocationWithinModule(context + ".getElement(" + i + ")");
 432  12518 final ElementSet newFree
 433    = getFreeSubjectVariables(list.getElement(i));
 434  12518 final ElementSet newBound
 435    = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
 436  12518 final ElementSet interBound = newFree.newIntersection(bound);
 437  12518 if (!interBound.isEmpty()) {
 438  24 throw new FormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
 439    FREE_VARIABLE_ALREADY_BOUND_TEXT
 440    + interBound, list.getElement(i), getCurrentContext());
 441    }
 442  12494 final ElementSet interFree = newBound.newIntersection(fre