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