Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
200   271   11   25
6   236   0.05   8
8     1.38  
1    
 
  FormalProofCheckerPluginTest       Line # 30 200 11 96.3% 0.9626168
 
  (4)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, 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    package org.qedeq.kernel.bo.service.logic;
16   
17    import java.io.File;
18   
19    import org.qedeq.kernel.bo.common.QedeqBo;
20    import org.qedeq.kernel.bo.test.QedeqBoTestCase;
21    import org.qedeq.kernel.se.common.DefaultModuleAddress;
22    import org.qedeq.kernel.se.common.ModuleAddress;
23    import org.qedeq.kernel.se.common.SourceFileException;
24   
25    /**
26    * Test the formal proof checker plugin.
27    *
28    * @author Michael Meyling
29    */
 
30    public class FormalProofCheckerPluginTest extends QedeqBoTestCase {
31   
 
32  0 toggle public FormalProofCheckerPluginTest() {
33  0 super();
34    }
35   
 
36  4 toggle public FormalProofCheckerPluginTest(final String name) {
37  4 super(name);
38    }
39   
 
40  76 toggle private String getArea(final String text) {
41  76 if (text == null) {
42  0 return "";
43    }
44  76 final int p = text.indexOf(".xml:");
45  76 if (p < 0) {
46  0 return text;
47    }
48  76 int n = text.indexOf("\n");
49  76 if (n < 0) {
50  0 n = text.length();
51    }
52  76 return text.substring(p + ".xml:".length(), n);
53   
54    }
 
55  76 toggle private String getArea(final SourceFileException e) {
56  76 return getArea(e.toString());
57    }
58   
 
59  1 toggle public void testPlugin() throws Exception {
60  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
61    "sample/qedeq_sample3.xml"));
62  1 getServices().checkFormallyProved(address);
63  1 final QedeqBo bo = getServices().getQedeqBo(address);
64  1 assertTrue(bo.isWellFormed());
65  1 assertEquals(0, bo.getWarnings().size());
66  1 assertEquals(0, bo.getErrors().size());
67    }
68   
 
69  1 toggle public void testPlugin2() throws Exception {
70  1 final ModuleAddress address = new DefaultModuleAddress(new File(getIndir(),
71    "proof/proof_001.xml"));
72  1 getServices().checkWellFormedness(address);
73  1 final QedeqBo bo = getServices().getQedeqBo(address);
74  1 assertTrue(bo.isWellFormed());
75  1 assertEquals(0, bo.getWarnings().size());
76  1 assertEquals(0, bo.getErrors().size());
77  1 getServices().checkFormallyProved(address);
78  1 assertTrue(bo.isWellFormed());
79  1 assertEquals(0, bo.getWarnings().size());
80  1 assertEquals(16, bo.getErrors().size());
81    // System.out.println("testPlugin2");
82    // bo.getErrors().printStackTrace(System.out);
83  1 assertEquals(37140, bo.getErrors().get(0).getErrorCode());
84  1 assertEquals("1067:32:1067:38", getArea(bo.getErrors().get(0)));
85  1 assertEquals(37140, bo.getErrors().get(1).getErrorCode());
86  1 assertEquals("1133:25:1135:35", getArea(bo.getErrors().get(1)));
87  1 assertEquals(37180, bo.getErrors().get(2).getErrorCode());
88  1 assertEquals("1353:33:1353:41", getArea(bo.getErrors().get(2)));
89  1 assertEquals(37150, bo.getErrors().get(3).getErrorCode());
90  1 assertEquals("1461:20:1461:30", getArea(bo.getErrors().get(3)));
91  1 assertEquals(37240, bo.getErrors().get(4).getErrorCode());
92  1 assertEquals("979:13:1002:23", getArea(bo.getErrors().get(4)));
93  1 assertEquals(37150, bo.getErrors().get(5).getErrorCode());
94  1 assertEquals("1945:20:1945:30", getArea(bo.getErrors().get(5)));
95  1 assertEquals(37140, bo.getErrors().get(6).getErrorCode());
96  1 assertEquals("1960:25:1966:34", getArea(bo.getErrors().get(6)));
97  1 assertEquals(37150, bo.getErrors().get(7).getErrorCode());
98  1 assertEquals("1974:20:1974:30", getArea(bo.getErrors().get(7)));
99  1 assertEquals(37140, bo.getErrors().get(8).getErrorCode());
100  1 assertEquals("1987:23:1996:32", getArea(bo.getErrors().get(8)));
101  1 assertEquals(37240, bo.getErrors().get(9).getErrorCode());
102  1 assertEquals("1497:13:1520:23", getArea(bo.getErrors().get(9)));
103  1 assertEquals(37150, bo.getErrors().get(10).getErrorCode());
104  1 assertEquals("2151:20:2151:29", getArea(bo.getErrors().get(10)));
105  1 assertEquals(37240, bo.getErrors().get(11).getErrorCode());
106  1 assertEquals("2040:13:2057:23", getArea(bo.getErrors().get(11)));
107  1 assertEquals(37140, bo.getErrors().get(12).getErrorCode());
108  1 assertEquals("2233:30:2233:36", getArea(bo.getErrors().get(12)));
109  1 assertEquals(37140, bo.getErrors().get(13).getErrorCode());
110  1 assertEquals("2282:27:2284:36", getArea(bo.getErrors().get(13)));
111  1 assertEquals(37200, bo.getErrors().get(14).getErrorCode());
112  1 assertEquals("2310:21:2329:28", getArea(bo.getErrors().get(14)));
113  1 assertEquals(37240, bo.getErrors().get(15).getErrorCode());
114  1 assertEquals("2186:13:2201:23", getArea(bo.getErrors().get(15)));
115    }
116   
 
117  1 toggle public void testPlugin3() throws Exception {
118  1 final ModuleAddress address = new DefaultModuleAddress(new File(getIndir(),
119    "proof/proof_002.xml"));
120  1 final boolean locationFailures = "true".equalsIgnoreCase(
121    System.getProperty("qedeq.test.xmlLocationFailures", "false"));
122  1 System.setProperty("qedeq.test.xmlLocationFailures", "false");
123  1 try {
124  1 getServices().checkWellFormedness(address);
125  1 final QedeqBo bo = getServices().getQedeqBo(address);
126  1 assertTrue(bo.isWellFormed());
127  1 assertEquals(0, bo.getWarnings().size());
128  1 assertEquals(0, bo.getErrors().size());
129  1 getServices().checkFormallyProved(address);
130  1 assertTrue(bo.isWellFormed());
131  1 assertEquals(0, bo.getWarnings().size());
132    // System.out.println("testPlugin3");
133    // bo.getErrors().printStackTrace(System.out);
134  1 assertEquals(37220, bo.getErrors().get(0).getErrorCode());
135  1 assertEquals("522:19:522:24", getArea(bo.getErrors().get(0)));
136  1 assertEquals(37210, bo.getErrors().get(1).getErrorCode());
137  1 assertEquals("535:19:537:35", getArea(bo.getErrors().get(1)));
138  1 assertEquals(37130, bo.getErrors().get(2).getErrorCode());
139  1 assertEquals("550:24:550:69", getArea(bo.getErrors().get(2)));
140  1 assertEquals(37130, bo.getErrors().get(3).getErrorCode());
141  1 assertEquals("572:24:572:56", getArea(bo.getErrors().get(3)));
142  1 assertEquals(37140, bo.getErrors().get(4).getErrorCode());
143  1 assertEquals("578:34:578:40", getArea(bo.getErrors().get(4)));
144  1 assertEquals(37210, bo.getErrors().get(5).getErrorCode());
145  1 assertEquals("620:19:621:35", getArea(bo.getErrors().get(5)));
146  1 assertEquals(37160, bo.getErrors().get(6).getErrorCode());
147  1 assertEquals("643:19:643:33", getArea(bo.getErrors().get(6)));
148  1 assertEquals(37160, bo.getErrors().get(7).getErrorCode());
149  1 assertEquals("676:19:676:33", getArea(bo.getErrors().get(7)));
150  1 assertEquals(37160, bo.getErrors().get(8).getErrorCode());
151  1 assertEquals("704:19:704:32", getArea(bo.getErrors().get(8)));
152  1 assertEquals(37160, bo.getErrors().get(9).getErrorCode());
153  1 assertEquals("714:23:714:31", getArea(bo.getErrors().get(9)));
154  1 assertEquals(37160, bo.getErrors().get(10).getErrorCode());
155  1 assertEquals("714:19:714:32", getArea(bo.getErrors().get(10)));
156  1 assertEquals(37240, bo.getErrors().get(11).getErrorCode());
157  1 assertEquals("503:13:508:23", getArea(bo.getErrors().get(11)));
158  1 assertEquals(37160, bo.getErrors().get(12).getErrorCode());
159  1 assertEquals("819:19:819:35", getArea(bo.getErrors().get(12)));
160  1 assertEquals(37160, bo.getErrors().get(13).getErrorCode());
161  1 assertEquals("952:19:952:24", getArea(bo.getErrors().get(13)));
162  1 assertEquals(37240, bo.getErrors().get(14).getErrorCode());
163  1 assertEquals("722:13:737:23", getArea(bo.getErrors().get(14)));
164  1 assertEquals(37130, bo.getErrors().get(15).getErrorCode());
165  1 assertEquals("1020:24:1020:59", getArea(bo.getErrors().get(15)));
166  1 assertEquals(37140, bo.getErrors().get(16).getErrorCode());
167  1 assertEquals("1032:30:1032:36", getArea(bo.getErrors().get(16)));
168  1 assertEquals(37160, bo.getErrors().get(17).getErrorCode());
169  1 assertEquals("1058:19:1058:41", getArea(bo.getErrors().get(17)));
170  1 assertEquals(37160, bo.getErrors().get(18).getErrorCode());
171  1 assertEquals("1080:34:1080:43", getArea(bo.getErrors().get(18)));
172  1 assertEquals(37140, bo.getErrors().get(19).getErrorCode());
173  1 assertEquals("1110:30:1110:36", getArea(bo.getErrors().get(19)));
174  1 assertEquals(37140, bo.getErrors().get(20).getErrorCode());
175  1 assertEquals("1126:23:1129:33", getArea(bo.getErrors().get(20)));
176  1 assertEquals(37160, bo.getErrors().get(21).getErrorCode());
177  1 assertEquals("1195:19:1195:34", getArea(bo.getErrors().get(21)));
178  1 assertEquals(37160, bo.getErrors().get(22).getErrorCode());
179  1 assertEquals("1235:19:1235:33", getArea(bo.getErrors().get(22)));
180  1 assertEquals(37210, bo.getErrors().get(23).getErrorCode());
181  1 assertEquals("1297:19:1299:35", getArea(bo.getErrors().get(23)));
182  1 assertEquals(37160, bo.getErrors().get(24).getErrorCode());
183  1 assertEquals("1336:19:1336:33", getArea(bo.getErrors().get(24)));
184  1 assertEquals(37160, bo.getErrors().get(25).getErrorCode());
185  1 assertEquals("1358:19:1358:24", getArea(bo.getErrors().get(25)));
186  1 assertEquals(37270, bo.getErrors().get(26).getErrorCode());
187  1 assertEquals("1382:19:1384:33", getArea(bo.getErrors().get(26)));
188  1 assertEquals(37270, bo.getErrors().get(27).getErrorCode());
189  1 assertEquals("1411:19:1413:31", getArea(bo.getErrors().get(27)));
190  1 assertEquals(37140, bo.getErrors().get(28).getErrorCode());
191  1 assertEquals("1429:30:1429:36", getArea(bo.getErrors().get(28)));
192  1 assertEquals(37150, bo.getErrors().get(29).getErrorCode());
193  1 assertEquals("1444:20:1444:30", getArea(bo.getErrors().get(29)));
194  1 assertEquals(37160, bo.getErrors().get(30).getErrorCode());
195  1 assertEquals("1470:19:1470:28", getArea(bo.getErrors().get(30)));
196  1 assertEquals(37240, bo.getErrors().get(31).getErrorCode());
197  1 assertEquals("979:13:1002:23", getArea(bo.getErrors().get(31)));
198  1 assertEquals(37160, bo.getErrors().get(32).getErrorCode());
199  1 assertEquals("1535:19:1535:32", getArea(bo.getErrors().get(32)));
200  1 assertEquals(37140, bo.getErrors().get(33).getErrorCode());
201  1 assertEquals("1541:30:1541:36", getArea(bo.getErrors().get(33)));
202  1 assertEquals(37160, bo.getErrors().get(34).getErrorCode());
203  1 assertEquals("1573:19:1573:33", getArea(bo.getErrors().get(34)));
204  1 assertEquals(37160, bo.getErrors().get(35).getErrorCode());
205  1 assertEquals("1605:19:1605:33", getArea(bo.getErrors().get(35)));
206  1 assertEquals(37140, bo.getErrors().get(36).getErrorCode());
207  1 assertEquals("1627:32:1627:38", getArea(bo.getErrors().get(36)));
208  1 assertEquals(37210, bo.getErrors().get(37).getErrorCode());
209  1 assertEquals("1693:19:1694:35", getArea(bo.getErrors().get(37)));
210  1 assertEquals(37160, bo.getErrors().get(38).getErrorCode());
211  1 assertEquals("1734:34:1734:45", getArea(bo.getErrors().get(38)));
212  1 assertEquals(37160, bo.getErrors().get(39).getErrorCode());
213  1 assertEquals("1800:19:1800:35", getArea(bo.getErrors().get(39)));
214  1 assertEquals(37160, bo.getErrors().get(40).getErrorCode());
215  1 assertEquals("1843:23:1843:36", getArea(bo.getErrors().get(40)));
216  1 assertEquals(37160, bo.getErrors().get(41).getErrorCode());
217  1 assertEquals("1843:37:1843:49", getArea(bo.getErrors().get(41)));
218  1 assertEquals(37270, bo.getErrors().get(42).getErrorCode());
219  1 assertEquals("1889:19:1890:31", getArea(bo.getErrors().get(42)));
220  1 assertEquals(37150, bo.getErrors().get(43).getErrorCode());
221  1 assertEquals("1892:20:1892:30", getArea(bo.getErrors().get(43)));
222  1 assertEquals(37270, bo.getErrors().get(44).getErrorCode());
223  1 assertEquals("1918:19:1919:31", getArea(bo.getErrors().get(44)));
224  1 assertEquals(37150, bo.getErrors().get(45).getErrorCode());
225  1 assertEquals("1921:20:1921:30", getArea(bo.getErrors().get(45)));
226  1 assertEquals(37140, bo.getErrors().get(46).getErrorCode());
227  1 assertEquals("1934:23:1943:32", getArea(bo.getErrors().get(46)));
228  1 assertEquals(37160, bo.getErrors().get(47).getErrorCode());
229  1 assertEquals("1976:19:1976:26", getArea(bo.getErrors().get(47)));
230  1 assertEquals(37240, bo.getErrors().get(48).getErrorCode());
231  1 assertEquals("1478:13:1501:23", getArea(bo.getErrors().get(48)));
232  1 assertEquals(37140, bo.getErrors().get(49).getErrorCode());
233  1 assertEquals("2033:25:2035:34", getArea(bo.getErrors().get(49)));
234  1 assertEquals(37160, bo.getErrors().get(50).getErrorCode());
235  1 assertEquals("2065:19:2065:34", getArea(bo.getErrors().get(50)));
236  1 assertEquals(37160, bo.getErrors().get(51).getErrorCode());
237  1 assertEquals("2087:19:2087:29", getArea(bo.getErrors().get(51)));
238  1 assertEquals(37150, bo.getErrors().get(52).getErrorCode());
239  1 assertEquals("2091:20:2091:29", getArea(bo.getErrors().get(52)));
240  1 assertEquals(37240, bo.getErrors().get(53).getErrorCode());
241  1 assertEquals("1987:13:2004:23", getArea(bo.getErrors().get(53)));
242  1 assertEquals(37130, bo.getErrors().get(54).getErrorCode());
243  1 assertEquals("2161:24:2161:45", getArea(bo.getErrors().get(54)));
244  1 assertEquals(37140, bo.getErrors().get(55).getErrorCode());
245  1 assertEquals("2173:30:2173:36", getArea(bo.getErrors().get(55)));
246  1 assertEquals(37140, bo.getErrors().get(56).getErrorCode());
247  1 assertEquals("2222:27:2224:36", getArea(bo.getErrors().get(56)));
248  1 assertEquals(37140, bo.getErrors().get(57).getErrorCode());
249  1 assertEquals("2254:35:2254:41", getArea(bo.getErrors().get(57)));
250  1 assertEquals(37200, bo.getErrors().get(58).getErrorCode());
251  1 assertEquals("2250:21:2269:28", getArea(bo.getErrors().get(58)));
252  1 assertEquals(37240, bo.getErrors().get(59).getErrorCode());
253  1 assertEquals("2126:13:2141:23", getArea(bo.getErrors().get(59)));
254  1 assertEquals(60, bo.getErrors().size());
255    } finally {
256  1 System.setProperty("qedeq.test.xmlLocationFailures",
257    Boolean.toString(locationFailures));
258    }
259    }
260   
 
261  1 toggle public void testPlugin4() throws Exception {
262  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
263    "math/qedeq_formal_logic_v1.xml"));
264  1 getServices().checkFormallyProved(address);
265  1 final QedeqBo bo = getServices().getQedeqBo(address);
266  1 assertTrue(bo.isWellFormed());
267  1 assertEquals(0, bo.getWarnings().size());
268  1 assertEquals(0, bo.getErrors().size());
269    }
270   
271    }
 
CloverReport generated by Clover Code Coverage v3.1.10
Fri May 24 2013 13:47:32 UTC.		   Clover: Open Source License registered to qedeq.org .