Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Dez 29 2005 18:38:29 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 283   Methods: 6
NCLOC: 167   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
FormulaChecker.java 0% 0% 0% 0%
coverage
 1    /* $Id: FormulaChecker.java,v 1.3 2005/06/08 21:55:56 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2005, 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   
 21    import org.qedeq.kernel.base.elli.Element;
 22    import org.qedeq.kernel.base.elli.ElementList;
 23    import org.qedeq.kernel.dto.elli.ElementSet;
 24   
 25   
 26    /**
 27    * This class deals with {@link org.qedeq.kernel.base.elli.Element}s which represent a
 28    * formula. It has methods to check those elements for certain criteria.
 29    *
 30    * @version $Revision: 1.3 $
 31    * @author Michael Meyling
 32    */
 33    public final class FormulaChecker {
 34   
 35    /** Operator string for logical "and". */
 36    public static final String CONJUNCTION_OPERATOR = "AND";
 37   
 38    /** Operator string for logical "or". */
 39    public static final String DISJUNCTION_OPERATOR = "OR";
 40   
 41    /** Operator string for logical implication. */
 42    public static final String IMPLICATION_OPERATOR = "IMPL";
 43   
 44    /** Operator string for logical equivalence. */
 45    public static final String EQUIVALENCE_OPERATOR = "EQUI";
 46   
 47    /** Operator string for logical negation. */
 48    public static final String NEGATION_OPERATOR = "NOT";
 49   
 50    /** Operator string for predicate constants. */
 51    public static final String PREDICATE_OPERATOR = "PRED";
 52   
 53    /** Operator string for subject variables. */
 54    public static final String SUBJECT_VARIABLE_OPERATOR = "VAR";
 55   
 56    /** Operator string for proposition variables. */
 57    public static final String PROPOSITION_VARIABLE_OPERATOR = "PROP";
 58   
 59    /** Operator string for predicate variables. */
 60    public static final String PREDICATE_VARIABLE_OPERATOR = "PREDVAR";
 61   
 62    /** Operator string for predicate argument list. */
 63    public static final String LIST_OPERATOR = "L";
 64   
 65    /** Operator string for logical "all" operator. */
 66    public static final String UNIVERSAL_QUANTIFIER_OPERATOR = "FORALL";
 67   
 68    /** Operator string for logical "exists" operator. */
 69    public static final String EXISTENTIAL_QUANTIFIER_OPERATOR = "EXISTS";
 70   
 71    /** Error message: first argument must be an atom. */
 72    private static final String FIRST_ARGUMENT_MUST_BE_AN_ATOM = "first argument must be an atom";
 73   
 74    /** Error message: second argument must be a list. */
 75    private static final String SECOND_ARGUMENT_MUST_BE_A_LIST = "second argument must be a list";
 76   
 77   
 78    /**
 79    * Constructor.
 80    */
 81  0 private FormulaChecker() {
 82    // nothing to do
 83    }
 84   
 85    /**
 86    * Is {@link Element} a formula?
 87    *
 88    * @param element check this element
 89    * @throws CheckException if it is no formula
 90    */
 91  0 public static final void checkFormula(final Element element)
 92    throws CheckException {
 93  0 if (element.isAtom()) {
 94  0 throw new CheckException("an atom is no formula", element);
 95    }
 96  0 final ElementList list = element.getList();
 97  0 final String operator = list.getOperator();
 98  0 if (operator.equals(CONJUNCTION_OPERATOR)
 99    || operator.equals(DISJUNCTION_OPERATOR)
 100    || operator.equals(IMPLICATION_OPERATOR)
 101    || operator.equals(EQUIVALENCE_OPERATOR)) {
 102  0 if (list.size() <= 1) {
 103  0 throw new CheckException(
 104    "more than one argument expected", element);
 105    }
 106    // check if all arguments are formulas and no bound variables
 107    // are free and vice versa
 108  0 final ElementSet free = new ElementSet();
 109  0 final ElementSet bound = new ElementSet();
 110  0 for (int i = 0; i < list.size(); i++) {
 111  0 FormulaChecker.checkFormula(list.getElement(i));
 112  0 final ElementSet newFree
 113    = FormulaChecker.getFreeSubjectVariables(list.getElement(i));
 114  0 final ElementSet newBound
 115    = FormulaChecker.getBoundSubjectVariables(list.getElement(i));
 116  0 if (!newFree.newIntersection(bound).isEmpty()) {
 117  0 throw new CheckException(
 118    "these free variables are already bound in previous formulas: "
 119    + newFree, list.getElement(i));
 120    }
 121  0 if (!newBound.newIntersection(free).isEmpty()) {
 122  0 throw new CheckException(
 123    "these bound variables are already free in previous formulas: "
 124    + newBound, list.getElement(i));
 125    }
 126  0 bound.union(newBound);
 127  0 free.union(newFree);
 128    }
 129  0 } else if (operator.equals(NEGATION_OPERATOR)) {
 130  0 if (list.size() != 1) {
 131  0 throw new CheckException(
 132    "negation requires exactly one argument", element);
 133    }
 134  0 FormulaChecker.checkFormula(list.getElement(0));
 135  0 } else if (operator.equals(PROPOSITION_VARIABLE_OPERATOR)) {
 136    // check if there is exactly one numeric argument
 137  0 if (list.size() != 1) {
 138  0 throw new CheckException("exactly one numeric argument expected",
 139    element);
 140    }
 141    // check if first argument is an atom
 142  0 if (!list.getElement(0).isAtom()) {
 143  0 throw new CheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM, element);
 144    }
 145  0 } else if (operator.equals(PREDICATE_VARIABLE_OPERATOR)) {
 146  0 if (list.size() != 2) {
 147  0 throw new CheckException("exactly two arguments expected",
 148    element);
 149    }
 150    // check if first argument is an atom
 151  0 if (!list.getElement(0).isAtom()) {
 152  0 throw new CheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM, element);
 153    }
 154   
 155    // check if second argument is list of subject variables
 156  0 if (!list.getElement(1).isList()) {
 157  0 throw new CheckException(SECOND_ARGUMENT_MUST_BE_A_LIST, element);
 158    }
 159  0 final ElementList vars = list.getElement(1).getList();
 160  0 if (!vars.getOperator().equals(LIST_OPERATOR)) {
 161  0 throw new CheckException("list operator expected", vars);
 162    }
 163  0 for (int i = 0; i < list.size(); i++) {
 164  0 FormulaChecker.checkSubjectVariable(list.getElement(i));
 165    }
 166   
 167  0 } else if (list.getOperator().equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 168    || list.getOperator().equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 169  0 if (list.size() != 2) {
 170  0 throw new CheckException("exactly two arguments expected",
 171    element);
 172    }
 173    // check if first argument is subject variable
 174  0 FormulaChecker.checkSubjectVariable(list.getElement(0));
 175   
 176    // check if second argument is a formula
 177  0 FormulaChecker.checkFormula(list.getElement(1));
 178   
 179    // check if subject variable is free in formula
 180  0 if (!FormulaChecker.getFreeSubjectVariables(list.getElement(1)).contains(
 181    list.getElement(0))) {
 182  0 throw new CheckException("subject variable not free in formula",
 183    list.getElement(0));
 184    }
 185    } else {
 186  0 throw new CheckException("not a logical operator", element);
 187    }
 188    }
 189   
 190   
 191    /**
 192    * Is {@link Element} an subject variable?
 193    *
 194    * @param element check this element
 195    * @return is is an atomic element
 196    */
 197  0 public static final boolean isSubjectVariable(final Element element) {
 198  0 try {
 199  0 FormulaChecker.checkSubjectVariable(element);
 200    } catch (CheckException e) {
 201  0 return false;
 202    }
 203  0 return true;
 204    }
 205   
 206   
 207    /**
 208    * Is {@link Element} an subject variable?
 209    *
 210    * @param element check this element
 211    * @throws CheckException if it is no subject variable
 212    */
 213  0 public static final void checkSubjectVariable(final Element element)
 214    throws CheckException {
 215  0 if (!element.isList() && element.getList().getOperator().equals(SUBJECT_VARIABLE_OPERATOR)
 216    && element.getList().size() == 1) {
 217    // check if first argument is an atom
 218  0 if (!element.getList().getElement(0).isAtom()) {
 219  0 throw new CheckException(FIRST_ARGUMENT_MUST_BE_AN_ATOM, element);
 220    }
 221    } else {
 222  0 throw new CheckException("subject variable expected", element);
 223    }
 224    }
 225   
 226   
 227    /**
 228    * Return all free subject variables of an element.
 229    *
 230    * @param element check this element
 231    * @return all free subject variables
 232    */
 233  0 public static final ElementSet getFreeSubjectVariables(final Element element) {
 234  0 final ElementSet free = new ElementSet();
 235  0 if (FormulaChecker.isSubjectVariable(element)) {
 236  0 free.add(element);
 237  0 } else if (element.isList()) {
 238  0 final ElementList list = element.getList();
 239  0 final String operator = list.getOperator();
 240  0 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 241    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 242  0 for (int i = 1; i < list.size(); i++) {
 243  0 free.union(FormulaChecker.getFreeSubjectVariables(list.getElement(i)));
 244    }
 245  0 free.remove(list.getElement(0));
 246    } else {
 247  0 for (int i = 0; i < list.size(); i++) {
 248  0 free.union(FormulaChecker.getFreeSubjectVariables(list.getElement(i)));
 249    }
 250    }
 251    }
 252  0 return free;
 253    }
 254   
 255    /**
 256    * Return all bound subject variables of an element.
 257    *
 258    * @param element check this element
 259    * @return all bound subject variables
 260    */
 261  0 public static final ElementSet getBoundSubjectVariables(final Element element) {
 262  0 final ElementSet bound = new ElementSet();
 263  0 if (element.isList()) {
 264  0 ElementList list = element.getList();
 265  0 final String operator = list.getOperator();
 266  0 if (operator.equals(EXISTENTIAL_QUANTIFIER_OPERATOR)
 267    || operator.equals(UNIVERSAL_QUANTIFIER_OPERATOR)) {
 268  0 for (int i = 1; i < list.size(); i++) {
 269  0 bound.union(FormulaChecker.getBoundSubjectVariables(
 270    list.getElement(i)));
 271    }
 272  0 bound.add(list.getElement(0));
 273    } else {
 274  0 for (int i = 0; i < list.size(); i++) {
 275  0 bound.union(FormulaChecker.getBoundSubjectVariables(list.getElement(i)));
 276    }
 277    }
 278    }
 279  0 return bound;
 280    }
 281   
 282   
 283    }
 
CloverReport generated by Clover Code Coverage v1.3.8
Do Dez 29 2005 18:39:59 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.