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: 265   Methods: 21
NCLOC: 175   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
QedeqBoFormalLogicChecker.java 57,7% 90,4% 95,2% 84,6%
coverage coverage
 1    /* $Id: QedeqBoFormalLogicChecker.java,v 1.4 2007/04/12 23:50:11 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.control;
 19   
 20    import java.util.HashMap;
 21    import java.util.Map;
 22   
 23    import org.qedeq.kernel.base.module.Axiom;
 24    import org.qedeq.kernel.base.module.Formula;
 25    import org.qedeq.kernel.base.module.FunctionDefinition;
 26    import org.qedeq.kernel.base.module.PredicateDefinition;
 27    import org.qedeq.kernel.base.module.Proposition;
 28    import org.qedeq.kernel.base.module.Qedeq;
 29    import org.qedeq.kernel.base.module.Rule;
 30    import org.qedeq.kernel.base.module.Term;
 31    import org.qedeq.kernel.bo.logic.ExistenceChecker;
 32    import org.qedeq.kernel.bo.logic.FormulaChecker;
 33    import org.qedeq.kernel.bo.module.IllegalModuleDataException;
 34    import org.qedeq.kernel.bo.module.ModuleContext;
 35    import org.qedeq.kernel.bo.module.ModuleDataException;
 36    import org.qedeq.kernel.bo.module.QedeqBo;
 37    import org.qedeq.kernel.bo.visitor.AbstractModuleVisitor;
 38    import org.qedeq.kernel.bo.visitor.QedeqNotNullTransverser;
 39    import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
 40   
 41   
 42    /**
 43    * Checks if all formulas of a QEDEQ module are well formed.
 44    *
 45    * @version $Revision: 1.4 $
 46    * @author Michael Meyling
 47    */
 48    public final class QedeqBoFormalLogicChecker extends AbstractModuleVisitor
 49    implements ExistenceChecker {
 50   
 51    /** QEDEQ module input object. */
 52    private final QedeqBo original;
 53   
 54    /** Current context during creation. */
 55    private final QedeqNotNullTransverser transverser;
 56   
 57    /** Maps identifiers to {@link PredicateDefinition}s. */
 58    private final Map predicateDefinitions = new HashMap();
 59   
 60    /** Maps identifiers to {@link FunctionDefinition}s. */
 61    private final Map functionDefinitions = new HashMap();
 62   
 63    /** Is the class operator already defined? */
 64    private boolean setDefinitionByFormula;
 65   
 66   
 67    /**
 68    * Constructor.
 69    *
 70    * @param globalContext Module location information.
 71    * @param qedeq BO QEDEQ module object.
 72    */
 73  26 private QedeqBoFormalLogicChecker(final String globalContext, final QedeqBo qedeq) {
 74  26 transverser = new QedeqNotNullTransverser(globalContext, this);
 75  26 original = qedeq;
 76    }
 77   
 78    /**
 79    * Checks if all formulas of a QEDEQ module are well formed.
 80    *
 81    * @param globalContext Module location information.
 82    * @param qedeq Basic QEDEQ module object.
 83    * @throws ModuleDataException Major problem occured.
 84    */
 85  26 public static void check(final String globalContext, final QedeqBo qedeq)
 86    throws ModuleDataException {
 87  26 final QedeqBoFormalLogicChecker checker = new QedeqBoFormalLogicChecker(globalContext,
 88    qedeq);
 89  26 checker.check();
 90    }
 91   
 92  26 private final void check() throws ModuleDataException {
 93  26 predicateDefinitions.clear();
 94  26 functionDefinitions.clear();
 95  26 setDefinitionByFormula = false;
 96  26 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 97    // TODO mime 20070102: quick hack to have the logical identity operator
 98  26 equal.setArgumentNumber("2");
 99  26 equal.setName("equal");
 100  26 equal.setLatexPattern("#1 \\ = \\ #2");
 101  26 predicateDefinitions.put(equal.getName() + "_" + equal.getArgumentNumber(), equal);
 102    // TODO mime 20070102: quick hack to get the negation of the logical identity operator
 103  26 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 104  26 notEqual.setArgumentNumber("2");
 105  26 notEqual.setName("notEqual");
 106  26 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 107  26 predicateDefinitions.put(notEqual.getName() + "_" + notEqual.getArgumentNumber(), notEqual);
 108  26 transverser.accept(original);
 109    }
 110   
 111  94 public final void visitEnter(final Axiom axiom) throws ModuleDataException {
 112  94 if (axiom == null) {
 113  0 return;
 114    }
 115  94 final String context = getCurrentContext().getLocationWithinModule();
 116  94 if (axiom.getFormula() != null) {
 117  94 setLocationWithinModule(context + ".getFormula().getElement()");
 118  94 final Formula formula = axiom.getFormula();
 119  94 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 120    }
 121  90 setLocationWithinModule(context);
 122  90 transverser.setBlocked(true);
 123    }
 124   
 125  90 public final void visitLeave(final Axiom axiom) {
 126  90 transverser.setBlocked(false);
 127    }
 128   
 129  70 public final void visitEnter(final PredicateDefinition definition)
 130    throws ModuleDataException {
 131  70 if (definition == null) {
 132  0 return;
 133    }
 134  70 final String context = getCurrentContext().getLocationWithinModule();
 135  70 final String key = definition.getName() + "_" + definition.getArgumentNumber();
 136  70 if (predicateDefinitions.get(key) != null) {
 137  0 throw new IllegalModuleDataException(HigherLogicalErrors.PREDICATE_ALREADY_DEFINED,
 138    HigherLogicalErrors.PREDICATE_ALREADY_DEFINED_TEXT, getCurrentContext());
 139    }
 140  70 if (definition.getFormula() != null) {
 141  57 setLocationWithinModule(context + ".getFormula().getElement()");
 142  57 final Formula formula = definition.getFormula();
 143  57 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 144    }
 145  70 predicateDefinitions.put(key, definition);
 146  70 setLocationWithinModule(context);
 147  70 transverser.setBlocked(true);
 148    }
 149   
 150  70 public final void visitLeave(final PredicateDefinition definition) {
 151  70 transverser.setBlocked(false);
 152    }
 153   
 154  96 public final void visitEnter(final FunctionDefinition definition)
 155    throws ModuleDataException {
 156  96 if (definition == null) {
 157  0 return;
 158    }
 159  96 final String context = getCurrentContext().getLocationWithinModule();
 160  96 final String key = definition.getName() + "_" + definition.getArgumentNumber();
 161  96 if (functionDefinitions.get(key) != null) {
 162  0 throw new IllegalModuleDataException(HigherLogicalErrors.FUNCTION_ALREADY_DEFINED,
 163    HigherLogicalErrors.FUNCTION_ALREADY_DEFINED_TEXT, getCurrentContext());
 164    }
 165  96 if (definition.getTerm() != null) {
 166  96 setLocationWithinModule(context + ".getTerm().getElement()");
 167  96 final Term term = definition.getTerm();
 168  96 FormulaChecker.checkTerm(term.getElement(), getCurrentContext(), this);
 169    }
 170  96 predicateDefinitions.put(key, definition);
 171  96 setLocationWithinModule(context);
 172  96 transverser.setBlocked(true);
 173    }
 174   
 175  96 public final void visitLeave(final FunctionDefinition definition) {
 176  96 transverser.setBlocked(false);
 177    }
 178   
 179  327 public final void visitEnter(final Proposition proposition)
 180    throws ModuleDataException {
 181  327 if (proposition == null) {
 182  0 return;
 183    }
 184  327 final String context = getCurrentContext().getLocationWithinModule();
 185  327 if (proposition.getFormula() != null) {
 186  327 setLocationWithinModule(context + ".getFormula().getElement()");
 187  327 final Formula formula = proposition.getFormula();
 188  327 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 189    }
 190  325 setLocationWithinModule(context);
 191  325 transverser.setBlocked(true);
 192    }
 193   
 194  325 public final void visitLeave(final Proposition definition) {
 195  325 transverser.setBlocked(false);
 196    }
 197   
 198  27 public final void visitEnter(final Rule rule) throws ModuleDataException {
 199  27 if (rule == null) {
 200  0 return;
 201    }
 202  27 if (rule.getName() != null) {
 203  27 if ("SET_DEFINION_BY_FORMULA".equals(rule.getName())) {
 204  6 setDefinitionByFormula = true;
 205    }
 206    }
 207  27 transverser.setBlocked(true);
 208    }
 209   
 210  27 public final void visitLeave(final Rule rule) {
 211  27 transverser.setBlocked(false);
 212    }
 213   
 214    /**
 215    * Set location information where are we within the original module.
 216    *
 217    * @param locationWithinModule Location within module.
 218    */
 219  1155 public void setLocationWithinModule(final String locationWithinModule) {
 220  1155 getCurrentContext().setLocationWithinModule(locationWithinModule);
 221    }
 222   
 223    /**
 224    * Get current context within original.
 225    *
 226    * @return Current context.
 227    */
 228  2316 public final ModuleContext getCurrentContext() {
 229  2316 return transverser.getCurrentContext();
 230    }
 231   
 232    /**
 233    * Get original QEDEQ module.
 234    *
 235    * @return Original QEDEQ module.
 236    */
 237  0 protected final Qedeq getQedeqOriginal() {
 238  0 return original;
 239    }
 240   
 241  2447 public boolean predicateExists(final String name, final int arguments) {
 242  2447 final PredicateDefinition definition = (PredicateDefinition) predicateDefinitions
 243    .get(name + "_" + arguments);
 244  2447 return null != definition;
 245    }
 246   
 247  1440 public boolean functionExists(final String name, final int arguments) {
 248  1440 final FunctionDefinition definition = (FunctionDefinition) predicateDefinitions
 249    .get(name + "_" + arguments);
 250  1440 return null != definition;
 251    }
 252   
 253  192 public boolean classOperatorExists() {
 254  192 return setDefinitionByFormula;
 255    }
 256   
 257  592 public boolean equalityOperatorExists() {
 258  592 return true;
 259    }
 260   
 261  574 public String getEqualityOperator() {
 262  574 return "equal";
 263    }
 264   
 265    }
 
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.