Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: So Feb 25 2007 22:22:30 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 240   Methods: 16
NCLOC: 155   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
QedeqBoFormalLogicChecker.java 57,7% 89% 93,8% 82,6%
coverage coverage
 1    /* $Id: QedeqBoFormalLogicChecker.java,v 1.2 2007/02/25 20:05:38 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.ModuleDataException;
 35    import org.qedeq.kernel.bo.module.QedeqBo;
 36    import org.qedeq.kernel.bo.visitor.AbstractModuleVisitor;
 37    import org.qedeq.kernel.bo.visitor.QedeqNotNullTransverser;
 38    import org.qedeq.kernel.context.ModuleContext;
 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.2 $
 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  10 private QedeqBoFormalLogicChecker(final String globalContext, final QedeqBo qedeq) {
 74  10 transverser = new QedeqNotNullTransverser(globalContext, this);
 75  10 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  10 public static void check(final String globalContext, final QedeqBo qedeq)
 86    throws ModuleDataException {
 87  10 final QedeqBoFormalLogicChecker checker = new QedeqBoFormalLogicChecker(globalContext,
 88    qedeq);
 89  10 checker.check();
 90    }
 91   
 92  10 private final void check() throws ModuleDataException {
 93  10 predicateDefinitions.clear();
 94  10 functionDefinitions.clear();
 95  10 setDefinitionByFormula = false;
 96  10 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 97    // TODO mime 20070102: quick hack to have the logical identity operator
 98  10 equal.setArgumentNumber("2");
 99  10 equal.setName("equal");
 100  10 equal.setLatexPattern("#1 \\ = \\ #2");
 101  10 predicateDefinitions.put(equal.getName() + "_" + equal.getArgumentNumber(), equal);
 102    // TODO mime 20070102: quick hack to get the negation of the logical identity operator
 103  10 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 104  10 notEqual.setArgumentNumber("2");
 105  10 notEqual.setName("notEqual");
 106  10 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 107  10 predicateDefinitions.put(notEqual.getName() + "_" + notEqual.getArgumentNumber(), notEqual);
 108  10 transverser.accept(original);
 109    }
 110   
 111  36 public final void visitEnter(final Axiom axiom) throws ModuleDataException {
 112  36 if (axiom == null) {
 113  0 return;
 114    }
 115  36 final String context = getCurrentContext().getLocationWithinModule();
 116  36 if (axiom.getFormula() != null) {
 117  36 setLocationWithinModule(context + ".getFormula().getElement()");
 118  36 final Formula formula = axiom.getFormula();
 119  36 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 120    }
 121  36 setLocationWithinModule(context);
 122    }
 123   
 124  24 public final void visitEnter(final PredicateDefinition definition)
 125    throws ModuleDataException {
 126  24 if (definition == null) {
 127  0 return;
 128    }
 129  24 final String context = getCurrentContext().getLocationWithinModule();
 130  24 final String key = definition.getName() + "_" + definition.getArgumentNumber();
 131  24 if (predicateDefinitions.get(key) != null) {
 132  0 throw new IllegalModuleDataException(HigherLogicalErrors.PREDICATE_ALREADY_DEFINED,
 133    HigherLogicalErrors.PREDICATE_ALREADY_DEFINED_TEXT, getCurrentContext());
 134    }
 135  24 if (definition.getFormula() != null) {
 136  20 setLocationWithinModule(context + ".getFormula().getElement()");
 137  20 final Formula formula = definition.getFormula();
 138  20 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 139    }
 140  24 predicateDefinitions.put(key, definition);
 141  24 setLocationWithinModule(context);
 142    }
 143   
 144  32 public final void visitEnter(final FunctionDefinition definition)
 145    throws ModuleDataException {
 146  32 if (definition == null) {
 147  0 return;
 148    }
 149  32 final String context = getCurrentContext().getLocationWithinModule();
 150  32 final String key = definition.getName() + "_" + definition.getArgumentNumber();
 151  32 if (functionDefinitions.get(key) != null) {
 152  0 throw new IllegalModuleDataException(HigherLogicalErrors.FUNCTION_ALREADY_DEFINED,
 153    HigherLogicalErrors.FUNCTION_ALREADY_DEFINED_TEXT, getCurrentContext());
 154    }
 155  32 if (definition.getTerm() != null) {
 156  32 setLocationWithinModule(context + ".getTerm().getElement()");
 157  32 final Term term = definition.getTerm();
 158  32 FormulaChecker.checkTerm(term.getElement(), getCurrentContext(), this);
 159    }
 160  32 predicateDefinitions.put(key, definition);
 161  32 setLocationWithinModule(context);
 162    }
 163   
 164  108 public final void visitEnter(final Proposition proposition)
 165    throws ModuleDataException {
 166  108 if (proposition == null) {
 167  0 return;
 168    }
 169  108 final String context = getCurrentContext().getLocationWithinModule();
 170  108 if (proposition.getFormula() != null) {
 171  108 setLocationWithinModule(context + ".getFormula().getElement()");
 172  108 final Formula formula = proposition.getFormula();
 173  108 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 174    }
 175  108 setLocationWithinModule(context);
 176    }
 177   
 178  16 public final void visitEnter(final Rule rule) throws ModuleDataException {
 179  16 if (rule == null) {
 180  0 return;
 181    }
 182  16 if (rule.getName() != null) {
 183  16 if ("SET_DEFINION_BY_FORMULA".equals(rule.getName())) {
 184  2 setDefinitionByFormula = true;
 185    }
 186    }
 187    }
 188   
 189    /**
 190    * Set location information where are we within the original module.
 191    *
 192    * @param locationWithinModule Location within module.
 193    */
 194  396 public void setLocationWithinModule(final String locationWithinModule) {
 195  396 getCurrentContext().setLocationWithinModule(locationWithinModule);
 196    }
 197   
 198    /**
 199    * Get current context within original.
 200    *
 201    * @return Current context.
 202    */
 203  792 public final ModuleContext getCurrentContext() {
 204  792 return transverser.getCurrentContext();
 205    }
 206   
 207    /**
 208    * Get original QEDEQ module.
 209    *
 210    * @return Original QEDEQ module.
 211    */
 212  0 protected final Qedeq getQedeqOriginal() {
 213  0 return original;
 214    }
 215   
 216  802 public boolean predicateExists(final String name, final int arguments) {
 217  802 final PredicateDefinition definition = (PredicateDefinition) predicateDefinitions
 218    .get(name + "_" + arguments);
 219  802 return null != definition;
 220    }
 221   
 222  480 public boolean functionExists(final String name, final int arguments) {
 223  480 final FunctionDefinition definition = (FunctionDefinition) predicateDefinitions
 224    .get(name + "_" + arguments);
 225  480 return null != definition;
 226    }
 227   
 228  64 public boolean classOperatorExists() {
 229  64 return setDefinitionByFormula;
 230    }
 231   
 232  202 public boolean equalityOperatorExists() {
 233  202 return true;
 234    }
 235   
 236  196 public String getEqualityOperator() {
 237  196 return "equal";
 238    }
 239   
 240    }
 
CloverReport generated by Clover Code Coverage v1.3.10
So Feb 25 2007 22:59:53 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.