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:
11: package de.uka.ilkd.key.proof;
12:
13: import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
14: import de.uka.ilkd.key.proof.mgt.ProofStatus;
15:
16: public abstract class ProofAggregate {
17:
18: private String name;
19: protected ProofStatus proofStatus = null;
20:
21: protected ProofAggregate(String name) {
22: this .name = name;
23: }
24:
25: public static ProofAggregate createProofAggregate(
26: ProofAggregate[] proofs, String name) {
27: if (proofs.length > 1) {
28: return new CompoundProof(proofs, name);
29: } else {
30: return proofs[0];
31: }
32: }
33:
34: public static ProofAggregate createProofAggregate(Proof[] proofs,
35: String name) {
36: if (proofs.length == 0)
37: return null; // needed for tests
38: if (proofs.length > 1) {
39: SingleProof singles[] = new SingleProof[proofs.length];
40: for (int i = 0; i < proofs.length; i++) {
41: singles[i] = new SingleProof(proofs[i], name);
42: }
43: return new CompoundProof(singles, name);
44: } else {
45: return new SingleProof(proofs[0], name);
46: }
47: }
48:
49: public static ProofAggregate createProofAggregate(Proof proof,
50: String name) {
51: return new SingleProof(proof, name);
52: }
53:
54: public abstract Proof[] getProofs();
55:
56: public Proof getFirstProof() {
57: return getProofs()[0];
58: }
59:
60: public void setProofEnv(ProofEnvironment env) {
61: Proof[] proofs = getProofs();
62: for (int i = 0; i < proofs.length; i++) {
63: proofs[i].setProofEnv(env);
64: }
65: }
66:
67: public abstract int size();
68:
69: public String description() {
70: return name;
71: }
72:
73: public String toString() {
74: return name;
75: }
76:
77: public abstract void updateProofStatus();
78:
79: public ProofStatus getStatus() {
80: if (proofStatus == null)
81: updateProofStatus();
82: return proofStatus;
83: }
84:
85: public abstract ProofAggregate[] getChildren();
86:
87: }
|