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.LinkedList;
14: import java.util.List;
15:
16: import de.uka.ilkd.key.proof.ProofAggregate;
17:
18: /**
19: * @deprecated
20: */
21: public abstract class AbstractContract implements Contract {
22:
23: protected List proofs = new LinkedList();
24: protected ProofEnvironment env;
25: protected String header;
26:
27: public void setProofEnv(ProofEnvironment env) {
28: if (this .env == null) {
29: this .env = env;
30: } else if (this .env != env) {
31: throw new IllegalStateException("Contract may belong to "
32: + "only one environment.");
33: }
34: }
35:
36: public ProofEnvironment getProofEnv() {
37: return env;
38: }
39:
40: public List getProofs() {
41: return proofs;
42: }
43:
44: public void addCompoundProof(ProofAggregate pl) {
45: proofs.add(pl);
46: }
47:
48: public void removeCompoundProof(ProofAggregate pl) {
49: proofs.remove(pl);
50: }
51:
52: /** Sets the textual header needed to later load the proof of this contract.
53: * This header is usually copied from the problem, in which the contract
54: * is defined/used.
55: */
56: public void setHeader(String s) {
57: if (header == null)
58: header = s;
59: }
60:
61: }
|