Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Mai 10 2007 03:16:40 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  800 private FormulaChecker(final ModuleContext context,
 67    final ExistenceChecker existenceChecker) {
 68  800 this.existenceChecker = existenceChecker;
 69  800 if (existenceChecker.equalityOperatorExists()
 70    && !existenceChecker.predicateExists(existenceChecker.getEqualityOperator(), 2)) {
 71  0 throw new IllegalArgumentException("equality predicate should exist, but it doesn't");
 72    }
 73  800 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  641 public static final void checkFormula(final Element element, final ModuleContext context,
 97    final ExistenceChecker existenceChecker) throws LogicalCheckException {
 98  641 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 99  641 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  159 public static final void checkTerm(final Element element, final ModuleContext context,
 123    final ExistenceChecker existenceChecker) throws LogicalCheckException {
 124  159 final FormulaChecker checker = new FormulaChecker(context, existenceChecker);
 125  159 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  4821 private final void checkFormula(final Element element)
 135    throws LogicalCheckException {
 136  4821 final String method = "checkFormula";
 137  4821 Trace.begin(this, method);
 138  4821 Trace.param(this, method, "element", element);
 139  4821 final String context = getCurrentContext().getLocationWithinModule();
 140  4821 Trace.param(this, method, "context", context);
 141  4821 checkList(element);
 142  4814 final ElementList list = element.getList();
 143  4814 final String listContext = context + ".getList()";
 144  4814 setLocationWithinModule(listContext);
 145  4814 final String operator = list.getOperator();
 146  4814 if (operator.equals(CONJUNCTION_OPERATOR)
 147    || operator.equals(DISJUNCTION_OPERATOR)
 148    || operator.equals(IMPLICATION_OPERATOR)
 149    || operator.equals(EQUIVALENCE_OPERATOR)) {
 150  1475 Trace.trace(this, method, "one of (and, or, implication, equivalence) operator found");
 151  1475 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  1466 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  1465 for (int i = 0; i < list.size(); i++) {
 162  3355 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 163  3355 checkFormula(list.getElement(i));
 164    }
 165  1459 setLocationWithinModule(listContext);
 166  1459 checkFreeAndBoundDisjunct(0, list);
 167  3339 } else if (operator.equals(NEGATION_OPERATOR)) {
 168  146 Trace.trace(this, method, "negation operator found");
 169  146 setLocationWithinModule(listContext);
 170  146 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  144 setLocationWithinModule(listContext + ".getElement(0)");
 176  144 checkFormula(list.getElement(0));
 177  3193 } else if (operator.equals(PREDICATE_VARIABLE)
 178    || operator.equals(PREDICATE_CONSTANT)) {
 179  2791 Trace.trace(this, method, "predicate operator found");
 180  2791 setLocationWithinModule(listContext);
 181  2791 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  2789 setLocationWithinModule(listContext + ".getElement(0)");
 188  2789 checkAtomFirst(list.getElement(0));
 189   
 190    // check if rest arguments are terms
 191  2781 for (int i = 1; i < list.size(); i++) {
 192  3598 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 193  3598 checkTerm(list.getElement(i));
 194    }
 195   
 196  2779 setLocationWithinModule(listContext);
 197  2779 checkFreeAndBoundDisjunct(1, list);
 198   
 199    // check if predicate is known
 200  2775 if (PREDICATE_CONSTANT.equals(operator) && !existenceChecker.predicateExists(
 201    list.getElement(0).getAtom().getString(), list.size() - 1)) {
 202  3 throw new FormulaCheckException(UNKNOWN_PREDICATE_CONSTANT,
 203    UNKNOWN_PREDICATE_CONSTANT_TEXT + "\""
 204    + list.getElement(0).getAtom().getString() + "\"", element,
 205    getCurrentContext());
 206    }
 207   
 208  402 } else if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 209    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 210    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 211  397 Trace.trace(this, method, "quantifier found");
 212  397 setLocationWithinModule(context);
 213  397 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  4724 setLocationWithinModule(context);
 222  4724 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  397 private void checkQuantifier(final Element element) throws LogicalCheckException {
 234  397 final String method = "checkQuantifier";
 235  397 Trace.begin(this, method);
 236  397 Trace.param(this, method, "element", element);
 237    // save context
 238  397 final String context = getCurrentContext().getLocationWithinModule();
 239  397 Trace.param(this, method, "context", context);
 240  397 checkList(element);
 241  397 final ElementList list = element.getList();
 242  397 final String listContext = context + ".getList()";
 243  397 setLocationWithinModule(listContext);
 244  397 final String operator = list.getOperator();
 245  397 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  397 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  397 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  397 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 266  397 checkSubjectVariable(list.getElement(0));
 267   
 268    // check if second argument is a formula
 269  394 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
 270  394 checkFormula(list.getElement(1));
 271   
 272  389 setLocationWithinModule(listContext);
 273    // check if subject variable is not already bound in formula
 274  389 if (FormulaChecker.getBoundSubjectVariables(list.getElement(1)).contains(
 275    list.getElement(0))) {
 276  9 throw new FormulaCheckException(SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA,
 277    SUBJECT_VARIABLE_ALREADY_BOUND_IN_FORMULA_TEXT, list.getElement(1),
 278    getCurrentContext());
 279    }
 280  380 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  380 if (list.size() > 2) {
 286    // check if third argument is a formula
 287  46 setLocationWithinModule(listContext + ".getElement(" + 2 + ")");
 288  46 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  364 setLocationWithinModule(context);
 303  364 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  5489 private void checkTerm(final Element element) throws LogicalCheckException {
 313  5489 final String method = "checkTerm";
 314  5489 Trace.begin(this, method);
 315  5489 Trace.param(this, method, "element", element);
 316    // save current context
 317  5489 final String context = getCurrentContext().getLocationWithinModule();
 318  5489 Trace.param(this, method, "context", context);
 319  5489 checkList(element);
 320  5485 final ElementList list = element.getList();
 321  5485 final String listContext = context + ".getList()";
 322  5485 setLocationWithinModule(listContext);
 323  5485 final String operator = list.getOperator();
 324  5485 if (operator.equals(SUBJECT_VARIABLE)) {
 325  3754 checkSubjectVariable(element);
 326  1731 } else if (operator.equals(FUNCTION_CONSTANT)
 327    || operator.equals(FUNCTION_VARIABLE)) {
 328   
 329    // function constants must have at least a function name
 330  1476 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  1475 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  1473 setLocationWithinModule(listContext + ".getElement(0)");
 343  1473 checkAtomFirst(list.getElement(0));
 344   
 345    // check if all arguments are terms
 346  1466 setLocationWithinModule(listContext);
 347  1466 for (int i = 1; i < list.size(); i++) {
 348  1732 setLocationWithinModule(listContext + ".getElement(" + i + ")");
 349  1732 checkTerm(list.getElement(i));
 350    }
 351   
 352  1465 setLocationWithinModule(listContext);
 353  1465 checkFreeAndBoundDisjunct(1, list);
 354   
 355    // check if function is known
 356  1461 setLocationWithinModule(listContext);
 357  1461 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  255 } else if (operator.equals(CLASS)) {
 366   
 367  244 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  242 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 373  242 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  241 setLocationWithinModule(listContext + ".getElement(" + 1 + ")");
 380  241 checkFormula(list.getElement(1));
 381   
 382    // check if class operator is allowed
 383  241 setLocationWithinModule(listContext);
 384  241 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  239 setLocationWithinModule(listContext + ".getElement(" + 0 + ")");
 391  239 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  5448 setLocationWithinModule(context);
 405  5448 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  5745 private void checkFreeAndBoundDisjunct(final int start,
 418    final ElementList list) throws LogicalCheckException {
 419    // save current context
 420  5745 final String context = getCurrentContext().getLocationWithinModule();
 421  5745 final ElementSet free = new ElementSet();
 422  5745 final ElementSet bound = new ElementSet();
 423  5745 for (int i = start; i < list.size(); i++) {
 424  8755 setLocationWithinModule(context + ".getElement(" + i + ")");
 425  8755 final ElementSet newFree
 426    = getFreeSubjectVariables(list.getElement(i));
 427  8755 final ElementSet newBound
 428    = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
 429  8755 final ElementSet interBound = newFree.newIntersection(bound);
 430  8755 if (!interBound.isEmpty()) {
 431  19 throw new FormulaCheckException(FREE_VARIABLE_ALREADY_BOUND,
 432    FREE_VARIABLE_ALREADY_BOUND_TEXT
 433    + interBound, list.getElement(i), getCurrentContext());
 434    }
 435  8736 final ElementSet interFree = newBound.newIntersection(free);
 436  8736 if (!interFree.isEmpty()) {
 437  16 throw new FormulaCheckException(BOUND_VARIABLE_ALREADY_FREE,
 438    BOUND_VARIABLE_ALREADY_FREE_TEXT
 439    + interFree, list.getElement(i), getCurrentContext());
 440    }
 441  8720 bound.union(newBound);
 442  8720 free.union(newFree);
 443    }
 444    // restore context
 445  5710 setLocationWithinModule(context);
 446    }
 447   
 448   
 449    /**
 450    * Is {@link Element} a subject variable?
 451    *
 452    * @param element Element to look onto.
 453    * @return Is it a subject variable?
 454    */
 455  32000 private final boolean isSubjectVariable(final Element element) {
 456  32000 if (element == null || !element.isList() || element.getList() == null) {
 457  8860 return false;
 458    }
 459  23140 final ElementList list = element.getList();
 460  23140 if (list.getOperator().equals(SUBJECT_VARIABLE)) {
 461  11896 if (list.size() != 1) {
 462  0 return false;
 463    }
 464  11896 final Element first = element.getList().getElement(0);
 465  11896 if (first == null || !first.isAtom() || first.getAtom() == null) {
 466  0 return false;
 467    }
 468  11896 final Atom atom = first.getAtom();
 469  11896 if (atom.getString() == null || atom.getAtom().getString() == null
 470    || atom.getString().length() == 0) {
 471  0 return false;
 472    }
 473    } else {
 474  11244 return false;
 475    }
 476  11896 return true;
 477    }
 478   
 479   
 480    /**
 481    * Check if {@link Element} is a subject variable.
 482    *
 483    * @param element Check this element.
 484    * @throws LogicalCheckException It is no subject variable.
 485    */
 486  4151 private final void checkSubjectVariable(final Element element)
 487    throws LogicalCheckException {
 488    // save current context
 489  4151 final String context = getCurrentContext().getLocationWithinModule();
 490  4151 checkList(element);
 491  4151 setLocationWithinModule(context + ".getList()");
 492  4151 if (element.getList().getOperator().equals(SUBJECT_VARIABLE)) {
 493  4148 if (element.getList().size() != 1) {
 494  2 throw new FormulaCheckException(EXACTLY_ONE_ARGUMENT_EXPECTED,
 495    EXACTLY_ONE_ARGUMENT_EXPECTED_TEXT, element.getList(), getCurrentContext());
 496    }
 497    // check if first argument is an atom
 498  4146 setLocationWithinModule(context + ".getList().getElement(0)");
 499  4146 checkAtomFirst(element.getList().getElement(0));
 500    } else {
 501  3 setLocationWithinModule(context + ".getList().getOperator()");
 502  3 throw new FormulaCheckException(SUBJECT_VARIABLE_EXPECTED,
 503    SUBJECT_VARIABLE_EXPECTED_TEXT, element, getCurrentContext());
 504    }
 505    // restore context
 506  4145 setLocationWithinModule(context);
 507    }
 508   
 509   
 510    /**
 511    * Return all free subject variables of an element.
 512    *
 513    * @param element Work on this element.
 514    * @return All free subject variables.
 515    */
 516  31758 private final ElementSet getFreeSubjectVariables(final Element element) {
 517  31758 final ElementSet free = new ElementSet();
 518  31758 if (isSubjectVariable(element)) {
 519  11655 free.add(element);
 520  20103 } else if (element.isList()) {
 521  11243 final ElementList list = element.getList();
 522  11243 final String operator = list.getOperator();
 523  11243 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 524    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 525    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
 526    || operator.equals(CLASS)) {
 527  652 for (int i = 1; i < list.size(); i++) {
 528  672 free.union(getFreeSubjectVariables(list.getElement(i)));
 529    }
 530  652 free.remove(list.getElement(0));
 531    } else {
 532  10591 for (int i = 0; i < list.size(); i++) {
 533  22331 free.union(getFreeSubjectVariables(list.getElement(i)));
 534    }
 535    }
 536    }
 537  31758 return free;
 538    }
 539   
 540    /**
 541    * Return all bound subject variables of an element.
 542    *
 543    * @param element Work on this element.
 544    * @return All bound subject variables.
 545    */
 546  50303 public static final ElementSet getBoundSubjectVariables(final Element element) {
 547  50303 final ElementSet bound = new ElementSet();
 548  50303 if (element.isList()) {
 549  26638 ElementList list = element.getList();
 550  26638 final String operator = list.getOperator();
 551    // if operator is quantifier or class term
 552  26638 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 553    || operator.equals(UNIQUE_EXISTENTIAL_QUANTIFIER_OPERATOR)
 554    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)
 555    || operator.equals(CLASS)) {
 556    // add subject variable to bound list
 557  855 bound.add(list.getElement(0));
 558    // add all bound variables of sub-elements
 559  855 for (int i = 1; i < list.size(); i++) {
 560  882 bound.union(FormulaChecker.getBoundSubjectVariables(
 561    list.getElement(i)));
 562    }
 563    } else {
 564    // add all bound variables of sub-elements
 565  25783 for (int i = 0; i < list.size(); i++) {
 566  39993 bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i)));
 567    }
 568    }
 569    }
 570  50303 return bound;
 571    }
 572   
 573    /**
 574    * Check common requirements for list elements that are checked for being a term or formula.
 575    *
 576    * @param element List element.
 577    * @throws ElementCheckException Requirements not fulfilled.
 578    */
 579  14858 private void checkList(final Element element) throws ElementCheckException {
 580    // save current context
 581  14858 final String context = getCurrentContext().getLocationWithinModule();
 582  14858 if (element == null) {
 583  2 throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
 584    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
 585    }
 586  14856 if (!element.isList()) {
 587  2 throw new ElementCheckException(LIST_EXPECTED,
 588    LIST_EXPECTED_TEXT, element, getCurrentContext());
 589    }
 590  14854 final ElementList list = element.getList();
 591  14854 setLocationWithinModule(context + ".getList()");
 592  14854 if (list == null) {
 593  2 throw new ElementCheckException(LIST_MUST_NOT_BE_NULL,
 594    LIST_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 595    }
 596  14852 final String operator = list.getOperator();
 597  14852 setLocationWithinModule(context + ".getList().getOperator()");
 598  14852 if (operator == null) {
 599  2 throw new ElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_NULL,
 600    OPERATOR_CONTENT_MUST_NOT_BE_NULL_TEXT + "\""
 601    + operator + "\"", element, getCurrentContext());
 602    }
 603  14850 if (operator.length() == 0) {
 604  3 throw new ElementCheckException(OPERATOR_CONTENT_MUST_NOT_BE_EMPTY,
 605    OPERATOR_CONTENT_MUST_NOT_BE_EMPTY_TEXT + "\""
 606    + operator + "\"", element, getCurrentContext());
 607    }
 608    // restore context
 609  14847 setLocationWithinModule(context);
 610    }
 611   
 612    /**
 613    * Check if element is an atom and has valid content. It is assumed, that this element is the
 614    * first of a list.
 615    *
 616    * @param element Check this for an atom.
 617    * @throws ElementCheckException No valid content.
 618    */
 619  8408 private void checkAtomFirst(final Element element) throws ElementCheckException {
 620    // save current context
 621  8408 final String context = getCurrentContext().getLocationWithinModule();
 622  8408 if (element == null) {
 623  0 throw new ElementCheckException(ELEMENT_MUST_NOT_BE_NULL,
 624    ELEMENT_MUST_NOT_BE_NULL_TEXT, null, getCurrentContext());
 625    }
 626  8408 if (!element.isAtom()) { // TODO mime 20061126: this is special?
 627  9 throw new ElementCheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM,
 628    FIRST_ARGUMENT_MUST_BE_AN_ATOM_TEXT, element, getCurrentContext());
 629    }
 630  8399 final Atom atom = element.getAtom();
 631  8399 setLocationWithinModule(context + ".getAtom()");
 632  8399 if (atom == null) {
 633  2 throw new ElementCheckException(ATOM_MUST_NOT_BE_NULL,
 634    ATOM_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 635    }
 636  8397 if (atom.getString() == null) {
 637  2 throw new ElementCheckException(ATOM_CONTENT_MUST_NOT_BE_NULL,
 638    ATOM_CONTENT_MUST_NOT_BE_NULL_TEXT, element, getCurrentContext());
 639    }
 640  8395 if (atom.getString().length() == 0) {
 641  3 throw new ElementCheckException(ATOM_CONTENT_MUST_NOT_BE_EMPTY,
 642    ATOM_CONTENT_MUST_NOT_BE_EMPTY_TEXT, element, getCurrentContext());
 643    }
 644    // restore context
 645  8392 setLocationWithinModule(context);
 646    }
 647   
 648    /**
 649    * Set location information where are we within the original module.
 650    *
 651    * @param locationWithinModule Location within module.
 652    */
 653  136833 protected void setLocationWithinModule(final String locationWithinModule) {
 654  136833 getCurrentContext().setLocationWithinModule(locationWithinModule);
 655    }
 656   
 657    /**
 658    * Get current context within original.
 659    *
 660    * @return Current context.
 661    */
 662  180825 protected final ModuleContext getCurrentContext() {
 663  180825 return currentContext;
 664    }
 665   
 666    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Do Mai 10 2007 04:02:49 CEST.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.