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: //This file is part of KeY - Integrated Deductive Software Design
09: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: // The KeY system is protected by the GNU General Public License.
14: // See LICENSE.TXT for details.
15: //
16: package de.uka.ilkd.key.proof.mgt;
17:
18: import de.uka.ilkd.key.util.Debug;
19:
20: public class ProofStatus {
21:
22: public final static ProofStatus OPEN = new ProofStatus(false,
23: false, true);
24: public final static ProofStatus CLOSED_BUT_LEMMAS_LEFT = new ProofStatus(
25: false, true, false);
26: public final static ProofStatus CLOSED = new ProofStatus(true,
27: false, false);
28:
29: private boolean closed;
30: private boolean closedButLemmasLeft;
31: private boolean open;
32:
33: public ProofStatus(boolean closed, boolean closedButLemmasLeft,
34: boolean open) {
35: this .closed = closed;
36: this .closedButLemmasLeft = closedButLemmasLeft;
37: this .open = open;
38: }
39:
40: public boolean getProofClosed() {
41: return closed;
42: }
43:
44: public boolean getProofClosedButLemmasLeft() {
45: return closedButLemmasLeft;
46: }
47:
48: public boolean getProofOpen() {
49: return open;
50: }
51:
52: public ProofStatus combineProofStatus(ProofStatus ps) {
53: if (getProofOpen() || ps.getProofOpen())
54: return OPEN;
55: if (getProofClosedButLemmasLeft()
56: || ps.getProofClosedButLemmasLeft())
57: return CLOSED_BUT_LEMMAS_LEFT;
58: if (getProofClosed() || ps.getProofClosed())
59: return CLOSED;
60: Debug.fail();
61: return null;
62: }
63:
64: public String toString() {
65: if (closed && !closedButLemmasLeft && !open) {
66: return "This proof is really closed.";
67: }
68: if (!closed && closedButLemmasLeft && !open) {
69: return "This proof is closed but there are Lemmas left to be proven.";
70: }
71: if (!closed && !closedButLemmasLeft && open) {
72: return "This proof is still open!";
73: }
74:
75: return "Illegal status!";
76:
77: }
78:
79: }
|