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.rule;
09:
10: import java.util.Iterator;
11:
12: import de.uka.ilkd.key.logic.op.ListOfProgramMethod;
13: import de.uka.ilkd.key.logic.op.Modality;
14: import de.uka.ilkd.key.proof.mgt.ContractSet;
15: import de.uka.ilkd.key.proof.mgt.DLMethodContract;
16: import de.uka.ilkd.key.proof.mgt.OldOperationContract;
17: import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
18: import de.uka.ilkd.key.speclang.ListOfClassInvariant;
19: import de.uka.ilkd.key.speclang.SLListOfClassInvariant;
20:
21: public class AutomatedContractConfigurator implements
22: ContractConfigurator {
23:
24: public final static AutomatedContractConfigurator INSTANCE = new AutomatedContractConfigurator();
25:
26: private SpecificationRepository repos;
27: private ListOfProgramMethod programMethods;
28: private OldOperationContract result;
29: private Modality modality;
30:
31: private AutomatedContractConfigurator() {
32: }
33:
34: public void setSpecification(SpecificationRepository repos) {
35: this .repos = repos;
36: }
37:
38: public void start() {
39: ContractSet ctSet = repos
40: .getContracts(programMethods, modality);
41: Iterator it = ctSet.iterator();
42: while (it.hasNext()) {
43: OldOperationContract ct = (OldOperationContract) it.next();
44: if (ct instanceof DLMethodContract) {
45: result = ct;
46: return;
47: }
48: }
49: if (ctSet.size() > 0) {
50: result = (OldOperationContract) ctSet.iterator().next();
51: return;
52: }
53: result = null;
54: }
55:
56: public OldOperationContract getMethodContract() {
57: return result;
58: }
59:
60: public ListOfClassInvariant getPreInvariants() {
61: return SLListOfClassInvariant.EMPTY_LIST;
62: }
63:
64: public ListOfClassInvariant getPostInvariants() {
65: return SLListOfClassInvariant.EMPTY_LIST;
66: }
67:
68: public void setProgramMethods(ListOfProgramMethod pm) {
69: this .programMethods = pm;
70: }
71:
72: public void setModality(Modality modality) {
73: this .modality = modality;
74: }
75:
76: public boolean wasSuccessful() {
77: return (result != null);
78: }
79:
80: public void clear() {
81: result = null;
82: }
83:
84: public void allowConfiguration(boolean allowConfig) {
85: // no effect currently, we do not configure anyway
86: }
87:
88: }
|