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