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 de.uka.ilkd.key.casetool.ModelClass;
21: import de.uka.ilkd.key.casetool.UMLModelClass;
22: import de.uka.ilkd.key.logic.Term;
23: import de.uka.ilkd.key.logic.op.LogicVariable;
24: import de.uka.ilkd.key.proof.mgt.Contract;
25: import de.uka.ilkd.key.proof.mgt.Contractable;
26: import de.uka.ilkd.key.speclang.SLTranslationError;
27:
28: /**
29: * The "BehaviouralSubtypingInv" proof obligation
30: * (formerly known as StructuralSubtyping).
31: */
32: public class BehaviouralSubtypingInvPO extends AbstractPO {
33:
34: private UMLModelClass subType;
35: private ModelClass super Type;
36:
37: //-------------------------------------------------------------------------
38: //constructors
39: //-------------------------------------------------------------------------
40:
41: public BehaviouralSubtypingInvPO(UMLModelClass subType,
42: ModelClass super Type) {
43: super ("BehaviouralSubtypingInv of " + subType.getClassName()
44: + " and " + super Type.getClassName(), subType);
45: this .subType = subType;
46: this .super Type = super Type;
47: }
48:
49: //-------------------------------------------------------------------------
50: //methods of ProofOblInput interface
51: //-------------------------------------------------------------------------
52:
53: public void readProblem(ModStrategy mod) throws ProofInputException {
54: //make sure initConfig has been set
55: if (initConfig == null) {
56: throw new IllegalStateException("InitConfig not set.");
57: }
58:
59: try {
60: //prepare self variable
61: LogicVariable selfVar = buildSelfVarAsLogicVar();
62:
63: //build conjunction of subtype invariants
64: Term subConjTerm = translateInvsOpen(subType
65: .getMyClassInvariants(), selfVar);
66:
67: //build conjunction of supertype invariants
68: Term super ConjTerm = translateInvsOpen(super Type
69: .getMyClassInvariants(), selfVar);
70:
71: //build implication
72: Term impTerm = tb.imp(subConjTerm, super ConjTerm);
73:
74: //build all-quantification
75: Term poTerm = tb.all(selfVar, impTerm);
76: poTerms = new Term[] { poTerm };
77: } catch (SLTranslationError e) {
78: throw new ProofInputException(e);
79: }
80: }
81:
82: public Contractable[] getObjectOfContract() {
83: return new Contractable[0];
84: }
85:
86: public boolean initContract(Contract ct) {
87: return false;
88: }
89: }
|