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.mgt;
12:
13: import java.util.Iterator;
14: import java.util.LinkedList;
15: import java.util.List;
16:
17: import de.uka.ilkd.key.logic.op.Modality;
18: import de.uka.ilkd.key.proof.ProofAggregate;
19:
20: /** represents a set of contracts (@link{Contract}}) with attached proofs.*/
21: public class ContractSet {
22:
23: private List contracts = new LinkedList();
24:
25: public Contract add(Contract ct) {
26: Iterator it = contracts.iterator();
27: while (it.hasNext()) {
28: Contract c = (Contract) it.next();
29: if (c.equals(ct)) {
30: return c;
31: }
32: }
33: contracts.add(ct);
34: return ct;
35: }
36:
37: public void addAll(ContractSet cs) {
38: if (cs == null)
39: return;
40: Iterator it = cs.iterator();
41: while (it.hasNext()) {
42: add((Contract) it.next());
43: }
44: }
45:
46: public Iterator iterator() {
47: return contracts.iterator();
48: }
49:
50: public void removeProofList(ProofAggregate pl) {
51: for (final Iterator it = iterator(); it.hasNext();) {
52: ((Contract) it.next()).removeCompoundProof(pl);
53: }
54: }
55:
56: public int size() {
57: return contracts.size();
58: }
59:
60: public Contract[] toArray() {
61: return (Contract[]) contracts.toArray(new Contract[contracts
62: .size()]);
63: }
64:
65: /** returns a set of contracts with the argument as identifying
66: * contracted object and the matching modality
67: */
68: public ContractSet getMethodContracts(Modality modality) {
69: ContractSet result = new ContractSet();
70: Iterator it = iterator();
71: while (it.hasNext()) {
72: Contract ct = (Contract) it.next();
73: if (ct instanceof OldOperationContract
74: && ((OldOperationContract) ct)
75: .applicableForModality(modality)) {
76: result.add(ct);
77: }
78: }
79: return result;
80: }
81:
82: }
|