01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //
09:
10: package de.uka.ilkd.key.proof.mgt;
11:
12: import java.util.Iterator;
13: import java.util.List;
14:
15: import de.uka.ilkd.key.proof.Proof;
16: import de.uka.ilkd.key.proof.ProofAggregate;
17: import de.uka.ilkd.key.rule.RuleApp;
18:
19: public abstract class LemmaRuleJustification implements
20: RuleJustification {
21:
22: private RuleJustification getJustification(RuleApp r,
23: ProofEnvironment env) {
24: return env.getJustifInfo().getJustification(r,
25: env.getInitialServices());
26: }
27:
28: public DepAnalysis dependsOn(Proof p) {
29: List list = getProofList();
30: Iterator it = list.iterator();
31: if (!it.hasNext()) {
32: return DepAnalysis.getInstance(false, "No Proof available "
33: + "for method contract");
34: }
35: while (it.hasNext()) {
36: ProofAggregate pl = (ProofAggregate) it.next();
37: if (pl == null) {
38: return new DepAnalysis(false, "No proof in proof list "
39: + "for method contract");
40: }
41: Proof[] proofs = pl.getProofs();
42: for (int i = 0; i < proofs.length; i++) {
43: Proof curr = proofs[i];
44: if (curr == p) {
45: return DepAnalysis.getInstance(true, null, curr,
46: "Direct dependency from "
47: + "rule to proof.");
48: }
49: }
50: }
51: it = list.iterator();
52: while (it.hasNext()) {
53: ProofAggregate pl = (ProofAggregate) it.next();
54: Proof[] proofs = pl.getProofs();
55: for (int i = 0; i < proofs.length; i++) {
56: Proof curr = proofs[i];
57: Iterator nonAxIt = curr.mgt().getAppliedNonAxioms();
58: while (nonAxIt.hasNext()) {
59: RuleApp nonAx = (RuleApp) nonAxIt.next();
60: DepAnalysis ana = getJustification(nonAx, p.env())
61: .dependsOn(p);
62: if (ana.depExists()) {
63: return DepAnalysis.getInstance(true, null,
64: curr, "Indirect dependency from "
65: + "rule to proof.");
66: }
67: }
68: }
69: }
70: return DepAnalysis.getInstance(false, null, null);
71: }
72:
73: public boolean isAxiomJustification() {
74: return false;
75: }
76:
77: }
|