Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Do Jan 11 2007 09:03:50 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 253   Methods: 16
NCLOC: 168   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
QedeqBoFormalLogicChecker.java 59,1% 86,7% 93,8% 82,3%
coverage coverage
 1    /* $Id: QedeqBoFactory.java,v 1.25 2006/10/20 20:23:05 m31 Exp $
 2    *
 3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
 4    *
 5    * Copyright 2000-2006, 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.CheckException;
 32    import org.qedeq.kernel.bo.logic.ExistenceChecker;
 33    import org.qedeq.kernel.bo.logic.FormulaChecker;
 34    import org.qedeq.kernel.bo.module.IllegalModuleDataException;
 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.context.ModuleContext;
 40    import org.qedeq.kernel.dto.module.PredicateDefinitionVo;
 41   
 42   
 43    /**
 44    * Checks if all formulas of a QEDEQ module are well formed.
 45    *
 46    * @version $Revision: 1.25 $
 47    * @author Michael Meyling
 48    */
 49    public final class QedeqBoFormalLogicChecker extends AbstractModuleVisitor
 50    implements ExistenceChecker {
 51   
 52    /** QEDEQ module input object. */
 53    private final QedeqBo original;
 54   
 55    /** Current context during creation. */
 56    private final QedeqNotNullTransverser transverser;
 57   
 58    /** Maps identifiers to {@link PredicateDefinition}s. */
 59    private final Map predicateDefinitions = new HashMap();
 60   
 61    /** Maps identifiers to {@link FunctionDefinition}s. */
 62    private final Map functionDefinitions = new HashMap();
 63   
 64    /** Is the class operator already defined? */
 65    private boolean setDefinitionByFormula;
 66   
 67   
 68    /**
 69    * Constructor.
 70    *
 71    * @param globalContext Module location information.
 72    * @param qedeq BO QEDEQ module object.
 73    */
 74  10 private QedeqBoFormalLogicChecker(final String globalContext, final QedeqBo qedeq) {
 75  10 transverser = new QedeqNotNullTransverser(globalContext, this);
 76  10 original = qedeq;
 77    }
 78   
 79    /**
 80    * Checks if all formulas of a QEDEQ module are well formed.
 81    *
 82    * @param globalContext Module location information.
 83    * @param qedeq Basic qedeq module object.
 84    * @throws ModuleDataException Major problem occured.
 85    */
 86  10 public static void check(final String globalContext, final QedeqBo qedeq)
 87    throws ModuleDataException {
 88  10 final QedeqBoFormalLogicChecker checker = new QedeqBoFormalLogicChecker(globalContext,
 89    qedeq);
 90  10 checker.check();
 91    }
 92   
 93  10 private final void check() throws ModuleDataException {
 94  10 predicateDefinitions.clear();
 95  10 functionDefinitions.clear();
 96  10 setDefinitionByFormula = false;
 97  10 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 98    // TODO mime 20070102: quick hack to have the logical identity operator
 99  10 equal.setArgumentNumber("2");
 100  10 equal.setName("equal");
 101  10 equal.setLatexPattern("#1 \\ = \\ #2");
 102  10 predicateDefinitions.put(equal.getName() + "_" + equal.getArgumentNumber(), equal);
 103    // TODO mime 20070102: quick hack to get the negation of the logical identity operator
 104  10 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 105  10 notEqual.setArgumentNumber("2");
 106  10 notEqual.setName("notEqual");
 107  10 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 108  10 predicateDefinitions.put(notEqual.getName() + "_" + notEqual.getArgumentNumber(), notEqual);
 109  10 transverser.accept(original);
 110    }
 111   
 112  32 public final void visitEnter(final Axiom axiom) throws ModuleDataException {
 113  32 if (axiom == null) {
 114  0 return;
 115    }
 116  32 final String context = getCurrentContext().getLocationWithinModule();
 117  32 if (axiom.getFormula() != null) {
 118  32 setLocationWithinModule(context + ".getFormula()");
 119  32 final Formula formula = axiom.getFormula();
 120  32 try {
 121  32 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 122    } catch (CheckException e) { // FIXME mime 20070109: remove after Context2XPath refactor
 123  0 throw new IllegalModuleDataException(e.getErrorCode(),
 124    "Logical Error", getCurrentContext(), e);
 125    }
 126    }
 127  32 setLocationWithinModule(context);
 128    }
 129   
 130  24 public final void visitEnter(final PredicateDefinition definition)
 131    throws ModuleDataException {
 132  24 if (definition == null) {
 133  0 return;
 134    }
 135  24 final String context = getCurrentContext().getLocationWithinModule();
 136  24 if (definition.getFormula() != null) {
 137  20 setLocationWithinModule(context + ".getFormula()");
 138  20 final Formula formula = definition.getFormula();
 139  20 try {
 140  20 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 141    } catch (CheckException e) { // FIXME mime 20070109: remove after Context2XPath refactor
 142  0 throw new IllegalModuleDataException(e.getErrorCode(),
 143    "Logical Error", getCurrentContext(), e);
 144    }
 145    }
 146  24 predicateDefinitions.put(definition.getName() + "_" + definition.getArgumentNumber(),
 147    definition);
 148  24 setLocationWithinModule(context);
 149    }
 150   
 151  32 public final void visitEnter(final FunctionDefinition definition)
 152    throws ModuleDataException {
 153  32 if (definition == null) {
 154  0 return;
 155    }
 156  32 final String context = getCurrentContext().getLocationWithinModule();
 157  32 if (definition.getTerm() != null) {
 158  32 setLocationWithinModule(context + ".getTerm()");
 159  32 final Term term = definition.getTerm();
 160  32 try {
 161  32 FormulaChecker.checkTerm(term.getElement(), getCurrentContext(), this);
 162    } catch (CheckException e) { // FIXME mime 20070109: remove after Context2XPath refactor
 163  0 throw new IllegalModuleDataException(e.getErrorCode(),
 164    "Logical Error", getCurrentContext(), e);
 165    }
 166    }
 167  32 predicateDefinitions.put(definition.getName() + "_" + definition.getArgumentNumber(),
 168    definition);
 169  32 setLocationWithinModule(context);
 170    }
 171   
 172  108 public final void visitEnter(final Proposition proposition)
 173    throws ModuleDataException {
 174  108 if (proposition == null) {
 175  0 return;
 176    }
 177  108 final String context = getCurrentContext().getLocationWithinModule();
 178  108 if (proposition.getFormula() != null) {
 179  108 setLocationWithinModule(context + ".getFormula()");
 180  108 final Formula formula = proposition.getFormula();
 181  108 try {
 182  108 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 183    } catch (CheckException e) { // FIXME mime 20070109: remove after Context2XPath refactor
 184  0 throw new IllegalModuleDataException(e.getErrorCode(),
 185    "Logical Error", getCurrentContext(), e);
 186    }
 187    }
 188  108 setLocationWithinModule(context);
 189    }
 190   
 191  4 public final void visitEnter(final Rule rule) throws ModuleDataException {
 192  4 if (rule == null) {
 193  0 return;
 194    }
 195  4 if (rule.getName() != null) {
 196  4 if ("SET_DEFINION_BY_FORMULA".equals(rule.getName())) {
 197  2 setDefinitionByFormula = true;
 198    }
 199    }
 200    }
 201   
 202    /**
 203    * Set location information where are we within the orginal module.
 204    *
 205    * @param locationWithinModule Location within module.
 206    */
 207  388 public void setLocationWithinModule(final String locationWithinModule) {
 208  388 getCurrentContext().setLocationWithinModule(locationWithinModule);
 209    }
 210   
 211    /**
 212    * Get current context within original.
 213    *
 214    * @return Current context.
 215    */
 216  776 public final ModuleContext getCurrentContext() {
 217  776 return transverser.getCurrentContext();
 218    }
 219   
 220    /**
 221    * Get original qedeq module.
 222    *
 223    * @return Original qedeq module.
 224    */
 225  0 protected final Qedeq getQedeqOriginal() {
 226  0 return original;
 227    }
 228   
 229  798 public boolean predicateExists(final String name, final int arguments) {
 230  798 final PredicateDefinition definition = (PredicateDefinition) predicateDefinitions
 231    .get(name + "_" + arguments);
 232  798 return null != definition;
 233    }
 234   
 235  480 public boolean functionExists(final String name, final int arguments) {
 236  480 final FunctionDefinition definition = (FunctionDefinition) predicateDefinitions
 237    .get(name + "_" + arguments);
 238  480 return null != definition;
 239    }
 240   
 241  64 public boolean classOperatorExists() {
 242  64 return setDefinitionByFormula;
 243    }
 244   
 245  198 public boolean equalityOperatorExists() {
 246  198 return true;
 247    }
 248   
 249  192 public String getEqualityOperator() {
 250  192 return "equal";
 251    }
 252   
 253    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Do Jan 11 2007 09:22:29 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.