001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: package de.uka.ilkd.key.proof.mgt;
010:
011: import java.util.HashSet;
012: import java.util.Iterator;
013: import java.util.List;
014: import java.util.Set;
015:
016: import de.uka.ilkd.key.gui.KeYMediator;
017: import de.uka.ilkd.key.gui.RuleAppListener;
018: import de.uka.ilkd.key.proof.*;
019: import de.uka.ilkd.key.rule.RuleApp;
020:
021: public class DefaultProofCorrectnessMgt implements ProofCorrectnessMgt {
022:
023: private Proof proof;
024: private Set cachedAppliedRules = new HashSet();
025: private KeYMediator mediator;
026: private DefaultMgtProofListener proofListener = new DefaultMgtProofListener();
027: private DefaultMgtProofTreeListener proofTreeListener = new DefaultMgtProofTreeListener();
028:
029: private ProofStatus proofStatus = null;
030:
031: private DepAnalysis lastAnalysisInfo;
032:
033: public DefaultProofCorrectnessMgt(Proof p) {
034: this .proof = p;
035: proof.addProofTreeListener(proofTreeListener);
036: }
037:
038: public RuleJustification getJustification(RuleApp r) {
039: return proof.env().getJustifInfo().getJustification(r,
040: proof.getServices());
041: }
042:
043: public boolean ruleApplicable(RuleApp r, Goal g) {
044: final RuleJustification just = getJustification(r);
045: if (just == null) {
046: System.err.println("Warning: No justification for rule "
047: + r.rule().name() + " found");
048: return true;
049: }
050: lastAnalysisInfo = just.dependsOn(proof);
051: return !lastAnalysisInfo.depExists();
052: }
053:
054: public String getLastAnalysisInfo() {
055: return lastAnalysisInfo == null ? "" : lastAnalysisInfo
056: .toString();
057: }
058:
059: public void updateProofStatus() {
060: boolean closed = false;
061: boolean closedButLemmasLeft = false;
062: boolean open = false;
063:
064: if (proof.openGoals().size() == 0) {
065: // either closed or closedButLemmasLeft
066: Iterator cachedAppliedRulesIt = cachedAppliedRules
067: .iterator();
068:
069: RuleApp rule = null;
070: RuleJustification ruleJusti = null;
071: List list = null;
072: Iterator listIterator = null;
073: ProofAggregate pl = null;
074: int size = 0;
075: Proof p = null;
076:
077: boolean allRulesClosed = true;
078: while (cachedAppliedRulesIt.hasNext()) {
079: // every rule must be proven correct
080: rule = (RuleApp) cachedAppliedRulesIt.next();
081: ruleJusti = getJustification(rule);
082: list = ruleJusti.getProofList();
083: listIterator = list.iterator();
084: boolean oneClosed = false;
085: while (listIterator.hasNext()) {
086: // one of these must be closed
087: pl = (ProofAggregate) listIterator.next();
088: boolean allClosed = true;
089: Proof[] proofs = pl.getProofs();
090: size = proofs.length;
091: for (int i = 0; i < size; i++) {
092: // all of these must be closed
093: p = proofs[i];
094: p.mgt().updateProofStatus();
095: if (p.mgt().getStatus().getProofClosed()) {
096: // This proof is closed so it is possible
097: // that all proofs are closed.
098: } else {
099: // There is a proof which is not closed,
100: // so not all proofs can be closed!
101: allClosed = false;
102: }
103: }
104: if (allClosed) {
105: // all proofs in the ProofList are closed, meaning
106: // that this proof is closed
107: oneClosed = true;
108: } else {
109: // Nothing to do here because this proof wasn't closed.
110: }
111: }
112: if (oneClosed) {
113: // This rule is closed so it is still possible all rules are
114: // closed and thus no need to change allRulesClosed here.
115: } else {
116: allRulesClosed = false;
117: }
118: }
119: if (allRulesClosed) {
120: closed = true;
121: } else {
122: closedButLemmasLeft = true;
123: }
124: } else {
125: open = true;
126: }
127: proofStatus = new ProofStatus(closed, closedButLemmasLeft, open);
128: }
129:
130: private void cacheAppliedRule(RuleApp r) {
131: cachedAppliedRules.add(r);
132: }
133:
134: public void ruleApplied(RuleApp r) {
135: RuleJustification rj = getJustification(r);
136: if (rj == null) {
137: System.err.println("No justification found for rule "
138: + r.rule().name());
139: return;
140: }
141: if (!rj.isAxiomJustification()) {
142: cacheAppliedRule(r);
143: }
144: }
145:
146: public void ruleUnApplied(RuleApp r) {
147: boolean success = cachedAppliedRules.remove(r);
148: if (success) {
149: updateProofStatus();
150: }
151: }
152:
153: public Iterator getAppliedNonAxioms() {
154: return cachedAppliedRules.iterator();
155: }
156:
157: public void setMediator(KeYMediator p_mediator) {
158: if (mediator != null)
159: mediator.removeRuleAppListener(proofListener);
160:
161: mediator = p_mediator;
162:
163: if (mediator != null)
164: mediator.addRuleAppListener(proofListener);
165: }
166:
167: public Proof getProof() {
168: return proof;
169: }
170:
171: public boolean proofSimilarTo(Proof p) {
172: return p.name().equals(getProof().name()); //%%%
173: }
174:
175: public ProofStatus getStatus() {
176: if (proofStatus == null)
177: updateProofStatus();
178: return proofStatus;
179: }
180:
181: class DefaultMgtProofListener implements RuleAppListener {
182:
183: /** invoked when a rule has been applied */
184: public void ruleApplied(ProofEvent e) {
185: if (DefaultProofCorrectnessMgt.this .getProof() == e
186: .getSource()) {
187: //%% actually I only want to listen to events of one proof
188: DefaultProofCorrectnessMgt.this .ruleApplied(e
189: .getRuleAppInfo().getRuleApp());
190: }
191: }
192: }
193:
194: class DefaultMgtProofTreeListener extends ProofTreeAdapter {
195: public void proofClosed(ProofTreeEvent e) {
196: ProofEnvironment pEnv = proof.env();
197: pEnv.updateProofStatus();
198: }
199:
200: public void proofPruned(ProofTreeEvent e) {
201:
202: }
203:
204: public void proofGoalsAdded(ProofTreeEvent e) {
205:
206: }
207:
208: public void proofStructureChanged(ProofTreeEvent e) {
209:
210: }
211: }
212:
213: }
|