1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
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 |
|
|
27 |
|
|
28 |
|
@author |
29 |
|
|
|
|
| 96.3% |
Uncovered Elements: 8 (214) |
Complexity: 11 |
Complexity Density: 0.05 |
|
30 |
|
public class FormalProofCheckerPluginTest extends QedeqBoTestCase { |
31 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
32 |
0
|
public FormalProofCheckerPluginTest() {... |
33 |
0
|
super(); |
34 |
|
} |
35 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
36 |
4
|
public FormalProofCheckerPluginTest(final String name) {... |
37 |
4
|
super(name); |
38 |
|
} |
39 |
|
|
|
|
| 60% |
Uncovered Elements: 6 (15) |
Complexity: 4 |
Complexity Density: 0.44 |
|
40 |
76
|
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 |
|
} |
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
55 |
76
|
private String getArea(final SourceFileException e) {... |
56 |
76
|
return getArea(e.toString()); |
57 |
|
} |
58 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (6) |
Complexity: 1 |
Complexity Density: 0.17 |
1
PASS
|
|
59 |
1
|
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 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (42) |
Complexity: 1 |
Complexity Density: 0.02 |
1
PASS
|
|
69 |
1
|
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 |
|
|
82 |
|
|
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 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (134) |
Complexity: 1 |
Complexity Density: 0.01 |
1
PASS
|
|
117 |
1
|
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 |
|
|
133 |
|
|
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 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (6) |
Complexity: 1 |
Complexity Density: 0.17 |
1
PASS
|
|
261 |
1
|
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 |
|
} |