Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: So Sep 2 2007 02:40:58 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 666   Methods: 17
NCLOC: 428   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.8 2007/04/12 23:50:08 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.8 $
 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(Elment, ModuleContext, ExistenceChecker) analogous
 50   
 51    /** Current context during creation. */
 52    private final ModuleContext currentContext;
 53   
 54    /** Existence checker for operators. */
 55    private final ExistenceChecker existenceChecker;
 56   
 57    /**
 58    * Constructor.
 59    *
 60    * @param context For location information. Important for locating errors.
 61    * @param existenceChecker Existence checker for operators.
 62    * @throws IllegalArgumentException The <code>existenceChecker</code> says the equality
 63    * operator exists but the predicate is not found. This should be a programming
 64    * error.
 65    */
 66  737 private FormulaChecker(final ModuleContext context,
 67    final ExistenceChecker existenceChecker) {
 68  737 this.existenceChecker = existenceChecker;
 69  737 if (existenceChecker.equalityOperatorExists()
 70    && !existenceChecker.predicateExists(existenceChecker.getEqualityOperator(), 2)) {
 71  0 throw new IllegalArgumentException("equality predicate should exist, but it doesn't");
 72    }
 73  737 currentContext = new ModuleContext(context);
 74    }
 75   
 76    /**
 77    * Is {@link Element} a formula?
 78    *
 79    * @param element Check this element.
 80    * @param context For location information. Important for locating errors.
 81    * @throws LogicalCheckException It is no formula.
 82    */
 83  51 public static final void checkFormula(final Element element, final ModuleContext context)
 84    throws LogicalCheckException {
 85  51 checkFormula(element, context, EverythingExists.getInstance());
 86    }
 87   
 88    /**
 89    * Is {@link Element} a formula?
 90    *
 91    * @param element Check this element.
 92    * @param context For location information. Important for locating errors.
 93    * @param existenceChecker Existence checker for operators.
 94    * @throws LogicalCheckException It is no formula.
 95    */
 96  594 public static final void checkFormula(final Element element, final ModuleContext context,
 97    final ExistenceChecker existenceChecker) throws LogicalCheckException {
 98  594 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 99  594 checker.checkFormula(element);
 100    }
 101   
 102    /**
 103    * Is {@link Element} a term?
 104    *
 105    * @param element Check this element.
 106    * @param context For location information. Important for locating errors.
 107    * @throws LogicalCheckException It is no term.
 108    */
 109  21 public static final void checkTerm(final Element element, final ModuleContext context)
 110    throws LogicalCheckException {
 111  21 checkTerm(element, context, EverythingExists.getInstance());
 112    }
 113   
 114    /**
 115    * Is {@link Element} a term?
 116    *
 117    * @param element Check this element.
 118    * @param context For location information. Important for locating errors.
 119    * @param existenceChecker Existence checker for operators.
 120    * @throws LogicalCheckException It is no term.
 121    */
 122  143 public static final void checkTerm(final Element element, final ModuleContext context,
 123    final ExistenceChecker existenceChecker) throws LogicalCheckException {
 124  143 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 125  143 checker.checkTerm(element);
 126    }
 127   
 128    /**
 129    * Is {@link Element} a formula?
 130    *
 131    * @param element Check this element.
 132    * @throws LogicalCheckException It is no formula.
 133    */
 134  4670 private final void checkFormula(final Element element)
 135    throws LogicalCheckException {
 136  4670 final String method = "checkFormula";
 137  4670 Trace.begin(this, method);
 138  4670 Trace.param(this, method, "element", element);
 139  4670 final String context = getCurrentContext().getLocationWithinModule();
 140  4670 Trace.param(this, method, "context", context);
 141  4670 checkList(element);
 142  4663 final ElementList list = element.getList();
 143  4663 final String listContext = context + ".getList()";
 144  4663 setLocationWithinModule(listContext);
 145  4663 final String operator = list.getOperator();
 146  4663 if (operator.equals(CONJUNCTION_OPERATOR)
 147    || operator.equals(DISJUNCTION_OPERATOR)
 148    || operator.equals(IMPLICATION_OPERATOR)
 149    || operator.equals(EQUIVALENCE_OPERATOR)) {
 150  1453 Trace.trace(this, method, "one of (and, or, implication, equivalence) operator found");
 151  1453 if (list.size() <= 1) {
 152  9 throw new FormulaCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
 153    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT + "\""
 154    + operator + "\"", element, getCurrentContext());
 155    }
 156  1444 if (operator.equals(IMPLICATION_OPERATOR) && list.size() != 2) {
 157  1 throw new FormulaCheckException(EXACTLY_TWO_ARGUMENTS_EXPECTED,
 158    EXACTLY_TWO_ARGUMENTS_EXPECTED_TEXT + "\""
 159    + operator + "\"", element, getCurrentContext());
 160    }
 161  1443 for (int i = 0; i < list.size(); i++) {
 162  3290 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 163  3290 checkFormula(list.getElement(i));
 164    }
 165  1434 setLocationWithinModule(listContext);
 166  1434 checkFreeAndBoundDisjunct(0, list);
 167  3210 } else if (operator.equals(NEGATION_OPERATOR)) {
 168  159 Trace.trace(this, method, "negation operator found");
 169  159 setLocationWithinModule(listContext);
 170  159 if (list.size() != 1) {
 171  2 throw new FormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
 172    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
 173    element, getCurrentContext());
 174    }
 175  157 setLocationWithinModule(listContext + ".getElement(0)");
 176  157 checkFormula(list.getElement(0));
 177  3051 } else if (operator.equals(PREDICATE_VARIABLE)
 178    || operator.equals(PREDICATE_CONSTANT)) {
 179  2670 Trace.trace(this, method, "predicate operator found");
 180  2670 setLocationWithinModule(listContext);
 181  2670 if (list.size() < 1) {
 182  2 throw new FormulaCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
 183    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT + "\"" + operator + "\"",
 184    element, getCurrentContext());
 185    }
 186    // check if first argument is an atom
 187  2668 setLocationWithinModule(listContext + ".getElement(0)");
 188  2668 checkAtomFirst(list.getElement(0));
 189   
 190    // check if rest arguments are terms
 191  2660 for (int i = 1; i < list.size(); i++) {
 192  3112 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 193  3112 checkTerm(list.getElement(i));
 194    }
 195   
 196  2658 setLocationWithinModule(listContext);
 197  2658 checkFreeAndBoundDisjunct(1, list);
 198   
 199    // check if predicate is known
 200  2654 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
 201    list.getElement(0).getAtom().getString(), list.size() - 1)) {
 202  4 throw new FormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
 203    UNKNOWN_PREDICATE_CONSTANT_TEXT + "\""
 204    + list.getElement(0).getAtom().getString() + "\"", element,
 205    getCurrentContext());
 206    }
 207   
 208  381 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 209    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 210    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 211  376 Trace.trace(this, method, "quantifier found");
 212  376 setLocationWithinModule(context);
 213  376 checkQuantifier(element);
 214    } else {
 215  5 setLocationWithinModule(listContext + ".getOperator()");
 216  5 throw new FormulaCheckException(UNKNOWN_LOGICAL_OPERATOR,
 217    UNKNOWN_LOGICAL_OPERATOR_TEXT + "\"" + operator + "\"",
 218    element, getCurrentContext());
 219    }
 220    // restore context
 221  4562 setLocationWithinModule(context);
 222  4562 Trace.end(this, method);
 223    }
 224   
 225    /**
 226    * Check quantifier element.
 227    *
 228    * @param element Check this element. Must be a quantifier element.
 229    * @throws LogicalCheckException Check failed.
 230    * @throws IllegalArgumentException <code>element.getList().getOperator()</code> is no
 231    * quantifier operator.
 232    */
 233  376 private void checkQuantifier(final Element element) throws LogicalCheckException {
 234  376 final String method = "checkQuantifier";
 235  376 Trace.begin(this, method);
 236  376 Trace.param(this, method, "element", element);
 237    // save context
 238  376 final String context = getCurrentContext().getLocationWithinModule();
 239  376 Trace.param(this, method, "context", context);
 240  376 checkList(element);
 241  376 final ElementList list = element.getList();
 242  376 final String listContext = context + ".getList()";
 243  376 setLocationWithinModule(listContext);
 244  376 final String operator = list.getOperator();
 245  376 if (!operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 246    && operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 247    && operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 248  0 throw new IllegalArgumentException("quantifier element expected but found: "
 249    + element.toString());
 250    }
 251  376 if (list.size() < 2 || list.size() > 3) {
 252  0 throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
 253    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, element, getCurrentContext());
 254    }
 255   
 256    // check if unique existential operator could be used
 257  376 if (operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 258    && !existenceChecker.equalityOperatorExists()) {
 259  0 setLocationWithinModule(listContext + ".getOperator()");
 260  0 throw new FormulaCheckException(EQUALITY_PREDICATE_NOT_YET_DEFINED,
 261    EQUALITY_PREDICATE_NOT_YET_DEFINED_TEXT, element, getCurrentContext());
 262    }
 263   
 264    // check if first argument is subject variable
 265  376 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 266  376 checkSubjectVariable(list.getElement(0));
 267   
 268    // check if second argument is a formula
 269  373 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
 270  373 checkFormula(list.getElement(1));
 271   
 272  368 setLocationWithinModule(listContext);
 273    // check if subject variable is not already bound in formula
 274  368 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
 275    list.getElement(0))) {
 276  11 throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 277    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
 278    getCurrentContext());
 279    }
 280  357 if (list.size() > 3) {
 281  0 throw new FormulaCheckException(EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED,
 282    EXACTLY_TWO_OR_THREE_ARGUMENTS_EXPECTED_TEXT, list,
 283    getCurrentContext());
 284    }
 285  357 if (list.size() > 2) {
 286    // check if third argument is a formula
 287  47 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
 288  47 checkFormula(list.getElement(2));
 289   
 290    // check if subject variable is not bound in formula
 291  45 setLocationWithinModule(listContext);
 292  45 if (FormulaChecker.getBoundSubjectVariables(list.getElement(2)).contains(
 293    list.getElement(0))) {
 294  3 throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 295    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(2),
 296    getCurrentContext());
 297    }
 298  42 setLocationWithinModule(listContext);
 299  42 checkFreeAndBoundDisjunct(1, list);
 300    }
 301    // restore context
 302  340 setLocationWithinModule(context);
 303  340 Trace.end(this, method);
 304    }
 305   
 306    /**
 307    * Is {@link Element} a term?
 308    *
 309    * @param element Check this element.
 310    * @throws LogicalCheckException It is no term.
 311    */
 312  4704 private void checkTerm(final Element element) throws LogicalCheckException {
 313  4704 final String method = "checkTerm";
 314  4704 Trace.begin(this, method);
 315  4704 Trace.param(this, method, "element", element);
 316    // save current context
 317  4704 final String context = getCurrentContext().getLocationWithinModule();
 318  4704 Trace.param(this, method, "context", context);
 319  4704 checkList(element);
 320  4700 final ElementList list = element.getList();
 321  4700 final String listContext = context + ".getList()";
 322  4700 setLocationWithinModule(listContext);
 323  4700 final String operator = list.getOperator();
 324  4700 if (operator.equals(SUBJECT_VARIABLE)) {
 325  3241 checkSubjectVariable(element);
 326  1459 } else if (operator.equals(FUNCTION_CONSTANT)
 327    || operator.equals(FUNCTION_VARIABLE)) {
 328   
 329    // function constants must have at least a function name
 330  1236 if (operator.equals(FUNCTION_CONSTANT) && list.size() < 1) {
 331  1 throw new TermCheckException(AT_LEAST_ONE_ARGUMENT_EXPECTED,
 332    AT_LEAST_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
 333    }
 334   
 335    // function variables must have at least a function name and at least one argument
 336  1235 if (operator.equals(FUNCTION_VARIABLE) && list.size() < 2) {
 337  2 throw new TermCheckException(MORE_THAN_ONE_ARGUMENT_EXPECTED,
 338    MORE_THAN_ONE_ARGUMENT_EXPECTED_TEXT, element, getCurrentContext());
 339    }
 340   
 341    // check if first argument is an atom
 342  1233 setLocationWithinModule(listContext + ".getElement(0)");
 343  1233 checkAtomFirst(list.getElement(0));
 344   
 345    // check if all arguments are terms
 346  1226 setLocationWithinModule(listContext);
 347  1226 for (int i = 1; i < list.size(); i++) {
 348  1449 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 349  1449 checkTerm(list.getElement(i));
 350    }
 351   
 352  1225 setLocationWithinModule(listContext);
 353  1225 checkFreeAndBoundDisjunct(1, list);
 354   
 355    // check if function is known
 356  1221 setLocationWithinModule(listContext);
 357  1221 if (FUNCTION_CONSTANT.equals(operator) && !existenceChecker.functionExists(
 358    list.getElement(0).getAtom().getString(), list.size() - 1)) {
 359  2 throw new FormulaCheckException(UNKNOWN_FUNCTION_CONSTANT,
 360    UNKNOWN_FUNCTION_CONSTANT_TEXT + "\""
 361    + list.getElement(0).getAtom().getString() + "\"", element,
 362    getCurrentContext());
 363    }
 364   
 365  223 } else if (operator.equals(CLASS)) {
 366   
 367  212 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  210 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 373  210 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  209 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
 380  209 checkFormula(list.getElement(1));
 381   
 382    // check if class operator is allowed
 383  209 setLocationWithinModule(listContext);
 384  209 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  207 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 391  207 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  4663 setLocationWithinModule(context);
 405  4663 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 LogicalCheckException At least one variable occurs free and bound in different
 415    * sub-elements.
 416    */
 417  5359 private void checkFreeAndBoundDisjunct(final int start,
 418    final ElementList list) throws LogicalCheckException {
 419    // save current context
 420  5359 final String context = getCurrentContext().getLocationWithinModule();
 421  5359 final ElementSet free = new ElementSet();
 422  5359 final ElementSet bound = new ElementSet();
 423  5359 for (int i = start; i < list.size(); i++) {
 424  7917 setLocationWithinModule(context + ".getElement(" + i + ")");
 425  7917 final ElementSet newFree
 426    = getFreeSubjectVariables(list.getElement(i));
 427  7917 final ElementSet newBound
 428    = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
 429  7917 final ElementSet interBound = newFree.newIntersection(bound);
 430  7917 if (!interBound.isEmpty()) {
 431  21 throw new FormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
 432    FREE_VARIABLE_ALREADY_BOUND_TEXT
 433    + interBound, list.getElement(i), getCurrentContext());
 434    }
 435  7896 final ElementSet interFree = newBound.newIntersection(free);
 436  7896 if (!interFree.isEmpty()) {
 437  18 throw new FormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
 438    BOUND_VARIABLE_ALREADY_FREE_TEXT
 439    + interFree, list.getElement(i), getCurrentContext());
 440    }
 441  7878 bound.union(newBound);
 442  7878