Clover coverage report - QedeqKernelSe Coverage Report
Coverage timestamp: Sa Jan 26 2008 14:11:34 CET
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 272   Methods: 16
NCLOC: 194   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
QedeqBoFormalLogicChecker.java 64,7% 84,6% 93,8% 80,9%
coverage coverage
 1    /* $Id: QedeqBoFormalLogicChecker.java,v 1.6 2008/01/26 12:39:09 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 org.qedeq.kernel.base.module.Axiom;
 21    import org.qedeq.kernel.base.module.Formula;
 22    import org.qedeq.kernel.base.module.FunctionDefinition;
 23    import org.qedeq.kernel.base.module.PredicateDefinition;
 24    import org.qedeq.kernel.base.module.Proposition;
 25    import org.qedeq.kernel.base.module.Qedeq;
 26    import org.qedeq.kernel.base.module.Rule;
 27    import org.qedeq.kernel.base.module.Term;
 28    import org.qedeq.kernel.bo.logic.ExistenceChecker;
 29    import org.qedeq.kernel.bo.logic.FormulaChecker;
 30    import org.qedeq.kernel.bo.logic.Function;
 31    import org.qedeq.kernel.bo.logic.Predicate;
 32    import org.qedeq.kernel.bo.module.IllegalModuleDataException;
 33    import org.qedeq.kernel.bo.module.LogicalState;
 34    import org.qedeq.kernel.bo.module.ModuleContext;
 35    import org.qedeq.kernel.bo.module.ModuleDataException;
 36    import org.qedeq.kernel.bo.module.ModuleProperties;
 37    import org.qedeq.kernel.bo.module.ModuleReferenceList;
 38    import org.qedeq.kernel.bo.visitor.AbstractModuleVisitor;
 39    import org.qedeq.kernel.bo.visitor.QedeqNotNullTraverser;
 40    import org.qedeq.kernel.common.SourceFileExceptionList;
 41    import org.qedeq.kernel.log.ModuleEventLog;
 42    import org.qedeq.kernel.trace.Trace;
 43    import org.qedeq.kernel.xml.mapper.ModuleDataException2XmlFileException;
 44   
 45   
 46    /**
 47    * Checks if all formulas of a QEDEQ module are well formed.
 48    *
 49    * @version $Revision: 1.6 $
 50    * @author Michael Meyling
 51    */
 52    public final class QedeqBoFormalLogicChecker extends AbstractModuleVisitor {
 53   
 54    /** This class. */
 55    private static final Class CLASS = QedeqBoFormalLogicChecker.class;
 56   
 57    /** QEDEQ module properties. */
 58    private final ModuleProperties prop;
 59   
 60    /** Current context during creation. */
 61    private final QedeqNotNullTraverser traverser;
 62   
 63    /** Existence checker for predicate and function constants. */
 64    private ModuleConstantsExistenceChecker existence;
 65   
 66    /**
 67    * Constructor.
 68    *
 69    * @param prop QEDEQ module properties object.
 70    */
 71  59 private QedeqBoFormalLogicChecker(final ModuleProperties prop) {
 72  59 this.traverser = new QedeqNotNullTraverser(prop.getModuleAddress(), this);
 73  59 this.prop = prop;
 74    }
 75   
 76    /**
 77    * Checks if all formulas of a QEDEQ module are well formed.
 78    *
 79    * @param prop QEDEQ module properties object.
 80    * @throws SourceFileExceptionList Major problem occurred.
 81    */
 82  99 public static void check(final ModuleProperties prop)
 83    throws SourceFileExceptionList {
 84  99 if (prop.isChecked()) {
 85  40 return;
 86    }
 87  59 if (!prop.hasLoadedRequiredModules()) {
 88  0 throw new IllegalStateException("QEDEQ module has not loaded with required files: "
 89    + prop);
 90    }
 91  59 prop.setLogicalProgressState(LogicalState.STATE_EXTERNAL_CHECKING);
 92  59 ModuleEventLog.getInstance().stateChanged(prop);
 93  59 ModuleReferenceList list = prop.getRequiredModules();
 94  59 for (int i = 0; i < list.size(); i++) {
 95  38 try {
 96  38 Trace.trace(CLASS, "check(ModuleProperties)", "checking label",
 97    list.getLabel(i));
 98  38 check(list.getModuleProperties(i));
 99    } catch (SourceFileExceptionList e) { // TODO mime 20080114: hard coded codes
 100  0 ModuleDataException md = new CheckRequiredModuleException(11231,
 101    "import check failed: " + list.getModuleProperties(i).getModuleAddress(),
 102    list.getModuleContext(i));
 103  0 final SourceFileExceptionList sfl =
 104    ModuleDataException2XmlFileException.createXmlFileExceptionList(md,
 105    prop.getModule().getQedeq());
 106  0 prop.setLogicalFailureState(LogicalState.STATE_EXTERNAL_CHECKING_FAILED, sfl);
 107  0 ModuleEventLog.getInstance().stateChanged(prop);
 108  0 throw e;
 109    }
 110    }
 111  59 prop.setLogicalProgressState(LogicalState.STATE_INTERNAL_CHECKING);
 112  59 ModuleEventLog.getInstance().stateChanged(prop);
 113  59 final QedeqBoFormalLogicChecker checker = new QedeqBoFormalLogicChecker(prop);
 114  59 try {
 115  59 checker.check();
 116    } catch (ModuleDataException e) {
 117  21 final SourceFileExceptionList sfl =
 118    ModuleDataException2XmlFileException.createXmlFileExceptionList(e,
 119    prop.getModule().getQedeq());
 120  21 prop.setLogicalFailureState(LogicalState.STATE_INTERNAL_CHECKING_FAILED, sfl);
 121  21 ModuleEventLog.getInstance().stateChanged(prop);
 122  21 throw sfl;
 123    }
 124  38 prop.setChecked(checker.existence);
 125  38 ModuleEventLog.getInstance().stateChanged(prop);
 126    }
 127   
 128  59 private void check() throws ModuleDataException {
 129  59 this.existence = new ModuleConstantsExistenceChecker(prop);
 130  59 traverser.accept(prop.getModule().getQedeq());
 131    }
 132   
 133  181 public void visitEnter(final Axiom axiom) throws ModuleDataException {
 134  181 if (axiom == null) {
 135  0 return;
 136    }
 137  181 final String context = getCurrentContext().getLocationWithinModule();
 138  181 if (axiom.getFormula() != null) {
 139  181 setLocationWithinModule(context + ".getFormula().getElement()");
 140  181 final Formula formula = axiom.getFormula();
 141  181 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), existence);
 142    }
 143  168 setLocationWithinModule(context);
 144  168 traverser.setBlocked(true);
 145    }
 146   
 147  168 public void visitLeave(final Axiom axiom) {
 148  168 traverser.setBlocked(false);
 149    }
 150   
 151  164 public void visitEnter(final PredicateDefinition definition)
 152    throws ModuleDataException {
 153  164 if (definition == null) {
 154  0 return;
 155    }
 156  164 final String context = getCurrentContext().getLocationWithinModule();
 157  164 final Predicate predicate = new Predicate(definition.getName(),
 158    definition.getArgumentNumber());
 159  164 if (existence.predicateExists(predicate)) {
 160  0 throw new IllegalModuleDataException(HigherLogicalErrors.PREDICATE_ALREADY_DEFINED,
 161    HigherLogicalErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicate,
 162    getCurrentContext());
 163    }
 164  164 if ("2".equals(predicate.getArguments())
 165    && ExistenceChecker.NAME_EQUAL.equals(predicate.getName())) {
 166  13 existence.setIdentityOperatorDefined(true, predicate.getName());
 167    }
 168  164 if (definition.getFormula() != null) {
 169  129 setLocationWithinModule(context + ".getFormula().getElement()");
 170  129 final Formula formula = definition.getFormula();
 171  129 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), existence);
 172    }
 173  164 existence.add(definition);
 174  164 setLocationWithinModule(context);
 175  164 traverser.setBlocked(true);
 176    }
 177   
 178  164 public void visitLeave(final PredicateDefinition definition) {
 179  164 traverser.setBlocked(false);
 180    }
 181   
 182  96 public void visitEnter(final FunctionDefinition definition)
 183    throws ModuleDataException {
 184  96 if (definition == null) {
 185  0 return;
 186    }
 187  96 final String context = getCurrentContext().getLocationWithinModule();
 188  96 final Function function = new Function(definition.getName(),
 189    definition.getArgumentNumber());
 190  96 if (existence.functionExists(function)) {
 191  0 throw new IllegalModuleDataException(HigherLogicalErrors.FUNCTION_ALREADY_DEFINED,
 192    HigherLogicalErrors.FUNCTION_ALREADY_DEFINED_TEXT + function,
 193    getCurrentContext());
 194    }
 195  96 if (definition.getTerm() != null) {
 196  96 setLocationWithinModule(context + ".getTerm().getElement()");
 197  96 final Term term = definition.getTerm();
 198  96 FormulaChecker.checkTerm(term.getElement(), getCurrentContext(), existence);
 199    }
 200  96 existence.add(definition);
 201  96 setLocationWithinModule(context);
 202  96 traverser.setBlocked(true);
 203    }
 204   
 205  96 public void visitLeave(final FunctionDefinition definition) {
 206  96 traverser.setBlocked(false);
 207    }
 208   
 209  374 public void visitEnter(final Proposition proposition)
 210    throws ModuleDataException {
 211  374 if (proposition == null) {
 212  0 return;
 213    }
 214  374 final String context = getCurrentContext().getLocationWithinModule();
 215  374 if (proposition.getFormula() != null) {
 216  374 setLocationWithinModule(context + ".getFormula().getElement()");
 217  374 final Formula formula = proposition.getFormula();
 218  374 FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), existence);
 219    }
 220  366 setLocationWithinModule(context);
 221  366 traverser.setBlocked(true);
 222    }
 223   
 224  366 public void visitLeave(final Proposition definition) {
 225  366 traverser.setBlocked(false);
 226    }
 227   
 228  114 public void visitEnter(final Rule rule) throws ModuleDataException {
 229  114 if (rule == null) {
 230  0 return;
 231    }
 232  114 if (rule.getName() != null) {
 233  114 if ("SET_DEFINION_BY_FORMULA".equals(rule.getName())) {
 234    // LATER mime 20080114: check if this rule can be proposed
 235  6 existence.setClassOperatorExists(true);
 236    }
 237    }
 238  114 traverser.setBlocked(true);
 239    }
 240   
 241  114 public void visitLeave(final Rule rule) {
 242  114 traverser.setBlocked(false);
 243    }
 244   
 245    /**
 246    * Set location information where are we within the original module.
 247    *
 248    * @param locationWithinModule Location within module.
 249    */
 250  1574 public void setLocationWithinModule(final String locationWithinModule) {
 251  1574 getCurrentContext().setLocationWithinModule(locationWithinModule);
 252    }
 253   
 254    /**
 255    * Get current context within original.
 256    *
 257    * @return Current context.
 258    */
 259  3169 public final ModuleContext getCurrentContext() {
 260  3169 return traverser.getCurrentContext();
 261    }
 262   
 263    /**
 264    * Get original QEDEQ module.
 265    *
 266    * @return Original QEDEQ module.
 267    */
 268  0 protected final Qedeq getQedeqOriginal() {
 269  0 return prop.getModule().getQedeq();
 270    }
 271   
 272    }
 
CloverReport generated by Clover Code Coverage v1.3.10
Sa Jan 26 2008 15:40:52 CET.		   Open Source License registered to the Hilbert II Project. This license of Clover is provided to support the development of Hilbert II only.