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: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
009: // Universitaet Koblenz-Landau, Germany
010: // Chalmers University of Technology, Sweden
011: //
012: // The KeY system is protected by the GNU General Public License.
013: // See LICENSE.TXT for details.
014: //
015: //
016:
017: package de.uka.ilkd.key.proof.init;
018:
019: import java.util.Map;
020:
021: import de.uka.ilkd.key.java.ArrayOfExpression;
022: import de.uka.ilkd.key.java.PositionInfo;
023: import de.uka.ilkd.key.java.StatementBlock;
024: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
025: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
026: import de.uka.ilkd.key.logic.JavaBlock;
027: import de.uka.ilkd.key.logic.ProgramElementName;
028: import de.uka.ilkd.key.logic.Term;
029: import de.uka.ilkd.key.logic.op.*;
030: import de.uka.ilkd.key.logic.sort.Sort;
031: import de.uka.ilkd.key.speclang.OperationContract;
032: import de.uka.ilkd.key.speclang.SLTranslationError;
033: import de.uka.ilkd.key.util.ExtList;
034:
035: /**
036: * The "RespectsModifies" proof obligation.
037: */
038: public class RespectsModifiesPO extends EnsuresPO {
039:
040: private final OperationContract contract;
041: private Term updateAnonMethodTerm = null;
042:
043: public RespectsModifiesPO(OperationContract contract,
044: InvariantSelectionStrategy invStrategy) {
045: super ("RespectsModifies", contract.getModelMethod(),
046: Modality.BOX, invStrategy, true);
047: this .contract = contract;
048: }
049:
050: private void buildUpdateAnonMethodTerm(ProgramVariable selfVar,
051: ListOfProgramVariable paramVars) throws SLTranslationError {
052: if (updateAnonMethodTerm != null) {
053: return;
054: }
055:
056: //build method declaration
057: ExtList extList = new ExtList();
058: ProgramElementName name = new ProgramElementName("anonMethod");
059: extList.addLast(name);
060: MethodDeclaration methodDecl = new MethodDeclaration(extList,
061: false);
062:
063: //build program method
064: ProgramMethod programMethod = new ProgramMethod(methodDecl,
065: javaInfo.getJavaLangObject(), javaInfo
066: .getJavaLangObject(), PositionInfo.UNDEFINED);
067:
068: //build java block
069: ProgramVariable pseudoSelfVar = new LocationVariable(
070: new ProgramElementName("anonObject"), Sort.NULL);
071: MethodBodyStatement call = new MethodBodyStatement(
072: programMethod, pseudoSelfVar, null,
073: new ArrayOfExpression());/*paramVars*/
074: StatementBlock sb = new StatementBlock(call);
075: JavaBlock jb = JavaBlock.createJavaBlock(sb);
076:
077: //build program term
078: Term programTerm = tb.dia(jb, tb.tt());
079:
080: //add update
081: updateAnonMethodTerm = translateModifies(contract, programTerm,
082: selfVar, toPV(paramVars));
083: }
084:
085: protected Term getPreTerm(ProgramVariable selfVar,
086: ListOfProgramVariable paramVars, ProgramVariable resultVar,
087: ProgramVariable exceptionVar, Map atPreFunctions)
088: throws SLTranslationError {
089: buildUpdateAnonMethodTerm(selfVar, paramVars);
090: Term preTerm = translatePre(contract, selfVar, toPV(paramVars));
091: Term result = tb.and(preTerm, updateAnonMethodTerm);
092: return result;
093: }
094:
095: protected Term getPostTerm(ProgramVariable selfVar,
096: ListOfProgramVariable paramVars, ProgramVariable resultVar,
097: ProgramVariable exceptionVar, Map atPreFunctions)
098: throws SLTranslationError {
099: buildUpdateAnonMethodTerm(selfVar, paramVars);
100: createAtPreFunctionsForTerm(updateAnonMethodTerm,
101: atPreFunctions);
102: Term result = replaceOps(atPreFunctions, updateAnonMethodTerm);
103: return result;
104: }
105: }
|