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.ListOfClassInvariant;
030: import de.uka.ilkd.key.speclang.OperationContract;
031: import de.uka.ilkd.key.speclang.SLTranslationError;
032:
033: /**
034: * The "StrongOperationContract" proof obligation.
035: */
036: public class StrongOperationContractPO extends AbstractPO {
037:
038: private final OperationContract contract;
039: private final ListOfClassInvariant assumedInvs;
040: private final ListOfClassInvariant ensuredInvs;
041:
042: //-------------------------------------------------------------------------
043: //constructors
044: //-------------------------------------------------------------------------
045:
046: public StrongOperationContractPO(OperationContract contract,
047: ListOfClassInvariant assumedInvs,
048: ListOfClassInvariant ensuredInvs) {
049: super (
050: "StrongOperationContract of "
051: + contract.getModelMethod(), contract
052: .getModelMethod().getContainingClass());
053: this .contract = contract;
054: this .assumedInvs = assumedInvs;
055: this .ensuredInvs = ensuredInvs;
056: }
057:
058: //-------------------------------------------------------------------------
059: //methods of ProofOblInput interface
060: //-------------------------------------------------------------------------
061:
062: public void readProblem(ModStrategy mod) throws ProofInputException {
063: //make sure initConfig has been set
064: if (initConfig == null) {
065: throw new IllegalStateException("InitConfig not set.");
066: }
067:
068: //prepare variables and container for @pre-functions
069: ModelMethod modelMethod = contract.getModelMethod();
070: ProgramVariable selfVar = buildSelfVarAsProgVar();
071: ListOfProgramVariable paramVars = buildParamVars(modelMethod);
072: ProgramVariable resultVar = buildResultVar(modelMethod);
073: ProgramVariable exceptionVar = buildExcVar();
074: Map atPreFunctions = new HashMap();
075:
076: try {
077: //translate precondition
078: Term preTerm = translatePre(contract, selfVar,
079: toPV(paramVars));
080:
081: //translate and conjoin assumed invariants
082: Term assumedInvsTerm = translateInvs(assumedInvs);
083:
084: //translate postcondition
085: Term postTerm = translatePost(contract, selfVar,
086: toPV(paramVars), resultVar, exceptionVar);
087:
088: //translate and conjoin ensured invariants
089: Term ensuredInvsTerm = translateInvs(ensuredInvs);
090:
091: //build post implication with updates
092: Term postImpTerm = tb.imp(postTerm, ensuredInvsTerm);
093: Term postUpdateTerm = translateModifies(contract,
094: postImpTerm, selfVar, toPV(paramVars));
095:
096: //build definitions for @pre-functions
097: Term atPreDefinitionsTerm = buildAtPreDefinitions(atPreFunctions);
098:
099: //put together @pre-definitions, precondition, and assumed invariants
100: Term defAndPreAndAssumedInvsTerm = tb.and(
101: atPreDefinitionsTerm, tb.and(preTerm,
102: assumedInvsTerm));
103:
104: //build top level implication
105: Term poTerm = tb.imp(defAndPreAndAssumedInvsTerm,
106: postUpdateTerm);
107: poTerms = new Term[] { poTerm };
108: } catch (SLTranslationError e) {
109: throw new ProofInputException(e);
110: }
111:
112: //register everything in namespaces
113: registerInNamespaces(selfVar);
114: registerInNamespaces(paramVars);
115: registerInNamespaces(resultVar);
116: registerInNamespaces(exceptionVar);
117: registerInNamespaces(atPreFunctions);
118: }
119:
120: public Contractable[] getObjectOfContract() {
121: return new Contractable[0];
122: }
123:
124: public boolean initContract(Contract ct) {
125: return false;
126: }
127: }
|