Clover Coverage Report
Coverage timestamp: Sat Sep 18 2010 04:09:52 UTC
../../../../../../img/srcFileCovDistChart10.png 0% of files have more coverage
34   238   10   3.4
0   131   0.29   10
10     1  
1    
 
  FormulaCheckerClassTermTest       Line # 30 34 10 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    import org.qedeq.kernel.base.list.Element;
19    import org.qedeq.kernel.bo.logic.FormulaChecker;
20    import org.qedeq.kernel.common.DefaultModuleAddress;
21    import org.qedeq.kernel.common.ModuleContext;
22   
23    /**
24    * For testing the {@link org.qedeq.kernel.bo.logic.FormulaChecker}.
25    * Testing formulas made of class terms.
26    *
27    * @version $Revision: 1.1 $
28    * @author Michael Meyling
29    */
 
30    public class FormulaCheckerClassTermTest extends AbstractFormulaChecker {
31   
32    /** For module access. */
33    private ModuleContext context;
34   
 
35  8 toggle protected void setUp() throws Exception {
36  8 context = new ModuleContext(new DefaultModuleAddress("http://memory.org/sample.xml"),
37    "getElement()");
38    }
39   
 
40  8 toggle protected void tearDown() throws Exception {
41  8 context = null;
42    }
43   
44    /**
45    * Function: checkTerm(Element).
46    * Type: positive
47    * Data: {x | A}
48    *
49    * @throws Exception Test failed.
50    */
 
51  1 toggle public void testClassTermPositive01() throws Exception {
52  1 final Element ele = TestParser.createElement(
53    "<CLASS><VAR id=\"x\" /><PREDVAR id=\"A\" /></CLASS>");
54    // System.out.println(ele.toString());
55   
56  1 assertFalse(FormulaChecker.checkTerm(ele, context).hasErrors());
57  1 assertFalse(FormulaChecker.checkTerm(ele, context, getChecker()).hasErrors());
58    }
59   
60    /**
61    * Function: checkTerm(Element).
62    * Type: positive
63    * Data: {x | phi(y, x)}
64    *
65    * @throws Exception Test failed.
66    */
 
67  1 toggle public void testClassTermPositive02() throws Exception {
68  1 final Element ele = TestParser.createElement(
69    "<CLASS>" +
70    " <VAR id=\"x\" />" +
71    " <PREDVAR id=\"phi\">" +
72    " <VAR id=\"y\" />" +
73    " <VAR id=\"x\" />" +
74    " </PREDVAR>" +
75    "</CLASS>");
76   
77    // System.out.println(ele.toString());
78  1 assertFalse(FormulaChecker.checkTerm(ele, context).hasErrors());
79  1 assertFalse(FormulaChecker.checkTerm(ele, context, getChecker()).hasErrors());
80    }
81   
82    /**
83    * Function: checkTerm(Element).
84    * Type: positive
85    * Data: {x | forall y phi(y, x)}
86    *
87    * @throws Exception Test failed.
88    */
 
89  1 toggle public void testClassTermPositive03() throws Exception {
90  1 final Element ele = TestParser.createElement(
91    "<CLASS>" +
92    " <VAR id=\"x\" />" +
93    " <FORALL>" +
94    " <VAR id=\"y\" />" +
95    " <PREDVAR id=\"phi\">" +
96    " <VAR id=\"y\" />" +
97    " <VAR id=\"x\" />" +
98    " </PREDVAR>" +
99    " </FORALL>" +
100    "</CLASS>");
101    // System.out.println(ele.toString());
102   
103  1 assertFalse(FormulaChecker.checkTerm(ele, context).hasErrors());
104  1 assertFalse(FormulaChecker.checkTerm(ele, context, getChecker()).hasErrors());
105    }
106   
107    /**
108    * Function: checkTerm(Element).
109    * Type: negative, code 30760, exactly two arguments expected
110    * Data: {x | phi(y, x) | phi(y, x)}
111    *
112    * @throws Exception Test failed.
113    */
 
114  1 toggle public void testClassTermNegative01() throws Exception {
115  1 final Element ele = TestParser.createElement(
116    "<CLASS>" +
117    " <VAR id=\"x\" />" +
118    " <PREDVAR id=\"phi\">" +
119    " <VAR id=\"y\" />" +
120    " <VAR id=\"x\" />" +
121    " </PREDVAR>" +
122    " <PREDVAR id=\"phi\">" +
123    " <VAR id=\"y\" />" +
124    " <VAR id=\"x\" />" +
125    " </PREDVAR>" +
126    "</CLASS>");
127    // System.out.println(ele.toString());
128   
129  1 LogicalCheckExceptionList list =
130    FormulaChecker.checkTerm(ele, context, getChecker());
131  1 assertEquals(1, list.size());
132  1 assertEquals(30760, list.get(0).getErrorCode());
133    }
134   
135    /**
136    * Function: checkTerm(Element).
137    * Type: negative, code 30760, exactly two arguments expected
138    * Data: {x | }
139    *
140    * @throws Exception Test failed.
141    */
 
142  1 toggle public void testClassTermNegative02() throws Exception {
143  1 final Element ele = TestParser.createElement(
144    "<CLASS>" +
145    " <VAR id=\"x\" />" +
146    "</CLASS>");
147    // System.out.println(ele.toString());
148  1 LogicalCheckExceptionList list =
149    FormulaChecker.checkTerm(ele, context, getChecker());
150  1 assertEquals(1, list.size());
151  1 assertEquals(30760, list.get(0).getErrorCode());
152    }
153   
154    /**
155    * Function: checkTerm(Element).
156    * Type: negative, code 30540, first argument must be a subject variable
157    * Data: {x | phi(y, x) | phi(y, x)}
158    *
159    * @throws Exception Test failed.
160    */
 
161  1 toggle public void testClassTermNegative03() throws Exception {
162  1 final Element ele = TestParser.createElement(
163    "<CLASS>" +
164    " <PREDVAR id=\"phi\">" +
165    " <VAR id=\"y\" />" +
166    " <VAR id=\"x\" />" +
167    " </PREDVAR>" +
168    " <PREDVAR id=\"phi\">" +
169    " <VAR id=\"y\" />" +
170    " <VAR id=\"x\" />" +
171    " </PREDVAR>" +
172    "</CLASS>");
173    // System.out.println(ele.toString());
174  1 LogicalCheckExceptionList list =
175    FormulaChecker.checkTerm(ele, context, getChecker());
176  1 assertEquals(1, list.size());
177  1 assertEquals(30540, list.get(0).getErrorCode());
178    }
179   
180    /**
181    * Function: checkTerm(Element).
182    * Type: negative, code 30550, subject variable already bound
183    * Data: {x | forall x phi(y, x)}
184    *
185    * @throws Exception Test failed.
186    */
 
187  1 toggle public void testClassTermNegative04() throws Exception {
188  1 final Element ele = TestParser.createElement(
189    "<CLASS>" +
190    " <VAR id=\"x\" />" +
191    " <FORALL>" +
192    " <VAR id=\"x\" />" +
193    " <PREDVAR id=\"phi\">" +
194    " <VAR id=\"y\" />" +
195    " <VAR id=\"x\" />" +
196    " </PREDVAR>" +
197    " </FORALL>" +
198    "</CLASS>");
199    // System.out.println(ele.toString());
200  1 LogicalCheckExceptionList list =
201    FormulaChecker.checkTerm(ele, context, getChecker());
202  1 assertEquals(1, list.size());
203  1 assertEquals(30550, list.get(0).getErrorCode());
204    }
205   
206   
207    /**
208    * Function: checkTerm(Element).
209    * Type: negative, code 30680, undefined class operator
210    * Data: {x | forall y phi(y, x)}
211    *
212    * @throws Exception Test failed.
213    */
 
214  1 toggle public void testClassTermNegative05() throws Exception {
215  1 final Element ele = TestParser.createElement(
216    "<CLASS>" +
217    " <VAR id=\"x\" />" +
218    " <FORALL>" +
219    " <VAR id=\"y\" />" +
220    " <PREDVAR id=\"phi\">" +
221    " <VAR id=\"y\" />" +
222    " <VAR id=\"x\" />" +
223    " </PREDVAR>" +
224    " </FORALL>" +
225    "</CLASS>");
226    // System.out.println(ele.toString());
227  1 LogicalCheckExceptionList list =
228    FormulaChecker.checkTerm(ele, context, getChecker()); // here class operator is defined
229  1 assertTrue(!list.hasErrors());
230  1 assertEquals(0, list.size());
231  1 list =
232    FormulaChecker.checkTerm(ele, context, getCheckerWithoutClass());
233  1 assertEquals(1, list.size());
234  1 assertEquals(30680, list.get(0).getErrorCode());
235    }
236   
237   
238    }