Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Mrz 27 2008 21:46:26 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.10 2008/03/27 05:16:23 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.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.common.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.10 $
 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  1121 private FormulaChecker(final ModuleContext context,
 70    final ExistenceChecker existenceChecker) {
 71  1121 this.existenceChecker = existenceChecker;
 72  1121 if (existenceChecker.equalityOperatorExists()
 73    && !existenceChecker.predicateExists(existenceChecker.getIdentityOperator(), 2)) {
 74  0 throw new IllegalArgumentException("equality predicate should exist, but it doesn't");
 75    }
 76  1121 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  962 public static final void checkFormula(final Element element, final ModuleContext context,
 88    final ExistenceChecker existenceChecker) throws LogicalCheckException {
 89  962 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 90  962 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  10639 private final void checkFormula(final Element element)
 141    throws LogicalCheckException {
 142  10639 final String method = "checkFormula";
 143  10639 Trace.begin(CLASS, this, method);
 144  10639 Trace.param(CLASS, this, method, "element", element);
 145  10639 final String context = getCurrentContext().getLocationWithinModule();
 146  10639 Trace.param(CLASS, this, method, "context", context);
 147  10639 checkList(element);
 148  10632 final ElementList list = element.getList();
 149  10632 final String listContext = context + ".getList()";
 150  10632 setLocationWithinModule(listContext);
 151  10632 final String operator = list.getOperator();
 152  10632 if (operator.equals(CONJUNCTION_OPERATOR)
 153    || operator.equals(DISJUNCTION_OPERATOR)
 154    || operator.equals(IMPLICATION_OPERATOR)
 155    || operator.equals(EQUIVALENCE_OPERATOR)) {
 156  3499 Trace.trace(CLASS, this, method,
 157    "one of (and, or, implication, equivalence) operator found");
 158  3499 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  3490 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  3489 for (int i = 0; i < list.size(); i++) {
 169  7880 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 170  7880 checkFormula(list.getElement(i));
 171    }
 172  3475 setLocationWithinModule(listContext);
 173  3475 checkFreeAndBoundDisjunct(0, list);
 174  7133 } else if (operator.equals(NEGATION_OPERATOR)) {
 175  399 Trace.trace(CLASS, this, method, "negation operator found");
 176  399 setLocationWithinModule(listContext);
 177  399 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  397 setLocationWithinModule(listContext + ".getElement(0)");
 183  397 checkFormula(list.getElement(0));
 184  6734 } else if (operator.equals(PREDICATE_VARIABLE)
 185    || operator.equals(PREDICATE_CONSTANT)) {
 186  5649 Trace.trace(CLASS, this, method, "predicate operator found");
 187  5649 setLocationWithinModule(listContext);
 188  5649 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  5647 setLocationWithinModule(listContext + ".getElement(0)");
 195  5647 checkAtomFirst(list.getElement(0));
 196   
 197    // check if rest arguments are terms
 198  5639 for (int i = 1; i < list.size(); i++) {
 199  4949 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 200  4949 checkTerm(list.getElement(i));
 201    }
 202   
 203  5637 setLocationWithinModule(listContext);
 204  5637 checkFreeAndBoundDisjunct(1, list);
 205   
 206    // check if predicate is known
 207  5633 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  1085 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 216    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 217    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 218  1080 Trace.trace(CLASS, this, method, "quantifier found");
 219  1080 setLocationWithinModule(context);
 220  1080 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  10516 setLocationWithinModule(context);
 229  10516 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  1080 private void checkQuantifier(final Element element) throws LogicalCheckException {
 241  1080 final String method = "checkQuantifier";
 242  1080 Trace.begin(CLASS, this, method);
 243  1080 Trace.param(CLASS, this, method, "element", element);
 244    // save context
 245  1080 final String context = getCurrentContext().getLocationWithinModule();
 246  1080 Trace.param(CLASS, this, method, "context", context);
 247  1080 checkList(element);
 248  1080 final ElementList list = element.getList();
 249  1080 final String listContext = context + ".getList()";
 250  1080 setLocationWithinModule(listContext);
 251  1080 final String operator = list.getOperator();
 252  1080 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  1080 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  1080 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  1080 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 273  1080 checkSubjectVariable(list.getElement(0));
 274   
 275    // check if second argument is a formula
 276  1077 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
 277  1077 checkFormula(list.getElement(1));
 278   
 279  1072 setLocationWithinModule(listContext);
 280    // check if subject variable is not already bound in formula
 281  1072 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  1058 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  1058 if (list.size() > 2) {
 293    // check if third argument is a formula
 294  82 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
 295  82 checkFormula(list.getElement(2));
 296   
 297    // check if subject variable is not bound in formula
 298  78 setLocationWithinModule(listContext);
 299  78 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  75 setLocationWithinModule(listContext);
 306  75 checkFreeAndBoundDisjunct(1, list);
 307    }
 308    // restore context
 309  1039 setLocationWithinModule(context);
 310  1039 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  6866 private void checkTerm(final Element element) throws LogicalCheckException {
 320  6866 final String method = "checkTerm";
 321  6866 Trace.begin(CLASS, this, method);
 322  6866 Trace.param(CLASS, this, method, "element", element);
 323    // save current context
 324  6866 final String context = getCurrentContext().getLocationWithinModule();
 325  6866 Trace.param(CLASS, this, method, "context", context);
 326  6866 checkList(element);
 327  6862 final ElementList list = element.getList();
 328  6862 final String listContext = context + ".getList()";
 329  6862 setLocationWithinModule(listContext);
 330  6862 final String operator = list.getOperator();
 331  6862 if (operator.equals(SUBJECT_VARIABLE)) {
 332  5105 checkSubjectVariable(element);
 333  1757 } else if (operator.equals(FUNCTION_CONSTANT)
 334    || operator.equals(FUNCTION_VARIABLE)) {
 335   
 336    // function constants must have at least a function name
 337  1502 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  1501 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  1499 setLocationWithinModule(listContext + ".getElement(0)");
 350  1499 checkAtomFirst(list.getElement(0));
 351   
 352    // check if all arguments are terms
 353  1492 setLocationWithinModule(listContext);
 354  1492 for (int i = 1; i < list.size(); i++) {
 355  1758 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 356  1758 checkTerm(list.getElement(i));
 357    }
 358   
 359  1491 setLocationWithinModule(listContext);
 360  1491 checkFreeAndBoundDisjunct(1, list);
 361   
 362    // check if function is known
 363  1487 setLocationWithinModule(listContext);
 364  1487 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  6825 setLocationWithinModule(context);
 412  6825 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  10678 private void checkFreeAndBoundDisjunct(final int start,
 425    final ElementList list) throws LogicalCheckException {
 426    // save current context
 427  10678 final String context = getCurrentContext().getLocationWithinModule();
 428  10678 final ElementSet free = new ElementSet();
 429  10678 final ElementSet bound = new ElementSet();
 430  10678 for (int i = start; i < list.size(); i++) {
 431  14713 setLocationWithinModule(context + ".getElement(" + i + ")");
 432  14713 final ElementSet newFree
 433    = getFreeSubjectVariables(list.getElement(i));
 434  14713 final ElementSet newBound
 435    = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
 436  14713 final ElementSet interBound = newFree.newIntersection(bound);
 437  14713 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  14689 final ElementSet interFree = newBound.newIntersection(free);
 443  14689 if (!interFree.isEmpty()) {
 444  18 throw new FormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
 445    BOUND_VARIABLE_ALREADY_FREE_TEXT
 446    + interFree, list.getElement(i), getCurrentContext());
 447    }
 448  14671 bound.union(newBound);
 449  14671 free.union(newFree);
 450    }
 451    // restore context
 452  10636 setLocationWithinModule(context);
 453    }
 454   
 455   
 456    /**
 457    * Is {@link Element} a subject variable?
 458    *
 459    * @param element Element to look onto.
 460    * @return Is it a subject variable?
 461    */
 462  56734 private final boolean isSubjectVariable(final Element element) {
 463  56734 if (element == null || !element.isList() || element.getList() == null) {
 464  16590 return false;
 465    }
 466  40144 final ElementList list = element.getList();
 467  40144 if (list.getOperator().equals(SUBJECT_VARIABLE)) {
 468  16145 if (list.size() != 1) {
 469  0 return false;
 470    }
 471  16145 final Element first = element.getList().getElement(0);
 472  16145 if (first == null || !first.isAtom() || first.getAtom() == null) {
 473  0 return false;
 474    }
 475  16145 final Atom atom = first.getAtom();
 476  16145 if (atom.getString() == null || atom.getAtom().getString() == null
 477    || atom.getString().length() == 0) {
 478  0 return false;
 479    }
 480    } else {
 481  23999 return false;
 482    }
 483  16145 return true;
 484    }
 485   
 486   
 487    /**
 488    * Check if {@link Element} is a subject variable.
 489    *
 490    * @param element Check this element.
 491    * @throws LogicalCheckException It is no subject variable.
 492    */
 493  6185 private final void checkSubjectVariable(final Element element)
 494    throws LogicalCheckException {
 495    // save current context
 496  6185 final String context = getCurrentContext().getLocationWithinModule();
 497  6185 checkList(element);
 498  6185 setLocationWithinModule(context + ".getList()");
 499  6185 if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
 500  6182 if (element.getList().size() != 1) {
 501  2 throw new FormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
 502    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext());
 503    }
 504    // check if first argument is an atom
 505  6180 setLocationWithinModule(context + ".getList().getElement(0)");
 506  6180 checkAtomFirst(element.getList().getElement(0));
 507    } else {
 508  3 setLocationWithinModule(context + ".getList().getOperator()");
 509  3 throw new FormulaCheckException(SUBJECT_VARIABLE_EXPECTED,
 510    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
 511    }
 512    // restore context
 513  6179 setLocationWithinModule(context);
 514    }
 515   
 516   
 517    /**
 518    * Return all free subject variables of an element.
 519    *
 520    * @param element Work on this element.
 521    * @return All free subject variables.
 522    */
 523  56492 private final ElementSet getFreeSubjectVariables(final Element element) {
 524  56492 final ElementSet free = new ElementSet();
 525  56492 if (isSubjectVariable(element)) {
 526  15904 free.add(element);
 527  40588 } else if (element.isList()) {
 528  23998 final ElementList list = element.getList();
 529  23998 final String operator = list.getOperator();
 530  23998 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 531    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 532    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
 533    || operator.equals(CLASS_OP)) {
 534  2103 for (int i = 1; i < list.size(); i++) {
 535  2156 free.union(getFreeSubjectVariables(list.getElement(i)));
 536    }
 537  2103 free.remove(list.getElement(0));
 538    } else {
 539  21895 for (int i = 0; i < list.size(); i++) {
 540  39623 free.union(getFreeSubjectVariables(list.getElement(i)));
 541    }
 542    }
 543    }
 544  56492 return free;
 545    }
 546   
 547    /**
 548    * Return all bound subject variables of an element.
 549    *
 550    * @param element Work on this element.
 551    * @return All bound subject variables.
 552    */
 553  84078 public static final ElementSet getBoundSubjectVariables(final Element element) {
 554  84078 final ElementSet bound = new ElementSet();
 555  84078 if (element.isList()) {
 556  46231 ElementList list = element.getList();
 557  46231 final String operator = list.getOperator();
 558    // if operator is quantifier or class term
 559  46231 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 560    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 561    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
 562    || operator.equals(CLASS_OP)) {
 563    // add subject variable to bound list
 564  2400 bound.add(list.getElement(0));
 565    // add all bound variables of sub-elements
 566  2400 for (int i = 1; i < list.size(); i++) {
 567  2473 bound.union(FormulaChecker.getBoundSubjectVariables(
 568    list.getElement(i)));
 569    }
 570    } else {
 571    // add all bound variables of sub-elements
 572  43831 for (int i = 0; i < list.size(); i++) {
 573  65503 bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i)));
 574    }
 575    }
 576    }
 577  84078 return bound;
 578    }
 579   
 580    /**
 581    * Check common requirements for list elements that are checked for being a term or formula.
 582    *
 583    * @param element List element.
 584    * @throws ElementCheckException Requirements not fulfilled.
 585    */
 586  24770 private void checkList(final Element element) throws ElementCheckException {
 587    // save current context
 588  24770 final String context = getCurrentContext().getLocationWithinModule();
 589  24770 if (element == null) {
 590  2 throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
 591    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
 592    }
 593  24768 if (!element.isList()) {
 594  2 throw new ElementCheckException(LIST_EXPECTED,
 595    LIST_EXPECTED_TEXT, element, getCurrentContext());
 596    }
 597  24766 final ElementList list = element.getList();
 598  24766 setLocationWithinModule(context + ".getList()");
 599  24766 if (list == null) {
 600  2 throw new ElementCheckException(LIST_MUST_NOT_BE_NULL,
 601    LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 602    }
 603  24764 final String operator = list.getOperator();
 604  24764 setLocationWithinModule(context + ".getList().getOperator()");
 605  24764 if (operator == null) {
 606  2 throw new ElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL,
 607    OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT + "\""
 608    + operator + "\"", element, getCurrentContext());
 609    }
 610  24762 if (operator.length() == 0) {
 611  3 throw new ElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY,
 612    OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\""
 613    + operator + "\"", element, getCurrentContext());
 614    }
 615    // restore context
 616  24759 setLocationWithinModule(context);
 617    }
 618   
 619    /**
 620    * Check if element is an atom and has valid content. It is assumed, that this element is the
 621    * first of a list.
 622    *
 623    * @param element Check this for an atom.
 624    * @throws ElementCheckException No valid content.
 625    */
 626  13326 private void checkAtomFirst(final Element element) throws ElementCheckException {
 627    // save current context
 628  13326 final String context = getCurrentContext().getLocationWithinModule();
 629  13326 if (element == null) {
 630  0 throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
 631    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
 632    }
 633  13326 if (!element.isAtom()) { // TODO mime 20061126: this is special?
 634  9 throw new ElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM,
 635    FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext());
 636    }
 637  13317 final Atom atom = element.getAtom();
 638  13317 setLocationWithinModule(context + ".getAtom()");
 639  13317 if (atom == null) {
 640  2 throw new ElementCheckException(ATOM_MUST_NOT_BE_NULL,
 641    ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 642    }
 643  13315 if (atom.getString() == null) {
 644  2 throw new ElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL,
 645    ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 646    }
 647  13313 if (atom.getString().length() == 0) {
 648  3 throw new ElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY,
 649    ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext());
 650    }
 651    // restore context
 652  13310 setLocationWithinModule(context);
 653    }
 654   
 655    /**
 656    * Set location information where are we within the original module.
 657    *
 658    * @param locationWithinModule Location within module.
 659    */
 660  229049 protected void setLocationWithinModule(final String locationWithinModule) {
 661  229049 getCurrentContext().setLocationWithinModule(locationWithinModule);
 662    }
 663   
 664    /**
 665    * Get current context within original.
 666    *
 667    * @return Current context.
 668    */
 669  302731 protected final ModuleContext getCurrentContext() {
 670  302731 return currentContext;
 671    }
 672   
 673    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Do Mrz 27 2008 21:55:30 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.