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: //This file is part of KeY - Integrated Deductive Software Design
09: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: //The KeY system is protected by the GNU General Public License.
14: //See LICENSE.TXT for details.
15: //
16: //
17:
18: package de.uka.ilkd.key.proof.init;
19:
20: import java.util.Iterator;
21: import java.util.Map;
22:
23: import de.uka.ilkd.key.casetool.ModelClass;
24: import de.uka.ilkd.key.casetool.UMLModelClass;
25: import de.uka.ilkd.key.logic.Term;
26: import de.uka.ilkd.key.proof.mgt.Contract;
27: import de.uka.ilkd.key.proof.mgt.Contractable;
28: import de.uka.ilkd.key.speclang.OperationContract;
29: import de.uka.ilkd.key.util.Debug;
30:
31: /**
32: * The "BehaviouralSubtypingOp" proof obligation.
33: */
34: public class BehaviouralSubtypingOpPO extends AbstractPO {
35:
36: private ListOfProofOblInput pairPOs;
37:
38: //-------------------------------------------------------------------------
39: //constructors
40: //-------------------------------------------------------------------------
41:
42: public BehaviouralSubtypingOpPO(UMLModelClass subtype,
43: ModelClass super type, Map contractPairs) {
44: super ("BehaviouralSubtypingOp of " + subtype.getClassName()
45: + " and " + super type.getClassName(), subtype);
46: pairPOs = SLListOfProofOblInput.EMPTY_LIST;
47:
48: Iterator it = contractPairs.entrySet().iterator();
49: while (it.hasNext()) {
50: Map.Entry e = (Map.Entry) (it.next());
51: OperationContract subContract = (OperationContract) (e
52: .getKey());
53: OperationContract super Contract = (OperationContract) (e
54: .getValue());
55: ProofOblInput pairPO = new BehaviouralSubtypingOpPairPO(
56: subContract, super Contract);
57: pairPOs = pairPOs.append(pairPO);
58: }
59: Debug.assertFalse(pairPOs.isEmpty());
60: }
61:
62: //-------------------------------------------------------------------------
63: //methods of ProofOblInput interface
64: //-------------------------------------------------------------------------
65:
66: public void readProblem(ModStrategy mod) throws ProofInputException {
67: int numPOs = pairPOs.size() * 2;
68: poTerms = new Term[numPOs];
69: poNames = new String[numPOs];
70:
71: IteratorOfProofOblInput it = pairPOs.iterator();
72: int i = 0;
73: while (it.hasNext()) {
74: BehaviouralSubtypingOpPairPO pairPO = (BehaviouralSubtypingOpPairPO) (it
75: .next());
76: pairPO.readProblem(mod);
77: poTerms[i] = pairPO.getTerm1();
78: poNames[i++] = pairPO.name() + " - Pre";
79: poTerms[i] = pairPO.getTerm2();
80: poNames[i++] = pairPO.name() + " - Post";
81: }
82: }
83:
84: public void setInitConfig(InitConfig conf) {
85: super .setInitConfig(conf);
86: IteratorOfProofOblInput it = pairPOs.iterator();
87: while (it.hasNext()) {
88: it.next().setInitConfig(conf);
89: }
90: }
91:
92: public Contractable[] getObjectOfContract() {
93: return new Contractable[0];
94: }
95:
96: public boolean initContract(Contract ct) {
97: return false;
98: }
99: }
|