1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
|
17 |
|
|
18 |
|
package org.qedeq.kernel.bo.service; |
19 |
|
|
20 |
|
import org.qedeq.base.trace.Trace; |
21 |
|
import org.qedeq.kernel.base.module.Axiom; |
22 |
|
import org.qedeq.kernel.base.module.Formula; |
23 |
|
import org.qedeq.kernel.base.module.FunctionDefinition; |
24 |
|
import org.qedeq.kernel.base.module.PredicateDefinition; |
25 |
|
import org.qedeq.kernel.base.module.Proposition; |
26 |
|
import org.qedeq.kernel.base.module.Rule; |
27 |
|
import org.qedeq.kernel.base.module.Term; |
28 |
|
import org.qedeq.kernel.bo.logic.FormulaChecker; |
29 |
|
import org.qedeq.kernel.bo.logic.wf.ExistenceChecker; |
30 |
|
import org.qedeq.kernel.bo.logic.wf.Function; |
31 |
|
import org.qedeq.kernel.bo.logic.wf.HigherLogicalErrors; |
32 |
|
import org.qedeq.kernel.bo.logic.wf.LogicalCheckExceptionList; |
33 |
|
import org.qedeq.kernel.bo.logic.wf.Predicate; |
34 |
|
import org.qedeq.kernel.bo.module.ControlVisitor; |
35 |
|
import org.qedeq.kernel.bo.module.KernelModuleReferenceList; |
36 |
|
import org.qedeq.kernel.bo.module.KernelQedeqBo; |
37 |
|
import org.qedeq.kernel.common.DefaultSourceFileExceptionList; |
38 |
|
import org.qedeq.kernel.common.IllegalModuleDataException; |
39 |
|
import org.qedeq.kernel.common.LogicalState; |
40 |
|
import org.qedeq.kernel.common.ModuleDataException; |
41 |
|
import org.qedeq.kernel.common.SourceFileExceptionList; |
42 |
|
|
43 |
|
|
44 |
|
|
45 |
|
|
46 |
|
|
47 |
|
@version |
48 |
|
@author |
49 |
|
|
|
|
| 79,9% |
Uncovered Elements: 30 (149) |
Complexity: 39 |
Complexity Density: 0,42 |
|
50 |
|
public final class QedeqBoFormalLogicChecker extends ControlVisitor { |
51 |
|
|
52 |
|
|
53 |
|
private static final Class CLASS = QedeqBoFormalLogicChecker.class; |
54 |
|
|
55 |
|
|
56 |
|
private ModuleConstantsExistenceChecker existence; |
57 |
|
|
58 |
|
|
59 |
|
|
60 |
|
|
61 |
|
@param |
62 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
63 |
62
|
private QedeqBoFormalLogicChecker(final KernelQedeqBo prop) {... |
64 |
62
|
super(prop); |
65 |
|
} |
66 |
|
|
67 |
|
|
68 |
|
|
69 |
|
|
70 |
|
@param |
71 |
|
@throws |
72 |
|
|
|
|
| 77,8% |
Uncovered Elements: 6 (27) |
Complexity: 6 |
Complexity Density: 0,29 |
|
73 |
113
|
public static void check(final DefaultKernelQedeqBo prop)... |
74 |
|
throws SourceFileExceptionList { |
75 |
113
|
if (prop.isChecked()) { |
76 |
51
|
return; |
77 |
|
} |
78 |
62
|
if (!prop.hasLoadedRequiredModules()) { |
79 |
0
|
throw new IllegalStateException("QEDEQ module has not loaded with required files: " |
80 |
|
+ prop); |
81 |
|
} |
82 |
62
|
prop.setLogicalProgressState(LogicalState.STATE_EXTERNAL_CHECKING); |
83 |
62
|
KernelModuleReferenceList list = (KernelModuleReferenceList) prop.getRequiredModules(); |
84 |
98
|
for (int i = 0; i < list.size(); i++) { |
85 |
36
|
try { |
86 |
36
|
Trace.trace(CLASS, "check(DefaultQedeqBo)", "checking label", |
87 |
|
list.getLabel(i)); |
88 |
36
|
check((DefaultKernelQedeqBo) list.getKernelQedeqBo(i)); |
89 |
|
} catch (SourceFileExceptionList e) { |
90 |
0
|
ModuleDataException md = new CheckRequiredModuleException(11231, |
91 |
|
"import check failed: " + list.getQedeqBo(i).getModuleAddress(), |
92 |
|
list.getModuleContext(i)); |
93 |
0
|
final SourceFileExceptionList sfl = prop.createSourceFileExceptionList(md); |
94 |
0
|
prop.setLogicalFailureState(LogicalState.STATE_EXTERNAL_CHECKING_FAILED, sfl); |
95 |
0
|
throw e; |
96 |
|
} |
97 |
|
} |
98 |
62
|
prop.setLogicalProgressState(LogicalState.STATE_INTERNAL_CHECKING); |
99 |
62
|
final QedeqBoFormalLogicChecker checker = new QedeqBoFormalLogicChecker(prop); |
100 |
62
|
try { |
101 |
62
|
checker.traverse(); |
102 |
|
} catch (SourceFileExceptionList sfl) { |
103 |
11
|
prop.setLogicalFailureState(LogicalState.STATE_INTERNAL_CHECKING_FAILED, sfl); |
104 |
11
|
throw sfl; |
105 |
|
} |
106 |
51
|
prop.setChecked(checker.existence); |
107 |
|
} |
108 |
|
|
|
|
| 60% |
Uncovered Elements: 2 (5) |
Complexity: 2 |
Complexity Density: 0,4 |
|
109 |
62
|
protected void traverse() throws DefaultSourceFileExceptionList {... |
110 |
62
|
try { |
111 |
62
|
this.existence = new ModuleConstantsExistenceChecker(getQedeqBo()); |
112 |
|
} catch (ModuleDataException me) { |
113 |
0
|
addModuleDataException(me); |
114 |
0
|
throw getSourceFileExceptionList(); |
115 |
|
} |
116 |
62
|
super.traverse(); |
117 |
|
} |
118 |
|
|
|
|
| 82,4% |
Uncovered Elements: 3 (17) |
Complexity: 4 |
Complexity Density: 0,36 |
|
119 |
175
|
public void visitEnter(final Axiom axiom) throws ModuleDataException {... |
120 |
175
|
if (axiom == null) { |
121 |
0
|
return; |
122 |
|
} |
123 |
175
|
final String context = getCurrentContext().getLocationWithinModule(); |
124 |
175
|
if (axiom.getFormula() != null) { |
125 |
175
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
126 |
175
|
final Formula formula = axiom.getFormula(); |
127 |
175
|
LogicalCheckExceptionList list = |
128 |
|
FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), existence); |
129 |
184
|
for (int i = 0; i < list.size(); i++) { |
130 |
9
|
addModuleDataException(list.get(i)); |
131 |
|
} |
132 |
|
} |
133 |
175
|
setLocationWithinModule(context); |
134 |
175
|
setBlocked(true); |
135 |
|
} |
136 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
137 |
175
|
public void visitLeave(final Axiom axiom) {... |
138 |
175
|
setBlocked(false); |
139 |
|
} |
140 |
|
|
|
|
| 77,8% |
Uncovered Elements: 6 (27) |
Complexity: 7 |
Complexity Density: 0,41 |
|
141 |
168
|
public void visitEnter(final PredicateDefinition definition)... |
142 |
|
throws ModuleDataException { |
143 |
168
|
if (definition == null) { |
144 |
0
|
return; |
145 |
|
} |
146 |
|
|
147 |
|
|
148 |
168
|
final String context = getCurrentContext().getLocationWithinModule(); |
149 |
168
|
final Predicate predicate = new Predicate(definition.getName(), |
150 |
|
definition.getArgumentNumber()); |
151 |
168
|
if (existence.predicateExists(predicate)) { |
152 |
0
|
throw new IllegalModuleDataException(HigherLogicalErrors.PREDICATE_ALREADY_DEFINED, |
153 |
|
HigherLogicalErrors.PREDICATE_ALREADY_DEFINED_TEXT + predicate, |
154 |
|
getCurrentContext()); |
155 |
|
} |
156 |
168
|
if ("2".equals(predicate.getArguments()) |
157 |
|
&& ExistenceChecker.NAME_EQUAL.equals(predicate.getName())) { |
158 |
17
|
existence.setIdentityOperatorDefined(true, predicate.getName()); |
159 |
|
} |
160 |
168
|
if (definition.getFormula() != null) { |
161 |
131
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
162 |
131
|
final Formula formula = definition.getFormula(); |
163 |
131
|
LogicalCheckExceptionList list = |
164 |
|
FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), existence); |
165 |
131
|
for (int i = 0; i < list.size(); i++) { |
166 |
0
|
addModuleDataException(list.get(i)); |
167 |
|
} |
168 |
|
} |
169 |
168
|
existence.add(definition); |
170 |
168
|
setLocationWithinModule(context); |
171 |
168
|
setBlocked(true); |
172 |
|
} |
173 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
174 |
168
|
public void visitLeave(final PredicateDefinition definition) {... |
175 |
168
|
setBlocked(false); |
176 |
|
} |
177 |
|
|
|
|
| 69,6% |
Uncovered Elements: 7 (23) |
Complexity: 5 |
Complexity Density: 0,33 |
|
178 |
96
|
public void visitEnter(final FunctionDefinition definition)... |
179 |
|
throws ModuleDataException { |
180 |
96
|
if (definition == null) { |
181 |
0
|
return; |
182 |
|
} |
183 |
|
|
184 |
96
|
final String context = getCurrentContext().getLocationWithinModule(); |
185 |
96
|
final Function function = new Function(definition.getName(), |
186 |
|
definition.getArgumentNumber()); |
187 |
96
|
if (existence.functionExists(function)) { |
188 |
0
|
throw new IllegalModuleDataException(HigherLogicalErrors.FUNCTION_ALREADY_DEFINED, |
189 |
|
HigherLogicalErrors.FUNCTION_ALREADY_DEFINED_TEXT + function, |
190 |
|
getCurrentContext()); |
191 |
|
} |
192 |
96
|
if (definition.getTerm() != null) { |
193 |
96
|
setLocationWithinModule(context + ".getTerm().getElement()"); |
194 |
96
|
final Term term = definition.getTerm(); |
195 |
96
|
LogicalCheckExceptionList list = |
196 |
|
FormulaChecker.checkTerm(term.getElement(), getCurrentContext(), existence); |
197 |
96
|
for (int i = 0; i < list.size(); i++) { |
198 |
0
|
addModuleDataException(list.get(i)); |
199 |
|
} |
200 |
|
} |
201 |
96
|
existence.add(definition); |
202 |
96
|
setLocationWithinModule(context); |
203 |
96
|
setBlocked(true); |
204 |
|
} |
205 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
206 |
96
|
public void visitLeave(final FunctionDefinition definition) {... |
207 |
96
|
setBlocked(false); |
208 |
|
} |
209 |
|
|
|
|
| 82,4% |
Uncovered Elements: 3 (17) |
Complexity: 4 |
Complexity Density: 0,36 |
|
210 |
390
|
public void visitEnter(final Proposition proposition)... |
211 |
|
throws ModuleDataException { |
212 |
390
|
if (proposition == null) { |
213 |
0
|
return; |
214 |
|
} |
215 |
390
|
final String context = getCurrentContext().getLocationWithinModule(); |
216 |
390
|
if (proposition.getFormula() != null) { |
217 |
390
|
setLocationWithinModule(context + ".getFormula().getElement()"); |
218 |
390
|
final Formula formula = proposition.getFormula(); |
219 |
390
|
LogicalCheckExceptionList list = |
220 |
|
FormulaChecker.checkFormula(formula.getElement(), getCurrentContext(), existence); |
221 |
394
|
for (int i = 0; i < list.size(); i++) { |
222 |
4
|
addModuleDataException(list.get(i)); |
223 |
|
} |
224 |
|
} |
225 |
390
|
setLocationWithinModule(context); |
226 |
390
|
setBlocked(true); |
227 |
|
} |
228 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
229 |
390
|
public void visitLeave(final Proposition definition) {... |
230 |
390
|
setBlocked(false); |
231 |
|
} |
232 |
|
|
|
|
| 75% |
Uncovered Elements: 3 (12) |
Complexity: 4 |
Complexity Density: 0,67 |
|
233 |
114
|
public void visitEnter(final Rule rule) throws ModuleDataException {... |
234 |
114
|
if (rule == null) { |
235 |
0
|
return; |
236 |
|
} |
237 |
114
|
if (rule.getName() != null) { |
238 |
114
|
if ("SET_DEFINION_BY_FORMULA".equals(rule.getName())) { |
239 |
|
|
240 |
6
|
existence.setClassOperatorExists(true); |
241 |
|
} |
242 |
|
} |
243 |
114
|
setBlocked(true); |
244 |
|
} |
245 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
246 |
114
|
public void visitLeave(final Rule rule) {... |
247 |
114
|
setBlocked(false); |
248 |
|
} |
249 |
|
|
250 |
|
|
251 |
|
|
252 |
|
|
253 |
|
@param |
254 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
255 |
1621
|
public void setLocationWithinModule(final String locationWithinModule) {... |
256 |
1621
|
getCurrentContext().setLocationWithinModule(locationWithinModule); |
257 |
|
} |
258 |
|
|
259 |
|
} |