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: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
11: // Universitaet Koblenz-Landau, Germany
12: // Chalmers University of Technology, Sweden
13: //
14: // The KeY system is protected by the GNU General Public License.
15: // See LICENSE.TXT for details.
16: package de.uka.ilkd.key.proof.mgt;
17:
18: import java.util.Iterator;
19:
20: import de.uka.ilkd.key.gui.KeYMediator;
21: import de.uka.ilkd.key.proof.Goal;
22: import de.uka.ilkd.key.proof.Proof;
23: import de.uka.ilkd.key.rule.RuleApp;
24:
25: public interface ProofCorrectnessMgt {
26:
27: boolean ruleApplicable(RuleApp r, Goal g);
28:
29: String getLastAnalysisInfo();
30:
31: ProofStatus getStatus();
32:
33: void updateProofStatus();
34:
35: void ruleApplied(RuleApp r);
36:
37: void ruleUnApplied(RuleApp r);
38:
39: Iterator getAppliedNonAxioms();
40:
41: void setMediator(KeYMediator p_mediator);
42:
43: boolean proofSimilarTo(Proof p);
44:
45: RuleJustification getJustification(RuleApp app);
46:
47: }
|