Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
../../../../../../img/srcFileCovDistChart10.png 0% of files have more coverage
108   819   23   4.7
0   606   0.21   23
23     1  
1    
 
  FormulaCheckerTest       Line # 33 108 23 100% 1.0
 
No Tests
 
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   
16    package org.qedeq.kernel.bo.logic.wf;
17   
18   
19   
20    import org.qedeq.base.trace.Trace;
21    import org.qedeq.kernel.bo.logic.common.FormulaChecker;
22    import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
23    import org.qedeq.kernel.se.base.list.Element;
24    import org.qedeq.kernel.se.common.DefaultModuleAddress;
25    import org.qedeq.kernel.se.common.ModuleContext;
26    import org.qedeq.kernel.xml.parser.BasicParser;
27   
28    /**
29    * For testing the {@link org.qedeq.kernel.bo.logic.FormulaChecker}.
30    *
31    * @author Michael Meyling
32    */
 
33    public class FormulaCheckerTest extends AbstractFormulaChecker {
34   
35    /** This class. */
36    private static final Class CLASS = FormulaCheckerTest.class;
37   
38    private ModuleContext context;
39   
40    private FormulaChecker checker;
41   
 
42  21 toggle protected void setUp() throws Exception {
43  21 context = new ModuleContext(new DefaultModuleAddress("http://memory.org/sample.xml"), "getElement()");
44  21 checker = new FormulaCheckerImpl();
45    }
46   
 
47  21 toggle protected void tearDown() throws Exception {
48  21 context = null;
49    }
50   
51    /**
52    * Function: checkFormula(Element)
53    * Type: positive
54    * Data: A & A.
55    *
56    * @throws Exception Test failed.
57    */
 
58  1 toggle public void testPositive1() throws Exception {
59  1 final Element ele = BasicParser.createElement("<AND><PREDVAR id=\"A\"/><PREDVAR id=\"A\"/></AND>");
60  1 Trace.param(CLASS, this, "testPositive1", "ele", ele);
61  1 assertFalse(checker.checkFormula(ele, context).hasErrors());
62  1 assertFalse(checker.checkFormula(ele, context, getChecker()).hasErrors());
63    }
64   
65    /**
66    * Function: checkFormula(Element)
67    * Type: positive
68    * Data: (all z (isSet(z) -> (z in x <-> z in y))) -> x = y.
69    *
70    * @throws Exception Test failed.
71    */
 
72  1 toggle public void testPositive2() throws Exception {
73  1 final Element ele = BasicParser.createElement(
74    "<IMPL>"
75    + " <FORALL>"
76    + " <VAR id=\"z\"/>"
77    + " <IMPL>"
78    + " <PREDCON ref=\"isSet\">"
79    + " <VAR id=\"z\"/>"
80    + " </PREDCON>"
81    + " <EQUI>"
82    + " <PREDCON ref=\"in\">"
83    + " <VAR id=\"z\"/>"
84    + " <VAR id=\"x\"/>"
85    + " </PREDCON>"
86    + " <PREDCON ref=\"in\">"
87    + " <VAR id=\"z\"/>"
88    + " <VAR id=\"y\"/>"
89    + " </PREDCON>"
90    + " </EQUI>"
91    + " </IMPL>"
92    + " </FORALL>"
93    + " <PREDCON ref=\"equal\">"
94    + " <VAR id=\"x\"/>"
95    + " <VAR id=\"y\"/>"
96    + " </PREDCON>"
97    + "</IMPL>");
98  1 Trace.param(CLASS, this, "testPositive2", "ele", ele);
99  1 assertFalse(checker.checkFormula(ele, context).hasErrors());
100  1 assertFalse(checker.checkFormula(ele, context, getChecker()).hasErrors());
101  1 assertFalse(checker.checkFormula(ele, context, getCheckerWithoutClass())
102    .hasErrors());
103    }
104   
105    /**
106    * Function: checkFormula(Element)
107    * Type: positive
108    * Data: (all isSet(z) (z in x <-> z in y)) -> x = y.
109    *
110    * @throws Exception Test failed.
111    */
 
112  1 toggle public void testPositive3() throws Exception {
113  1 final Element ele = BasicParser.createElement(
114    "<IMPL>"
115    + " <FORALL>"
116    + " <VAR id=\"z\"/>"
117    + " <PREDCON ref=\"isSet\">"
118    + " <VAR id=\"z\"/>"
119    + " </PREDCON>"
120    + " <EQUI>"
121    + " <PREDCON ref=\"in\">"
122    + " <VAR id=\"z\"/>"
123    + " <VAR id=\"x\"/>"
124    + " </PREDCON>"
125    + " <PREDCON ref=\"in\">"
126    + " <VAR id=\"z\"/>"
127    + " <VAR id=\"y\"/>"
128    + " </PREDCON>"
129    + " </EQUI>"
130    + " </FORALL>"
131    + " <PREDCON ref=\"equal\">"
132    + " <VAR id=\"x\"/>"
133    + " <VAR id=\"y\"/>"
134    + " </PREDCON>"
135    + "</IMPL>");
136  1 Trace.param(CLASS, this, "testPositive3", "ele", ele);
137  1 assertFalse(checker.checkFormula(ele, context).hasErrors());
138  1 assertFalse(checker.checkFormula(ele, context, getChecker()).hasErrors());
139  1 assertFalse(checker.checkFormula(ele, context, getCheckerWithoutClass())
140    .hasErrors());
141    }
142   
143    /**
144    * Function: checkFormula(Element)
145    * Type: positive
146    * Data: (all z (all t isSet(t) (z in x <-> z in y))) -> x = y.
147    *
148    * @throws Exception Test failed.
149    */
 
150  1 toggle public void testPositive4() throws Exception {
151  1 final Element ele = BasicParser.createElement(
152    "<IMPL>"
153    + " <FORALL>"
154    + " <VAR id=\"z\"/>"
155    + " <FORALL>"
156    + " <VAR id=\"t\"/>"
157    + " <PREDCON ref=\"isSet\">"
158    + " <VAR id=\"t\"/>"
159    + " </PREDCON>"
160    + " <EQUI>"
161    + " <PREDCON ref=\"in\">"
162    + " <VAR id=\"z\"/>"
163    + " <VAR id=\"x\"/>"
164    + " </PREDCON>"
165    + " <PREDCON ref=\"in\">"
166    + " <VAR id=\"z\"/>"
167    + " <VAR id=\"y\"/>"
168    + " </PREDCON>"
169    + " </EQUI>"
170    + " </FORALL>"
171    + " </FORALL>"
172    + " <PREDCON ref=\"equal\">"
173    + " <VAR id=\"x\"/>"
174    + " <VAR id=\"y\"/>"
175    + " </PREDCON>"
176    + "</IMPL>");
177  1 Trace.param(CLASS, this, "testPositive4", "ele", ele);
178  1 assertFalse(checker.checkFormula(ele, context).hasErrors());
179  1 assertFalse(checker.checkFormula(ele, context, getChecker()).hasErrors());
180  1 assertFalse(checker.checkFormula(ele, context, getCheckerWithoutClass())
181    .hasErrors());
182    }
183   
184    /**
185    * Function: checkFormula(Element)
186    * Type: positive
187    * Data: (all z (all t (z in x <-> z in y))) -> (all z (all t (z in x <-> z in y)))
188    *
189    * @throws Exception Test failed.
190    */
 
191  1 toggle public void testPositive5() throws Exception {
192  1 final Element ele = BasicParser.createElement(
193    "<IMPL>"
194    + " <FORALL>"
195    + " <VAR id=\"z\"/>"
196    + " <FORALL>"
197    + " <VAR id=\"t\"/>"
198    + " <EQUI>"
199    + " <PREDCON ref=\"in\">"
200    + " <VAR id=\"z\"/>"
201    + " <VAR id=\"x\"/>"
202    + " </PREDCON>"
203    + " <PREDCON ref=\"in\">"
204    + " <VAR id=\"z\"/>"
205    + " <VAR id=\"y\"/>"
206    + " </PREDCON>"
207    + " </EQUI>"
208    + " </FORALL>"
209    + " </FORALL>"
210    + " <FORALL>"
211    + " <VAR id=\"z\"/>"
212    + " <FORALL>"
213    + " <VAR id=\"t\"/>"
214    + " <EQUI>"
215    + " <PREDCON ref=\"in\">"
216    + " <VAR id=\"z\"/>"
217    + " <VAR id=\"x\"/>"
218    + " </PREDCON>"
219    + " <PREDCON ref=\"in\">"
220    + " <VAR id=\"z\"/>"
221    + " <VAR id=\"y\"/>"
222    + " </PREDCON>"
223    + " </EQUI>"
224    + " </FORALL>"
225    + " </FORALL>"
226    + "</IMPL>");
227  1 Trace.param(CLASS, this, "testPositive5", "ele", ele);
228  1 assertFalse(checker.checkFormula(ele, context).hasErrors());
229  1 assertFalse(checker.checkFormula(ele, context, getChecker()).hasErrors());
230  1 assertFalse(checker.checkFormula(ele, context, getCheckerWithoutClass())
231    .hasErrors());
232    }
233   
234    /**
235    * Function: checkFormula(Element)
236    * Type: positive
237    * Data: (all z (all t (z in P(x) <-> z in y))) -> (all z (all t (z in x <-> z in y)))
238    *
239    * @throws Exception Test failed.
240    */
 
241  1 toggle public void testPositive6() throws Exception {
242  1 final Element ele = BasicParser.createElement(
243    "<IMPL>"
244    + " <FORALL>"
245    + " <VAR id=\"z\"/>"
246    + " <FORALL>"
247    + " <VAR id=\"t\"/>"
248    + " <EQUI>"
249    + " <PREDCON ref=\"in\">"
250    + " <VAR id=\"z\"/>"
251    + " <FUNCON ref=\"power\">"
252    + " <VAR id=\"x\"/>"
253    + " </FUNCON>"
254    + " </PREDCON>"
255    + " <PREDCON ref=\"in\">"
256    + " <VAR id=\"z\"/>"
257    + " <VAR id=\"y\"/>"
258    + " </PREDCON>"
259    + " </EQUI>"
260    + " </FORALL>"
261    + " </FORALL>"
262    + " <FORALL>"
263    + " <VAR id=\"z\"/>"
264    + " <FORALL>"
265    + " <VAR id=\"t\"/>"
266    + " <EQUI>"
267    + " <PREDCON ref=\"in\">"
268    + " <VAR id=\"z\"/>"
269    + " <VAR id=\"x\"/>"
270    + " </PREDCON>"
271    + " <PREDCON ref=\"in\">"
272    + " <VAR id=\"z\"/>"
273    + " <VAR id=\"y\"/>"
274    + " </PREDCON>"
275    + " </EQUI>"
276    + " </FORALL>"
277    + " </FORALL>"
278    + "</IMPL>");
279  1 Trace.param(CLASS, this, "testPositive6", "ele", ele);
280  1 assertFalse(checker.checkFormula(ele, context).hasErrors());
281  1 assertFalse(checker.checkFormula(ele, context, getChecker()).hasErrors());
282  1 assertFalse(checker.checkFormula(ele, context, getCheckerWithoutClass())
283    .hasErrors());
284    }
285   
286    /**
287    * Function: checkFormula(Element)
288    * Type: positive
289    * Data: y = [x | phi(x)} <-> all z (z in y <-> z in {x | phi(x)})
290    *
291    * @throws Exception Test failed.
292    */
 
293  1 toggle public void testPositive7() throws Exception {
294  1 final Element ele = BasicParser.createElement(
295    " <EQUI>"
296    + " <PREDCON ref=\"equal\">"
297    + " <VAR id=\"y\"/>"
298    + " <CLASS>"
299    + " <VAR id=\"x\"/>"
300    + " <PREDVAR id=\"\\phi\">"
301    + " <VAR id=\"x\"/>"
302    + " </PREDVAR>"
303    + " </CLASS>"
304    + " </PREDCON>"
305    + " <FORALL>"
306    + " <VAR id=\"z\"/>"
307    + " <EQUI>"
308    + " <PREDCON ref=\"in\">"
309    + " <VAR id=\"z\"/>"
310    + " <VAR id=\"y\"/>"
311    + " </PREDCON>"
312    + " <PREDCON ref=\"in\">"
313    + " <VAR id=\"z\"/>"
314    + " <CLASS>"
315    + " <VAR id=\"x\"/>"
316    + " <PREDVAR id=\"\\phi\">"
317    + " <VAR id=\"x\"/>"
318    + " </PREDVAR>"
319    + " </CLASS>"
320    + " </PREDCON>"
321    + " </EQUI>"
322    + " </FORALL>"
323    + " </EQUI>"
324    );
325  1 Trace.param(CLASS, this, "testPositive7", "ele", ele);
326  1 assertFalse(checker.checkFormula(ele, context).hasErrors());
327  1 assertFalse(checker.checkFormula(ele, context, getChecker()).hasErrors());
328    }
329   
330    /**
331    * Function: checkFormula(Element)
332    * Type: positive
333    * Data: all y (all z (phi(z) <-> z in y) -> y = {z | phi(z)})
334    *
335    * @throws Exception Test failed.
336    */
 
337  1 toggle public void testPositive8() throws Exception {
338  1 final Element ele = BasicParser.createElement(
339    "<FORALL>"
340    + " <VAR id=\"y\"/>"
341    + " <IMPL>"
342    + " <FORALL>"
343    + " <VAR id=\"z\"/>"
344    + " <EQUI>"
345    + " <PREDVAR ref=\"phi\">"
346    + " <VAR id=\"z\"/>"
347    + " </PREDVAR>"
348    + " <PREDCON ref=\"in\">"
349    + " <VAR id=\"z\"/>"
350    + " <VAR id=\"y\"/>"
351    + " </PREDCON>"
352    + " </EQUI>"
353    + " </FORALL>"
354    + " <PREDCON ref=\"equal\">"
355    + " <VAR id=\"y\"/>"
356    + " <CLASS>"
357    + " <VAR id=\"z\"/>"
358    + " <PREDVAR ref=\"phi\">"
359    + " <VAR id=\"z\"/>"
360    + " </PREDVAR>"
361    + " </CLASS>"
362    + " </PREDCON>"
363    + " </IMPL>"
364    + "</FORALL>");
365  1 Trace.param(CLASS, this, "testPositive8", "ele", ele);
366  1 assertFalse(checker.checkFormula(ele, context).hasErrors());
367  1 assertFalse(checker.checkFormula(ele, context, getChecker()).hasErrors());
368    }
369   
370    /**
371    * Function: checkFormula(Element)
372    * Type: negative, code 30550
373    * Data: (all z (all z isSet(z) (z in x <-> z in y))) -> x = y.
374    * Reason: z is quantifier variable for two times
375    *
376    * @throws Exception Test failed.
377    */
 
378  1 toggle public void testNegative1() throws Exception {
379  1 final Element ele = BasicParser.createElement(
380    "<IMPL>"
381    + " <FORALL>"
382    + " <VAR id=\"z\"/>"
383    + " <FORALL>"
384    + " <VAR id=\"z\"/>"
385    + " <PREDCON ref=\"isSet\">"
386    + " <VAR id=\"z\"/>"
387    + " </PREDCON>"
388    + " <EQUI>"
389    + " <PREDCON ref=\"in\">"
390    + " <VAR id=\"z\"/>"
391    + " <VAR id=\"x\"/>"
392    + " </PREDCON>"
393    + " <PREDCON ref=\"in\">"
394    + " <VAR id=\"z\"/>"
395    + " <VAR id=\"y\"/>"
396    + " </PREDCON>"
397    + " </EQUI>"
398    + " </FORALL>"
399    + " </FORALL>"
400    + " <PREDCON ref=\"equal\">"
401    + " <VAR id=\"x\"/>"
402    + " <VAR id=\"y\"/>"
403    + " </PREDCON>"
404    + "</IMPL>");
405  1 Trace.param(CLASS, this, "testNegative1", "ele", ele);
406  1 LogicalCheckExceptionList list =
407    checker.checkFormula(ele, context);
408  1 assertEquals(1, list.size());
409  1 assertEquals(30550, list.get(0).getErrorCode());
410    }
411   
412    /**
413    * Function: checkFormula(Element)
414    * Type: positive
415    * Data: (all z (all t isSet(z) (z in x <-> z in y))) -> x = y.
416    * Restriction formula for t contains no t but that is ok.
417    *
418    * @throws Exception Test failed.
419    */
 
420  1 toggle public void testPositive9() throws Exception {
421  1 final Element ele = BasicParser.createElement(
422    "<IMPL>"
423    + " <FORALL>"
424    + " <VAR id=\"z\"/>"
425    + " <FORALL>"
426    + " <VAR id=\"t\"/>"
427    + " <PREDCON ref=\"isSet\">"
428    + " <VAR id=\"z\"/>"
429    + " </PREDCON>"
430    + " <EQUI>"
431    + " <PREDCON ref=\"in\">"
432    + " <VAR id=\"z\"/>"
433    + " <VAR id=\"x\"/>"
434    + " </PREDCON>"
435    + " <PREDCON ref=\"in\">"
436    + " <VAR id=\"z\"/>"
437    + " <VAR id=\"y\"/>"
438    + " </PREDCON>"
439    + " </EQUI>"
440    + " </FORALL>"
441    + " </FORALL>"
442    + " <PREDCON ref=\"equal\">"
443    + " <VAR id=\"x\"/>"
444    + " <VAR id=\"y\"/>"
445    + " </PREDCON>"
446    + "</IMPL>");
447  1 Trace.param(CLASS, this, "testPositive9", "ele", ele);
448  1 assertFalse(checker.checkFormula(ele, context).hasErrors());
449    }
450   
451    /**
452    * Function: checkFormula(Element)
453    * Type: negative, code 30780
454    * Data: (all z (all x (z in x <-> z in y))) -> (all z (all t (z in x <-> z in y)))
455    * Reason: x occurs non free and free
456    *
457    * @throws Exception Test failed.
458    */
 
459  1 toggle public void testNegative3() throws Exception {
460  1 final Element ele = BasicParser.createElement(
461    "<IMPL>"
462    + " <FORALL>"
463    + " <VAR id=\"z\"/>"
464    + " <FORALL>"
465    + " <VAR id=\"x\"/>"
466    + " <EQUI>"
467    + " <PREDCON ref=\"in\">"
468    + " <VAR id=\"z\"/>"
469    + " <VAR id=\"x\"/>"
470    + " </PREDCON>"
471    + " <PREDCON ref=\"in\">"
472    + " <VAR id=\"z\"/>"
473    + " <VAR id=\"y\"/>"
474    + " </PREDCON>"
475    + " </EQUI>"
476    + " </FORALL>"
477    + " </FORALL>"
478    + " <FORALL>"
479    + " <VAR id=\"z\"/>"
480    + " <FORALL>"
481    + " <VAR id=\"t\"/>"
482    + " <EQUI>"
483    + " <PREDCON ref=\"in\">"
484    + " <VAR id=\"z\"/>"
485    + " <VAR id=\"x\"/>"
486    + " </PREDCON>"
487    + " <PREDCON ref=\"in\">"
488    + " <VAR id=\"z\"/>"
489    + " <VAR id=\"y\"/>"
490    + " </PREDCON>"
491    + " </EQUI>"
492    + " </FORALL>"
493    + " </FORALL>"
494    + "</IMPL>");
495  1 Trace.param(CLASS, this, "testNegative3", "ele", ele);
496  1 LogicalCheckExceptionList list =
497    checker.checkFormula(ele, context);
498  1 assertEquals(1, list.size());
499  1 assertEquals(30780, list.get(0).getErrorCode());
500    }
501   
502    /**
503    * Function: checkFormula(Element)
504    * Type: negative, code 30780
505    * Data: (all x (all y (all z (z in x <-> z in y)) -> (z = y)))
506    * Reason: z occurs non free and free
507    *
508    * @throws Exception Test failed.
509    */
 
510  1 toggle public void testNegative4() throws Exception {
511  1 final Element ele = BasicParser.createElement(
512    "<FORALL>"
513    + " <VAR id=\"x\"/>"
514    + " <FORALL>"
515    + " <VAR id=\"y\"/>"
516    + " <IMPL>"
517    + " <FORALL>"
518    + " <VAR id=\"z\"/>"
519    + " <EQUI>"
520    + " <PREDCON ref=\"in\">"
521    + " <VAR id=\"z\"/>"
522    + " <VAR id=\"x\"/>"
523    + " </PREDCON>"
524    + " <PREDCON ref=\"in\">"
525    + " <VAR id=\"z\"/>"
526    + " <VAR id=\"y\"/>"
527    + " </PREDCON>"
528    + " </EQUI>"
529    + " </FORALL>"
530    + " <PREDCON ref=\"equal\">"
531    + " <VAR id=\"z\"/>"
532    + " <VAR id=\"y\"/>"
533    + " </PREDCON>"
534    + " </IMPL>"
535    + " </FORALL>"
536    + "</FORALL>"
537    );
538  1 Trace.param(CLASS, this, "testNegative4", "ele", ele);
539  1 LogicalCheckExceptionList list =
540    checker.checkFormula(ele, context);
541  1 assertEquals(1, list.size());
542  1 assertEquals(30780, list.get(0).getErrorCode());
543    }
544   
545    /**
546    * Function: checkFormula(Element)
547    * Type: negative, code 30780
548    * Data: (all x (all y (all z (z in x <-> z in y))) -> (x = y))
549    * Reason: y occurs non free and free
550    *
551    * @throws Exception Test failed.
552    */
 
553  1 toggle public void testNegative5() throws Exception {
554  1 final Element ele = BasicParser.createElement(
555    "<FORALL>"
556    + " <VAR id=\"x\"/>"
557    + " <IMPL>"
558    + " <FORALL>"
559    + " <VAR id=\"y\"/>"
560    + " <FORALL>"
561    + " <VAR id=\"z\"/>"
562    + " <EQUI>"
563    + " <PREDCON ref=\"in\">"
564    + " <VAR id=\"z\"/>"
565    + " <VAR id=\"x\"/>"
566    + " </PREDCON>"
567    + " <PREDCON ref=\"in\">"
568    + " <VAR id=\"z\"/>"
569    + " <VAR id=\"y\"/>"
570    + " </PREDCON>"
571    + " </EQUI>"
572    + " </FORALL>"
573    + " </FORALL>"
574    + " <PREDCON ref=\"equal\">"
575    + " <VAR id=\"x\"/>"
576    + " <VAR id=\"y\"/>"
577    + " </PREDCON>"
578    + " </IMPL>"
579    + "</FORALL>"
580    );
581  1 Trace.param(CLASS, this, "testNegative5", "ele", ele);
582  1 LogicalCheckExceptionList list =
583    checker.checkFormula(ele, context);
584  1 assertEquals(1, list.size());
585  1 assertEquals(30780, list.get(0).getErrorCode());
586    }
587   
588    /**
589    * Function: checkFormula(Element)
590    * Type: negative, code 30770
591    * Data: (all x ((x = y) -> all y (all z (z in x <-> z in y))))
592    * Reason: y occurs free and non free
593    *
594    * @throws Exception Test failed.
595    */
 
596  1 toggle public void testNegative6() throws Exception {
597  1 final Element ele = BasicParser.createElement(
598    "<FORALL>"
599    + " <VAR id=\"x\"/>"
600    + " <IMPL>"
601    + " <PREDCON ref=\"equal\">"
602    + " <VAR id=\"x\"/>"
603    + " <VAR id=\"y\"/>"
604    + " </PREDCON>"
605    + " <FORALL>"
606    + " <VAR id=\"y\"/>"
607    + " <FORALL>"
608    + " <VAR id=\"z\"/>"
609    + " <EQUI>"
610    + " <PREDCON ref=\"in\">"
611    + " <VAR id=\"z\"/>"
612    + " <VAR id=\"x\"/>"
613    + " </PREDCON>"
614    + " <PREDCON ref=\"in\">"
615    + " <VAR id=\"z\"/>"
616    + " <VAR id=\"y\"/>"
617    + " </PREDCON>"
618    + " </EQUI>"
619    + " </FORALL>"
620    + " </FORALL>"
621    + " </IMPL>"
622    + "</FORALL>"
623    );
624  1 Trace.param(CLASS, this, "testNegative6", "ele", ele);
625  1 LogicalCheckExceptionList list =
626    checker.checkFormula(ele, context);
627  1 assertEquals(1, list.size());
628  1 assertEquals(30770, list.get(0).getErrorCode());
629    }
630   
631    /**
632    * Function: checkFormula(Element)
633    * Type: negative, code 30740
634    * Data: (x = y) ->
635    * Reason: second operand missing
636    *
637    * @throws Exception Test failed.
638    */
 
639  1 toggle public void testNegative7() throws Exception {
640  1 final Element ele = BasicParser.createElement(
641    "<IMPL>"
642    + " <PREDCON ref=\"equal\">"
643    + " <VAR id=\"x\"/>"
644    + " <VAR id=\"y\"/>"
645    + " </PREDCON>"
646    + "</IMPL>"
647    );
648  1 Trace.param(CLASS, this, "testNegative7", "ele", ele);
649  1 LogicalCheckExceptionList list =
650    checker.checkFormula(ele, context);
651  1 assertEquals(1, list.size());
652  1 assertEquals(30740, list.get(0).getErrorCode());
653    }
654   
655    /**
656    * Function: checkFormula(Element)
657    * Type: negative, code 30530
658    * Data: x -> y
659    * Reason: x and y are no formulas
660    *
661    * @throws Exception Test failed.
662    */
 
663  1 toggle public void testNegative8() throws Exception {
664  1 final Element ele = BasicParser.createElement(
665    "<IMPL>"
666    + " <VAR id=\"x\"/>"
667    + " <VAR id=\"y\"/>"
668    + "</IMPL>"
669    );
670  1 Trace.param(CLASS, this, "testNegative8", "ele", ele);
671  1 LogicalCheckExceptionList list =
672    checker.checkFormula(ele, context);
673    // System.out.println(list);
674  1 assertEquals(2, list.size());
675  1 assertEquals(30530, list.get(0).getErrorCode());
676  1 assertEquals(30530, list.get(1).getErrorCode());
677    }
678   
679    /**
680    * Function: checkFormula(Element)
681    * Type: negative, code 30530
682    * Data: UIMPL(x, y)
683    * Reason: UIMPL is an unknown logical operator
684    *
685    * @throws Exception Test failed.
686    */
 
687  1 toggle public void testNegative9() throws Exception {
688  1 final Element ele = BasicParser.createElement(
689    "<UIMPL>"
690    + " <VAR id=\"x\"/>"
691    + " <VAR id=\"y\"/>"
692    + "</UIMPL>"
693    );
694  1 Trace.param(CLASS, this, "testNegative9", "ele", ele);
695  1 LogicalCheckExceptionList list =
696    checker.checkFormula(ele, context);
697  1 assertEquals(1, list.size());
698  1 assertEquals(30530, list.get(0).getErrorCode());
699    }
700   
701    /**
702    * Function: checkFormula(Element)
703    * Type: negative, code 30620
704    * Data: sirup(x, unknown(y))
705    * Reason: "unknown" is an unknown term operator
706    *
707    * @throws Exception Test failed.
708    */
 
709  1 toggle public void testNegative10() throws Exception {
710  1 final Element ele = BasicParser.createElement(
711    "<PREDVAR id=\"sirup\">"
712    + " <VAR id=\"x\"/>"
713    + " <unknown id=\"y\"/>"
714    + "</PREDVAR>"
715    );
716  1 Trace.param(CLASS, this, "testNegative10", "ele", ele);
717  1 LogicalCheckExceptionList list =
718    checker.checkFormula(ele, context);
719  1 assertEquals(1, list.size());
720  1 assertEquals(30620, list.get(0).getErrorCode());
721    }
722   
723    /**
724    * Function: checkFormula(Element)
725    * Type: negative, code 30590
726    * Data: x union unknown(y)
727    * Reason: "and" is an unknown predicate constant
728    *
729    * @throws Exception Test failed.
730    */
 
731  1 toggle public void testNegative11() throws Exception {
732  1 final Element ele = BasicParser.createElement(
733    "<PREDCON ref=\"and\">"
734    + " <VAR id=\"x\"/>"
735    + " <FUNCON ref=\"power\">"
736    + " <VAR id=\"y\"/>"
737    + " </FUNCON>"
738    + "</PREDCON>"
739    );
740  1 Trace.param(CLASS, this, "testNegative11", "ele", ele);
741  1 checker.checkFormula(ele, context);
742  1 LogicalCheckExceptionList list =
743    checker.checkFormula(ele, context, getChecker());
744  1 assertEquals(1, list.size());
745  1 assertEquals(30590, list.get(0).getErrorCode());
746    }
747   
748    /**
749    * Function: checkTerm(Element)
750    * Type: negative, code 30690
751    * Data: x union unknown(y)
752    * Reason: "unknown" is an unknown term operator
753    *
754    * @throws Exception Test failed.
755    */
 
756  1 toggle public void testNegative12() throws Exception {
757  1 final Element ele = BasicParser.createElement(
758    "<FUNCON ref=\"union\">"
759    + " <VAR id=\"x\"/>"
760    + " <FUNCON ref=\"unknown\">"
761    + " <VAR id=\"y\"/>"
762    + " </FUNCON>"
763    + "</FUNCON>"
764    );
765  1 Trace.param(CLASS, this, "testNegative12", "ele", ele);
766  1 checker.checkTerm(ele, context);
767  1 LogicalCheckExceptionList list =
768    checker.checkTerm(ele, context, getChecker());
769  1 assertEquals(1, list.size());
770  1 assertEquals(30690, list.get(0).getErrorCode());
771    }
772   
773    /**
774    * Function: checkFormula(Element)
775    * Type: negative, code 30680
776    * Data: all y (all z (phi(z) <-> z in y) -> y = {z | phi(z)})
777    * Reason: "{ .. }" is an unknown term operator
778    *
779    * @throws Exception Test failed.
780    */
 
781  1 toggle public void testNegative13() throws Exception {
782  1 final Element ele = BasicParser.createElement(
783    "<FORALL>"
784    + " <VAR id=\"y\"/>"
785    + " <IMPL>"
786    + " <FORALL>"
787    + " <VAR id=\"z\"/>"
788    + " <EQUI>"
789    + " <PREDVAR ref=\"phi\">"
790    + " <VAR id=\"z\"/>"
791    + " </PREDVAR>"
792    + " <PREDCON ref=\"in\">"
793    + " <VAR id=\"z\"/>"
794    + " <VAR id=\"y\"/>"
795    + " </PREDCON>"
796    + " </EQUI>"
797    + " </FORALL>"
798    + " <PREDCON ref=\"equal\">"
799    + " <VAR id=\"y\"/>"
800    + " <CLASS>"
801    + " <VAR id=\"z\"/>"
802    + " <PREDVAR ref=\"phi\">"
803    + " <VAR id=\"z\"/>"
804    + " </PREDVAR>"
805    + " </CLASS>"
806    + " </PREDCON>"
807    + " </IMPL>"
808    + "</FORALL>"
809    );
810  1 Trace.param(CLASS, this, "testNegative13", "ele", ele);
811  1 checker.checkFormula(ele, context);
812  1 checker.checkFormula(ele, context, getChecker());
813  1 LogicalCheckExceptionList list =
814    checker.checkFormula(ele, context, getCheckerWithoutClass());
815  1 assertEquals(1, list.size());
816  1 assertEquals(30680, list.get(0).getErrorCode());
817    }
818   
819    }
 
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 .