Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: So Mrz 11 2007 07:05:19 CET
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.3 2007/03/11 01:19:34 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.3 $
 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  30 private QedeqBoFormalLogicChecker(final String globalContext, final QedeqBo qedeq) {
 74  30 transverser = new QedeqNotNullTransverser(globalContext, this);
 75  30 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  30 public static void check(final String globalContext, final QedeqBo qedeq)
 86    throws ModuleDataException {
 87  30 final QedeqBoFormalLogicChecker checker = new QedeqBoFormalLogicChecker(globalContext,
 88    qedeq);
 89  30 checker.check();
 90    }
 91   
 92  30 private final void check() throws ModuleDataException {
 93  30 predicateDefinitions.clear();
 94  30 functionDefinitions.clear();
 95  30 setDefinitionByFormula = false;
 96  30 final PredicateDefinitionVo equal = new PredicateDefinitionVo();
 97    // TODO mime 20070102: quick hack to have the logical identity operator
 98  30 equal.setArgumentNumber("2");
 99  30 equal.setName("equal");
 100  30 equal.setLatexPattern("#1 \\ = \\ #2");
 101  30 predicateDefinitions.put(equal.getName() + "_" + equal.getArgumentNumber(), equal);
 102    // TODO mime 20070102: quick hack to get the negation of the logical identity operator
 103  30 final PredicateDefinitionVo notEqual = new PredicateDefinitionVo();
 104  30 notEqual.setArgumentNumber("2");
 105  30 notEqual.setName("notEqual");
 106  30 notEqual.setLatexPattern("#1 \\ \\neq \\ #2");
 107  30 predicateDefinitions.put(notEqual.getName() + "_" + notEqual.getArgumentNumber(), notEqual);
 108  30 transverser.accept(original);
 109    }
 110   
 111  91 public final void visitEnter(final Axiom axiom) throws ModuleDataException {
 112  91 if (axiom == null) {
 113  0 return;
 114    }
 115  91 final String context = getCurrentContext().getLocationWithinModule();
 116  91 if (axiom.getFormula() != null) {
 117  91 setLocationWithinModule(context + ".getFormula().getElement()");
 118  91 final Formula formula = axiom.getFormula();
 119  91 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 120    }
 121  87 setLocationWithinModule(context);
 122  87 transverser.setBlocked(true);
 123    }
 124   
 125  87 public final void visitLeave(final Axiom axiom) {
 126  87 transverser.setBlocked(false);
 127    }
 128   
 129  64 public final void visitEnter(final PredicateDefinition definition)
 130    throws ModuleDataException {
 131  64 if (definition == null) {
 132  0 return;
 133    }
 134  64 final String context = getCurrentContext().getLocationWithinModule();
 135  64 final String key = definition.getName() + "_" + definition.getArgumentNumber();
 136  64 if (predicateDefinitions.get(key) != null) {
 137  0 throw new IllegalModuleDataException(HigherLogicalErrors.PREDICATE_ALREADY_DEFINED,
 138    HigherLogicalErrors.PREDICATE_ALREADY_DEFINED_TEXT, getCurrentContext());
 139    }
 140  64 if (definition.getFormula() != null) {
 141  50 setLocationWithinModule(context + ".getFormula().getElement()");
 142  50 final Formula formula = definition.getFormula();
 143  50 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 144    }
 145  64 predicateDefinitions.put(key, definition);
 146  64 setLocationWithinModule(context);
 147  64 transverser.setBlocked(true);
 148    }
 149   
 150  64 public final void visitLeave(final PredicateDefinition definition) {
 151  64 transverser.setBlocked(false);
 152    }
 153   
 154  80 public final void visitEnter(final FunctionDefinition definition)
 155    throws ModuleDataException {
 156  80 if (definition == null) {
 157  0 return;
 158    }
 159  80 final String context = getCurrentContext().getLocationWithinModule();
 160  80 final String key = definition.getName() + "_" + definition.getArgumentNumber();
 161  80 if (functionDefinitions.get(key) != null) {
 162  0 throw new IllegalModuleDataException(HigherLogicalErrors.FUNCTION_ALREADY_DEFINED,
 163    HigherLogicalErrors.FUNCTION_ALREADY_DEFINED_TEXT, getCurrentContext());
 164    }
 165  80 if (definition.getTerm() != null) {
 166  80 setLocationWithinModule(context + ".getTerm().getElement()");
 167  80 final Term term = definition.getTerm();
 168  80 FormulaChecker.checkTerm(term.getElement(), getCurrentContext(), this);
 169    }
 170  80 predicateDefinitions.put(key, definition);
 171  80 setLocationWithinModule(context);
 172  80 transverser.setBlocked(true);
 173    }
 174   
 175  80 public final void visitLeave(final FunctionDefinition definition) {
 176  80 transverser.setBlocked(false);
 177    }
 178   
 179  273 public final void visitEnter(final Proposition proposition)
 180    throws ModuleDataException {
 181  273 if (proposition == null) {
 182  0 return;
 183    }
 184  273 final String context = getCurrentContext().getLocationWithinModule();
 185  273 if (proposition.getFormula() != null) {
 186  273 setLocationWithinModule(context + ".getFormula().getElement()");
 187  273 final Formula formula = proposition.getFormula();
 188  273 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), this);
 189    }
 190  271 setLocationWithinModule(context);
 191  271 transverser.setBlocked(true);
 192    }
 193   
 194  271 public final void visitLeave(final Proposition definition) {
 195  271 transverser.setBlocked(false);
 196    }
 197   
 198  33 public final void visitEnter(final Rule rule) throws ModuleDataException {
 199  33 if (rule == null) {
 200  0 return;
 201    }
 202  33 if (rule.getName() != null) {
 203  33 if ("SET_DEFINION_BY_FORMULA".equals(rule.getName())) {
 204  5 setDefinitionByFormula = true;
 205    }
 206    }
 207  33 transverser.setBlocked(true);
 208    }
 209   
 210  33 public final void visitLeave(final Rule rule) {
 211  33 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  996 public void setLocationWithinModule(final String locationWithinModule) {
 220  996 getCurrentContext().setLocationWithinModule(locationWithinModule);
 221    }
 222   
 223    /**
 224    * Get current context within original.
 225    *
 226    * @return Current context.
 227    */
 228  1998 public final ModuleContext getCurrentContext() {
 229  1998 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  2034 public boolean predicateExists(final String name, final int arguments) {
 242  2034 final PredicateDefinition definition = (PredicateDefinition) predicateDefinitions
 243    .get(name + "_" + arguments);
 244  2034 return null != definition;
 245    }
 246   
 247  1200 public boolean functionExists(final String name, final int arguments) {
 248  1200 final FunctionDefinition definition = (FunctionDefinition) predicateDefinitions
 249    .get(name + "_" + arguments);
 250  1200 return null != definition;
 251    }
 252   
 253  160 public boolean classOperatorExists() {
 254  160 return setDefinitionByFormula;
 255    }
 256   
 257  509 public boolean equalityOperatorExists() {
 258  509 return true;
 259    }
 260   
 261  494 public String getEqualityOperator() {
 262  494 return "equal";
 263    }
 264   
 265    }
 
CloverReport generated by Clover Code Coverage v1.3.10
So Mrz 11 2007 08:01:23 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.