Clover Coverage Report
Coverage timestamp: Sa Aug 2 2008 13:56:27 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
73   186   15   7,3
0   139   0,21   10
10     1,5  
1    
 
  CheckLogicTest       Line # 55 73 15 91,6% 0.91566265
 
  (5)
 
1    /* $Id: CheckLogicTest.java,v 1.1 2008/07/26 07:59:13 m31 Exp $
2    *
3    * This file is part of the project "Hilbert II" - http://www.qedeq.org
4    *
5    * Copyright 2000-2008, 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.logic.wf;
19   
20    import java.io.File;
21    import java.io.IOException;
22   
23    import javax.xml.parsers.ParserConfigurationException;
24   
25    import org.qedeq.base.io.IoUtility;
26    import org.qedeq.base.test.QedeqTestCase;
27    import org.qedeq.base.trace.Trace;
28    import org.qedeq.kernel.bo.logic.FormulaChecker;
29    import org.qedeq.kernel.bo.module.InternalKernelServices;
30    import org.qedeq.kernel.bo.module.KernelModuleReferenceList;
31    import org.qedeq.kernel.bo.module.QedeqFileDao;
32    import org.qedeq.kernel.bo.service.DefaultKernelQedeqBo;
33    import org.qedeq.kernel.bo.service.ModuleLabelsCreator;
34    import org.qedeq.kernel.bo.service.QedeqBoFormalLogicChecker;
35    import org.qedeq.kernel.bo.service.QedeqVoBuilder;
36    import org.qedeq.kernel.bo.test.KernelFacade;
37    import org.qedeq.kernel.common.DefaultSourceFileExceptionList;
38    import org.qedeq.kernel.common.ModuleAddress;
39    import org.qedeq.kernel.common.ModuleDataException;
40    import org.qedeq.kernel.common.SourceFileException;
41    import org.qedeq.kernel.common.SourceFileExceptionList;
42    import org.qedeq.kernel.dto.module.QedeqVo;
43    import org.qedeq.kernel.xml.dao.XmlQedeqFileDao;
44    import org.qedeq.kernel.xml.handler.module.QedeqHandler;
45    import org.qedeq.kernel.xml.parser.SaxDefaultHandler;
46    import org.qedeq.kernel.xml.parser.SaxParser;
47    import org.xml.sax.SAXException;
48   
49    /**
50    * Test generating LaTeX files for all known samples.
51    *
52    * @version $Revision: 1.1 $
53    * @author Michael Meyling
54    */
 
55    public final class CheckLogicTest extends QedeqTestCase {
56   
57    /** This class. */
58    private static final Class CLASS = FormulaChecker.class;
59   
60   
 
61  0 toggle public CheckLogicTest() {
62  0 super();
63    }
64   
 
65  5 toggle public CheckLogicTest(final String name) {
66  5 super(name);
67    }
68   
 
69  5 toggle public void setUp() {
70  5 KernelFacade.startup();
71    }
72   
 
73  5 toggle public void tearDown() {
74  5 KernelFacade.shutdown();
75    }
76   
 
77  1 toggle public void testNegative00() throws Exception {
78  1 try {
79  1 generate(getFile("qedeq_error_sample_00.xml"));
80  0 fail("DefaultSourceFileExceptionList expected");
81    } catch (DefaultSourceFileExceptionList ex) {
82  1 Trace.trace(CLASS, this, "testNegative00", ex);
83  1 assertEquals(1, ex.size());
84  1 final SourceFileException check = ex.get(0);
85    // check.printStackTrace();
86  1 assertEquals(9001, check.getErrorCode());
87  1 assertEquals(36, check.getSourceArea().getStartPosition().getLine());
88  1 assertEquals(1, check.getSourceArea().getStartPosition().getColumn());
89  1 assertEquals(36, check.getSourceArea().getEndPosition().getLine());
90  1 assertEquals(20, check.getSourceArea().getEndPosition().getColumn());
91    }
92    }
93   
 
94  1 toggle public void testNegative01() throws Exception {
95  1 try {
96  1 generate(getFile("qedeq_error_sample_01.xml"));
97  0 fail("DefaultSourceFileExceptionList expected");
98    } catch (DefaultSourceFileExceptionList ex) {
99  1 Trace.trace(CLASS, this, "testNegative01", ex);
100  1 assertEquals(1, ex.size());
101  1 final SourceFileException check = ex.get(0);
102  1 assertEquals(9001, check.getErrorCode());
103  1 assertEquals(39, check.getSourceArea().getStartPosition().getLine());
104  1 assertEquals(1, check.getSourceArea().getStartPosition().getColumn());
105  1 assertEquals(39, check.getSourceArea().getEndPosition().getLine());
106  1 assertEquals(35, check.getSourceArea().getEndPosition().getColumn());
107    }
108    }
109   
 
110  1 toggle public void testNegative02() throws Exception {
111  1 try {
112  1 generate(getFile("qedeq_error_sample_02.xml"));
113  0 fail("ModuleDataException expected");
114    } catch (SourceFileExceptionList sfl) {
115  1 Trace.trace(CLASS, this, "testNegative02", sfl);
116  1 final Exception e = (Exception) sfl.get(0).getCause();
117  1 Trace.param(CLASS, this, "testNegative02", "name", e.getClass().getName());
118  1 assertTrue(e instanceof LogicalCheckException);
119  1 final LogicalCheckException check = (LogicalCheckException) e;
120  1 assertEquals(30550, check.getErrorCode());
121  1 assertEquals("getChapterList().get(0).getSectionList().get(0).getSubsectionList().get(0).getNodeType().getAxiom().getFormula().getElement().getList().getElement(1).getList()", check.getContext().getLocationWithinModule());
122  1 assertNull(check.getReferenceContext());
123    }
124    }
125   
 
126  1 toggle public void testNegative03() throws Exception {
127  1 try {
128  1 generate(getFile("qedeq_error_sample_03.xml"));
129  0 fail("ModuleDataException expected");
130    } catch (SourceFileExceptionList sfl) {
131  1 Trace.trace(CLASS, this, "testNegative03", sfl);
132  1 final Exception e = (Exception) sfl.get(0).getCause();
133  1 assertTrue(e instanceof LogicalCheckException);
134  1 final LogicalCheckException check = (LogicalCheckException) e;
135  1 assertEquals(30770, check.getErrorCode());
136  1 assertEquals("getChapterList().get(0).getSectionList().get(0).getSubsectionList().get(0).getNodeType().getAxiom().getFormula().getElement().getList().getElement(1)", check.getContext().getLocationWithinModule());
137  1 assertNull(check.getReferenceContext());
138    }
139    }
140   
 
141  1 toggle public void testNegative04() throws Exception {
142  1 try {
143  1 generate(getFile("qedeq_error_sample_04.xml"));
144  0 fail("ModuleDataException expected");
145    } catch (SourceFileExceptionList sfl) {
146  1 Trace.trace(CLASS, this, "testNegative04", sfl);
147  1 final Exception e = (Exception) sfl.get(0).getCause();
148  1 assertTrue(e instanceof LogicalCheckException);
149  1 final LogicalCheckException check = (LogicalCheckException) e;
150  1 assertEquals(30780, check.getErrorCode());
151  1 assertEquals("getChapterList().get(0).getSectionList().get(0).getSubsectionList().get(0).getNodeType().getAxiom().getFormula().getElement().getList().getElement(1)", check.getContext().getLocationWithinModule());
152  1 assertNull(check.getReferenceContext());
153    }
154    }
155   
156    /**
157    * Check logic of QEDEQ module given as XML file.
158    *
159    * @param xmlFile Module file to check.
160    */
 
161  5 toggle private static void generate(final File xmlFile) throws IOException,
162    ParserConfigurationException, SAXException, ModuleDataException,
163    SourceFileExceptionList {
164  5 final ModuleAddress context = KernelFacade.getKernelContext().getModuleAddress(
165    IoUtility.toUrl(xmlFile.getAbsoluteFile()));
166  5 SaxDefaultHandler handler = new SaxDefaultHandler();
167  5 QedeqHandler simple = new QedeqHandler(handler);
168  5 handler.setBasisDocumentHandler(simple);
169  5 SaxParser parser = new SaxParser(handler);
170  5 parser.parse(xmlFile, null);
171  3 final QedeqVo qedeq = (QedeqVo) simple.getQedeq();
172  3 final InternalKernelServices services = (InternalKernelServices) IoUtility
173    .getFieldContent(KernelFacade.getKernelContext(), "services");
174  3 final QedeqFileDao loader = new XmlQedeqFileDao();
175  3 loader.setServices(services);
176  3 final DefaultKernelQedeqBo prop = (DefaultKernelQedeqBo) KernelFacade
177    .getKernelContext().getQedeqBo(context);
178  3 prop.setQedeqFileDao(loader);
179  3 IoUtility.setFieldContent(prop, "qedeq", qedeq);
180  3 prop.setLoaded(QedeqVoBuilder.createQedeq(prop.getModuleAddress(), qedeq),
181    new ModuleLabelsCreator(prop).createLabels());
182  3 prop.setLoadedRequiredModules(new KernelModuleReferenceList());
183  3 QedeqBoFormalLogicChecker.check(prop);
184    }
185   
186    }
 
CloverReport generated by Clover Code Coverage v2.3.1
Sa Aug 2 2008 13:56:32 CEST.		   Clover: Open Source License registered to qedeq.org .