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.mgt;
09:
10: import java.util.HashMap;
11: import java.util.LinkedList;
12: import java.util.List;
13: import java.util.Map;
14:
15: import de.uka.ilkd.key.java.Services;
16: import de.uka.ilkd.key.proof.Proof;
17: import de.uka.ilkd.key.rule.*;
18: import de.uka.ilkd.key.util.Debug;
19:
20: public class ComplexRuleJustificationBySpec implements
21: ComplexRuleJustification {
22:
23: private Map contract2Just = new HashMap();
24:
25: public ComplexRuleJustificationBySpec() {
26: }
27:
28: public void add(Contract ct, RuleJustificationBySpec just) {
29: contract2Just.put(ct, just);
30: }
31:
32: public RuleJustification getSpecificJustification(RuleApp app,
33: Services services) {
34: if (app instanceof MethodContractRuleApp) {
35: return (RuleJustification) contract2Just
36: .get(((MethodContractRuleApp) app)
37: .getMethodContract());
38: } else if (app instanceof BuiltInRuleApp) {
39: return (RuleJustification) contract2Just
40: .get(UseMethodContractRule.INSTANCE
41: .selectExistingContract(
42: services,
43: app.posInOccurrence(),
44: AutomatedContractConfigurator.INSTANCE));
45: } else {
46: Debug.fail(); // should never be the case
47: return null;
48: }
49: }
50:
51: public DepAnalysis dependsOn(Proof p) {
52: // TODO Auto-generated method stub
53: return null;
54: }
55:
56: public boolean isAxiomJustification() {
57: return false;
58: }
59:
60: public List getProofList() {
61: return new LinkedList();
62: }
63:
64: }
|