Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
Overview   Package   File
    FRAMES   NO FRAMES     
105   339   20   9.55
18   286   0.19   11
11     1.82  
1    
 
  ProofCheckerTest       Line # 43 105 20 95.5% 0.95522386
 
  (3)
 
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    package org.qedeq.kernel.bo.logic.proof.checker;
16   
17    import java.io.File;
18   
19    import org.qedeq.kernel.bo.KernelContext;
20    import org.qedeq.kernel.bo.logic.common.LogicalCheckExceptionList;
21    import org.qedeq.kernel.bo.logic.common.ReferenceResolver;
22    import org.qedeq.kernel.bo.logic.proof.common.ProofChecker;
23    import org.qedeq.kernel.bo.logic.proof.common.RuleChecker;
24    import org.qedeq.kernel.bo.module.KernelNodeBo;
25    import org.qedeq.kernel.bo.module.KernelQedeqBo;
26    import org.qedeq.kernel.bo.test.QedeqBoTestCase;
27    import org.qedeq.kernel.se.base.list.Element;
28    import org.qedeq.kernel.se.base.module.FormalProofLineList;
29    import org.qedeq.kernel.se.base.module.Proposition;
30    import org.qedeq.kernel.se.common.DefaultModuleAddress;
31    import org.qedeq.kernel.se.common.ModuleAddress;
32    import org.qedeq.kernel.se.common.ModuleContext;
33    import org.qedeq.kernel.se.common.RuleKey;
34    import org.qedeq.kernel.se.dto.list.DefaultAtom;
35    import org.qedeq.kernel.se.dto.list.DefaultElementList;
36    import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
37   
38    /**
39    * For testing of checking formal proofs.
40    *
41    * @author Michael Meyling
42    */
 
43    public class ProofCheckerTest extends QedeqBoTestCase {
44   
45    private ProofChecker checker0;
46   
47    private ProofChecker checker1;
48   
49    private ProofChecker checker2;
50   
51    private RuleChecker ruleCheckerAll;
52   
53    private ReferenceResolver resolverLocal;
54   
55    private Element disjunction_idempotence_axiom =
56    new DefaultElementList("IMPL", new Element[] {
57    new DefaultElementList("OR", new Element[] {
58    new DefaultElementList("PREDVAR", new Element[] {
59    new DefaultAtom("A")
60    }),
61    new DefaultElementList("PREDVAR", new Element[] {
62    new DefaultAtom("A")
63    })
64    }),
65    new DefaultElementList("PREDVAR", new Element[] {
66    new DefaultAtom("A")
67    })
68    });
69   
70    private Element disjunction_weakening_axiom =
71    new DefaultElementList("IMPL", new Element[] {
72    new DefaultElementList("PREDVAR", new Element[] {
73    new DefaultAtom("A")
74    }),
75    new DefaultElementList("OR", new Element[] {
76    new DefaultElementList("PREDVAR", new Element[] {
77    new DefaultAtom("A")
78    }),
79    new DefaultElementList("PREDVAR", new Element[] {
80    new DefaultAtom("B")
81    })
82    })
83    });
84   
85    private Element disjunction_addition_axiom =
86    new DefaultElementList("IMPL", new Element[] {
87    new DefaultElementList("IMPL", new Element[] {
88    new DefaultElementList("PREDVAR", new Element[] {
89    new DefaultAtom("A")
90    }),
91    new DefaultElementList("PREDVAR", new Element[] {
92    new DefaultAtom("B")
93    })
94    }),
95    new DefaultElementList("IMPL", new Element[] {
96    new DefaultElementList("IMPL", new Element[] {
97    new DefaultElementList("PREDVAR", new Element[] {
98    new DefaultAtom("C")
99    }),
100    new DefaultElementList("PREDVAR", new Element[] {
101    new DefaultAtom("A")
102    })
103    }),
104    new DefaultElementList("IMPL", new Element[] {
105    new DefaultElementList("PREDVAR", new Element[] {
106    new DefaultAtom("C")
107    }),
108    new DefaultElementList("PREDVAR", new Element[] {
109    new DefaultAtom("B")
110    })
111    })
112    })
113    });
114   
115    private Element universal_instantiation_axiom =
116    new DefaultElementList("IMPL", new Element[] {
117    new DefaultElementList("FORALL", new Element[] {
118    new DefaultElementList("VAR", new Element[] {
119    new DefaultAtom("x")
120    }),
121    new DefaultElementList("PREDVAR", new Element[] {
122    new DefaultAtom("\\phi"),
123    new DefaultElementList("VAR", new Element[] {
124    new DefaultAtom("x")
125    })
126    })
127    }),
128    new DefaultElementList("PREDVAR", new Element[] {
129    new DefaultAtom("\\phi"),
130    new DefaultElementList("VAR", new Element[] {
131    new DefaultAtom("y")
132    })
133    })
134    });
135   
136    private Element existencial_generalization_axiom =
137    new DefaultElementList("IMPL", new Element[] {
138    new DefaultElementList("PREDVAR", new Element[] {
139    new DefaultAtom("\\phi"),
140    new DefaultElementList("VAR", new Element[] {
141    new DefaultAtom("y")
142    })
143    }),
144    new DefaultElementList("EXISTS", new Element[] {
145    new DefaultElementList("VAR", new Element[] {
146    new DefaultAtom("x")
147    }),
148    new DefaultElementList("PREDVAR", new Element[] {
149    new DefaultAtom("\\phi"),
150    new DefaultElementList("VAR", new Element[] {
151    new DefaultAtom("x")
152    })
153    })
154    })
155    });
156   
 
157  3 toggle public void setUp() throws Exception {
158  3 super.setUp();
159  3 checker0 = new ProofChecker0Impl();
160  3 checker1 = new ProofChecker1Impl();
161  3 checker2 = new ProofChecker2Impl();
162  3 ruleCheckerAll = new RuleChecker() {
 
163  96 toggle public RuleKey getRule(String ruleName) {
164  96 return new RuleKey(ruleName, "0.01.00");
165    }
166    };
167  3 resolverLocal = new ReferenceResolver() {
 
168  264 toggle public Element getNormalizedFormula(Element element) {
169  264 return element;
170    }
171   
 
172  0 toggle public Element getNormalizedLocalProofLineReference(String reference) {
173  0 return null;
174    }
175   
 
176  20 toggle public Element getNormalizedReferenceFormula(String reference) {
177  20 if ("axiom:disjunction_idempotence".equals(reference)) {
178  2 return disjunction_idempotence_axiom;
179  18 } else if ("axiom:disjunction_weakening".equals(reference)) {
180  2 return disjunction_weakening_axiom;
181  16 } else if ("axiom:disjunction_addition".equals(reference)) {
182  8 return disjunction_addition_axiom;
183  8 } else if ("axiom:universalInstantiation".equals(reference)) {
184  6 return universal_instantiation_axiom;
185  2 } else if ("axiom:existencialGeneralization".equals(reference)) {
186  2 return existencial_generalization_axiom;
187    }
188  0 return null;
189    }
190   
 
191  0 toggle public ModuleContext getReferenceContext(String reference) {
192  0 return null;
193    }
194   
 
195  48 toggle public boolean isLocalProofLineReference(String reference) {
196  48 return false;
197    }
198   
 
199  20 toggle public boolean isProvedFormula(String reference) {
200  20 return true;
201    }
202    };
203    }
204   
205   
 
206  1 toggle public void testCheck1() throws Exception {
207  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
208    "sample/qedeq_sample3.xml"));
209  1 KernelContext.getInstance().checkWellFormedness(address);
210  1 final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address);
211  1 assertTrue(bo.isWellFormed());
212  1 assertNotNull(bo.getWarnings());
213  1 assertEquals(0, bo.getWarnings().size());
214  1 assertEquals(0, bo.getErrors().size());
215  1 final KernelNodeBo node = bo.getLabels().getNode("proposition:one");
216  1 final Proposition prop = node.getNodeVo().getNodeType().getProposition();
217  1 final FormalProofLineList original = prop.getFormalProofList().get(0)
218    .getFormalProofLineList();
219  1 final FormalProofLineListVo list = new FormalProofLineListVo();
220  10 for (int i = 0; i < 9; i++) {
221  9 list.add(original.get(i));
222    }
223  1 LogicalCheckExceptionList e0 =
224    checker0.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
225    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
226  1 assertNotNull(e0);
227  1 assertEquals(1, e0.size());
228  1 assertEquals(37400, e0.get(0).getErrorCode());
229  1 LogicalCheckExceptionList e1 =
230    checker1.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
231    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
232  1 assertNotNull(e1);
233  1 assertEquals(0, e1.size());
234  1 LogicalCheckExceptionList e2 =
235    checker2.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
236    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
237  1 assertNotNull(e2);
238  1 assertEquals(0, e2.size());
239    }
240   
 
241  1 toggle public void testCheck4() throws Exception {
242  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
243    "sample/qedeq_sample3.xml"));
244  1 KernelContext.getInstance().checkWellFormedness(address);
245  1 final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address);
246  1 assertTrue(bo.isWellFormed());
247  1 assertNotNull(bo.getWarnings());
248  1 assertEquals(0, bo.getWarnings().size());
249  1 assertEquals(0, bo.getErrors().size());
250  1 final KernelNodeBo node = bo.getLabels().getNode("proposition:four");
251  1 final Proposition prop = node.getNodeVo().getNodeType().getProposition();
252  1 final FormalProofLineList original = prop.getFormalProofList().get(0)
253    .getFormalProofLineList();
254  1 final FormalProofLineListVo list = new FormalProofLineListVo();
255  9 for (int i = 0; i < 8; i++) {
256  8 list.add(original.get(i));
257    }
258  1 LogicalCheckExceptionList e0 =
259    checker0.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
260    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
261  1 assertNotNull(e0);
262  1 assertEquals(1, e0.size());
263  1 assertEquals(37400, e0.get(0).getErrorCode());
264  1 LogicalCheckExceptionList e1 =
265    checker1.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
266    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
267  1 assertNotNull(e1);
268  1 assertEquals(0, e1.size());
269  1 LogicalCheckExceptionList e2 =
270    checker2.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
271    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
272  1 assertNotNull(e2);
273  1 assertEquals(0, e2.size());
274    }
275   
 
276  1 toggle public void testCheck6() throws Exception {
277  1 final ModuleAddress address = new DefaultModuleAddress(new File(getDocDir(),
278    "sample/qedeq_sample3.xml"));
279  1 KernelContext.getInstance().checkWellFormedness(address);
280  1 final KernelQedeqBo bo = (KernelQedeqBo) KernelContext.getInstance().getQedeqBo(address);
281  1 assertTrue(bo.isWellFormed());
282  1 assertNotNull(bo.getWarnings());
283  1 assertEquals(0, bo.getWarnings().size());
284  1 assertEquals(0, bo.getErrors().size());
285  1 final KernelNodeBo node = bo.getLabels().getNode("proposition:six");
286  1 final Proposition prop = node.getNodeVo().getNodeType().getProposition();
287  1 final FormalProofLineList original = prop.getFormalProofList().get(0)
288    .getFormalProofLineList();
289  1 FormalProofLineListVo list = new FormalProofLineListVo();
290  16 for (int i = 0; i < 15; i++) {
291  15 list.add(original.get(i));
292    }
293  1 LogicalCheckExceptionList e0 =
294    checker0.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
295    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
296  1 assertNotNull(e0);
297  1 assertEquals(1, e0.size());
298  1 assertEquals(37400, e0.get(0).getErrorCode());
299  1 LogicalCheckExceptionList e2 =
300    checker1.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
301    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
302  1 assertNotNull(e2);
303  1 assertEquals(1, e2.size());
304  1 assertEquals(37200, e2.get(0).getErrorCode());
305  1 list.add(original.get(15));
306  1 LogicalCheckExceptionList e3 =
307    checker1.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
308    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
309  1 assertNotNull(e3);
310  1 assertEquals(0, e3.size());
311   
312  1 list = new FormalProofLineListVo();
313  16 for (int i = 0; i < 15; i++) {
314  15 list.add(original.get(i));
315    }
316  1 LogicalCheckExceptionList e4 =
317    checker2.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
318    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
319  1 assertNotNull(e4);
320    // System.out.println(e2);
321    // Element2LatexImpl transform = new Element2LatexImpl(new ModuleLabels());
322    // System.out.println(transform.getLatex(universal_instantiation_axiom));
323    // System.out.println(e2);
324  1 assertEquals(1, e4.size());
325    // System.out.println(e2.get(0));
326  1 assertEquals(37200, e4.get(0).getErrorCode());
327  1 list.add(original.get(15));
328  1 LogicalCheckExceptionList e5 =
329    checker2.checkProof(prop.getFormula().getElement(), list, ruleCheckerAll,
330    DefaultModuleAddress.MEMORY.createModuleContext(), resolverLocal);
331  1 assertNotNull(e5);
332    // System.out.println(e2);
333    // Element2LatexImpl transform = new Element2LatexImpl(new ModuleLabels());
334    // System.out.println(transform.getLatex(universal_instantiation_axiom));
335    // System.out.println(e3);
336  1 assertEquals(0, e5.size());
337    }
338   
339    }
 
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 .