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: package de.uka.ilkd.key.proof;
09:
10: import java.util.LinkedList;
11: import java.util.List;
12:
13: import de.uka.ilkd.key.proof.mgt.ProofStatus;
14: import de.uka.ilkd.key.util.Debug;
15:
16: public class CompoundProof extends ProofAggregate {
17:
18: private ProofAggregate[] proofs;
19:
20: CompoundProof(ProofAggregate[] proofs, String name) {
21: super (name);
22: if (proofs.length <= 1)
23: Debug.fail();
24: this .proofs = proofs;
25: }
26:
27: private void addProofsToList(List l) {
28: for (int i = 0; i < size(); i++) {
29: if (proofs[i] instanceof SingleProof) {
30: l.add(proofs[i].getFirstProof());
31: } else {
32: ((CompoundProof) proofs[i]).addProofsToList(l);
33: }
34: }
35: }
36:
37: public Proof[] getProofs() {
38: List l = new LinkedList();
39: addProofsToList(l);
40: return (Proof[]) l.toArray(new Proof[0]);
41: }
42:
43: public int size() {
44: return proofs.length;
45: }
46:
47: public ProofAggregate get(int i) {
48: return proofs[i];
49: }
50:
51: public void updateProofStatus() {
52: proofs[0].updateProofStatus();
53: ProofStatus ps = proofs[0].getStatus();
54: for (int i = 1; i < proofs.length; i++) {
55: proofs[i].updateProofStatus();
56: ps = ps.combineProofStatus(proofs[i].getStatus());
57: }
58: proofStatus = ps;
59: }
60:
61: public ProofAggregate[] getChildren() {
62: return proofs;
63: }
64:
65: public boolean equals(Object o) {
66: if (!(o instanceof CompoundProof))
67: return false;
68: CompoundProof cmp = (CompoundProof) o;
69: for (int i = 0; i < cmp.size(); i++) {
70: if (!cmp.get(i).equals(get(i)))
71: return false;
72: }
73: return true;
74: }
75:
76: public int hashCode() {
77: int result = 17;
78: for (int i = 0; i < size(); i++) {
79: result = 37 * result + get(i).hashCode();
80: }
81: return result;
82: }
83: }
|