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 de.uka.ilkd.key.proof.Proof;
14: import de.uka.ilkd.key.proof.init.ProofOblInput;
15: import de.uka.ilkd.key.rule.NoPosTacletApp;
16: import de.uka.ilkd.key.rule.Taclet;
17:
18: public class LemmaSpec extends AbstractContract {
19:
20: private NoPosTacletApp lemma;
21:
22: public LemmaSpec(NoPosTacletApp lemma) {
23: this .lemma = lemma;
24: }
25:
26: public Taclet getLemmaAndRegister() {
27: return lemma.taclet();
28: }
29:
30: public Object getObjectOfContract() {
31: return lemma;
32: }
33:
34: public ProofOblInput getProofOblInput(Proof proof) {
35: return null; // not implemented yet
36: }
37:
38: public String toString() {
39: return "Lemma specification: " + lemma;
40: }
41:
42: public boolean equals(Object cmp) {
43: if (!(cmp instanceof LemmaSpec))
44: return false;
45: return lemma.equals(((LemmaSpec) cmp).lemma);
46: }
47:
48: public int hashCode() {
49: return lemma.hashCode();
50: }
51:
52: public String getName() {
53: return toString();
54: }
55:
56: }
|