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(free);
 443  12494 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  12476 bound.union(newBound);
 449  12476 free.union(newFree);
 450    }
 451    // restore context
 452  8791 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  47592 private final boolean isSubjectVariable(final Element element) {
 463  47592 if (element == null || !element.isList() || element.getList() == null) {
 464  13677 return false;
 465    }
 466  33915 final ElementList list = element.getList();
 467  33915 if (list.getOperator().equals(SUBJECT_VARIABLE)) {
 468  14672 if (list.size() != 1) {
 469  0 return false;
 470    }
 471  14672 final Element first = element.getList().getElement(0);
 472  14672 if (first == null || !first.isAtom() || first.getAtom() == null) {
 473  0 return false;
 474    }
 475  14672 final Atom atom = first.getAtom();
 476  14672 if (atom.getString() == null || atom.getAtom().getString() == null
 477    || atom.getString().length() == 0) {
 478  0 return false;
 479    }
 480    } else {
 481  19243 return false;
 482    }
 483  14672 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  5501 private final void checkSubjectVariable(final Element element)
 494    throws LogicalCheckException {
 495    // save current context
 496  5501 final String context = getCurrentContext().getLocationWithinModule();
 497  5501 checkList(element);
 498  5501 setLocationWithinModule(context + ".getList()");
 499  5501 if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
 500  5498 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  5496 setLocationWithinModule(context + ".getList().getElement(0)");
 506  5496 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  5495 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  47350 private final ElementSet getFreeSubjectVariables(final Element element) {
 524  47350 final ElementSet free = new ElementSet();
 525  47350 if (isSubjectVariable(element)) {
 526  14431 free.add(element);
 527  32919 } else if (element.isList()) {
 528  19242 final ElementList list = element.getList();
 529  19242 final String operator = list.getOperator();
 530  19242 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  1625 for (int i = 1; i < list.size(); i++) {
 535  1664 free.union(getFreeSubjectVariables(list.getElement(i)));
 536    }
 537  1625 free.remove(list.getElement(0));
 538    } else {
 539  17617 for (int i = 0; i < list.size(); i++) {
 540  33168 free.union(getFreeSubjectVariables(list.getElement(i)));
 541    }
 542    }
 543    }
 544  47350 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  71941 public static final ElementSet getBoundSubjectVariables(final Element element) {
 554  71941 final ElementSet bound = new ElementSet();
 555  71941 if (element.isList()) {
 556  39184 ElementList list = element.getList();
 557  39184 final String operator = list.getOperator();
 558    // if operator is quantifier or class term
 559  39184 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  1898 bound.add(list.getElement(0));
 565    // add all bound variables of sub-elements
 566  1898 for (int i = 1; i < list.size(); i++) {
 567  1952 bound.union(FormulaChecker.getBoundSubjectVariables(
 568    list.getElement(i)));
 569    }
 570    } else {
 571    // add all bound variables of sub-elements
 572  37286 for (int i = 0; i < list.size(); i++) {
 573  56315 bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i)));
 574    }
 575    }
 576    }
 577  71941 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  21252 private void checkList(final Element element) throws ElementCheckException {
 587    // save current context
 588  21252 final String context = getCurrentContext().getLocationWithinModule();
 589  21252 if (element == null) {
 590  2 throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
 591    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
 592    }
 593  21250 if (!element.isList()) {
 594  2 throw new ElementCheckException(LIST_EXPECTED,
 595    LIST_EXPECTED_TEXT, element, getCurrentContext());
 596    }
 597  21248 final ElementList list = element.getList();
 598  21248 setLocationWithinModule(context + ".getList()");
 599  21248 if (list == null) {
 600  2 throw new ElementCheckException(LIST_MUST_NOT_BE_NULL,
 601    LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 602    }
 603  21246 final String operator = list.getOperator();
 604  21246 setLocationWithinModule(context + ".getList().getOperator()");
 605  21246 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  21244 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  21241 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  11568 private void checkAtomFirst(final Element element) throws ElementCheckException {
 627    // save current context
 628  11568 final String context = getCurrentContext().getLocationWithinModule();
 629  11568 if (element == null) {
 630  0 throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
 631    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
 632    }
 633  11568 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  11559 final Atom atom = element.getAtom();
 638  11559 setLocationWithinModule(context + ".getAtom()");
 639  11559 if (atom == null) {
 640  2 throw new ElementCheckException(ATOM_MUST_NOT_BE_NULL,
 641    ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 642    }
 643  11557 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  11555 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  11552 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  195947 protected void setLocationWithinModule(final String locationWithinModule) {
 661  195947 getCurrentContext().setLocationWithinModule(locationWithinModule);
 662    }
 663   
 664    /**
 665    * Get current context within original.
 666    *
 667    * @return Current context.
 668    */
 669  258990 protected final ModuleContext getCurrentContext() {
 670  258990 return currentContext;
 671    }
 672   
 673    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Sa Jan 26 2008 15:40:52 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.