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