001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof.init;
019:
020: import java.util.HashMap;
021: import java.util.Map;
022:
023: import de.uka.ilkd.key.casetool.ModelMethod;
024: import de.uka.ilkd.key.logic.Term;
025: import de.uka.ilkd.key.logic.op.ListOfProgramVariable;
026: import de.uka.ilkd.key.logic.op.ProgramVariable;
027: import de.uka.ilkd.key.proof.mgt.Contract;
028: import de.uka.ilkd.key.proof.mgt.Contractable;
029: import de.uka.ilkd.key.speclang.OperationContract;
030: import de.uka.ilkd.key.speclang.SLTranslationError;
031:
032: /**
033: * The "BehaviouralSubtypingOpPair" proof obligation.
034: */
035: public class BehaviouralSubtypingOpPairPO extends AbstractPO {
036:
037: private OperationContract subContract;
038: private OperationContract super Contract;
039:
040: //-------------------------------------------------------------------------
041: //constructors
042: //-------------------------------------------------------------------------
043:
044: public BehaviouralSubtypingOpPairPO(OperationContract subContract,
045: OperationContract super Contract) {
046: super ("BehaviouralSubtypingOpPair for "
047: + subContract.getModelMethod(), subContract
048: .getModelMethod().getContainingClass());
049: this .subContract = subContract;
050: this .super Contract = super Contract;
051: }
052:
053: //-------------------------------------------------------------------------
054: //methods of ProofOblInput interface
055: //-------------------------------------------------------------------------
056:
057: public void readProblem(ModStrategy mod) throws ProofInputException {
058: //make sure initConfig has been set
059: if (initConfig == null) {
060: throw new IllegalStateException("InitConfig not set.");
061: }
062:
063: poTerms = new Term[2];
064: poNames = new String[2];
065:
066: //prepare variables and container for @pre-functions
067: ModelMethod modelMethod = subContract.getModelMethod();
068: ProgramVariable selfVar = buildSelfVarAsProgVar();
069: ListOfProgramVariable paramVars = buildParamVars(modelMethod);
070: ProgramVariable resultVar = buildResultVar(modelMethod);
071: ProgramVariable exceptionVar = buildExcVar();
072: Map atPreFunctions = new HashMap();
073:
074: try {
075: //build precondition implication
076: Term super PreTerm = translatePre(super Contract, selfVar,
077: toPV(paramVars));
078: Term subPreTerm = translatePre(subContract, selfVar,
079: toPV(paramVars));
080: poTerms[0] = tb.imp(super PreTerm, subPreTerm);
081: poNames[0] = "Preconditions";
082:
083: //build inner postcondition implication
084: Term subPostTerm = translatePost(subContract, selfVar,
085: toPV(paramVars), resultVar, exceptionVar);
086: Term super PostTerm = translatePost(super Contract, selfVar,
087: toPV(paramVars), resultVar, exceptionVar);
088: Term postImpTerm = tb.imp(subPostTerm, super PostTerm);
089:
090: //build updates
091: Term postUpdateTerm = translateModifies(subContract,
092: postImpTerm, selfVar, toPV(paramVars));
093:
094: //build definitions for @pre-functions
095: Term atPreDefinitionsTerm = buildAtPreDefinitions(atPreFunctions);
096:
097: //put together @pre-definitions and sub precondition
098: Term defAndSubPreTerm = tb.and(atPreDefinitionsTerm,
099: subPreTerm);
100:
101: //build postcondition implication
102: poTerms[1] = tb.imp(defAndSubPreTerm, postUpdateTerm);
103: poNames[1] = "Postconditions";
104: } catch (SLTranslationError e) {
105: throw new ProofInputException(e);
106: }
107:
108: //register everything in namespaces
109: registerInNamespaces(selfVar);
110: registerInNamespaces(paramVars);
111: registerInNamespaces(resultVar);
112: registerInNamespaces(exceptionVar);
113: registerInNamespaces(atPreFunctions);
114: }
115:
116: public Contractable[] getObjectOfContract() {
117: return new Contractable[0];
118: }
119:
120: public boolean initContract(Contract ct) {
121: return false;
122: }
123:
124: //-------------------------------------------------------------------------
125:
126: protected Term getTerm1() {
127: return poTerms[0];
128: }
129:
130: protected Term getTerm2() {
131: return poTerms[1];
132: }
133: }
|