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: package de.uka.ilkd.key.proof.mgt;
009:
010: import java.util.HashMap;
011: import java.util.Iterator;
012: import java.util.Map;
013:
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.statement.CatchAllStatement;
016: import de.uka.ilkd.key.logic.Namespace;
017: import de.uka.ilkd.key.logic.ProgramElementName;
018: import de.uka.ilkd.key.logic.Term;
019: import de.uka.ilkd.key.logic.op.LocationVariable;
020: import de.uka.ilkd.key.logic.op.ProgramVariable;
021: import de.uka.ilkd.key.proof.Proof;
022:
023: /**
024: * @deprecated
025: */
026: public abstract class DefaultOperationContract extends AbstractContract
027: implements OldOperationContract, HoareTripleContract {
028:
029: protected abstract Term getAdditionalAxioms();
030:
031: public InstantiatedMethodContract instantiate(
032: MethodContractInstantiation insts, Proof proof) {
033:
034: final Services services = proof.getServices();
035:
036: final Namespace localFunctions = new Namespace();
037: final Namespace localProgramVariables = new Namespace();
038: final Map replacementMap = new HashMap();
039:
040: instantiateMethodParameters(insts, replacementMap,
041: localFunctions, localProgramVariables);
042:
043: instantiateMethodReceiver(insts, replacementMap,
044: localFunctions, localProgramVariables);
045:
046: instantiateMethodReturnVariable(insts, replacementMap,
047: localFunctions, localProgramVariables);
048:
049: final ProgramVariable excVar = instantiateCatchAllStatement(
050: getCatchAllStatement(), replacementMap, localFunctions,
051: localProgramVariables, services);
052:
053: instantiateAtPreSymbols(replacementMap, localFunctions,
054: localProgramVariables);
055:
056: instantiateAuxiliarySymbols(replacementMap, localFunctions,
057: localProgramVariables, proof.getServices());
058: return InstantiatedMethodContract.create(replacementMap,
059: getPre(), getPost(), getAdditionalAxioms(),
060: getModifies(), insts.getModality(), excVar,
061: localFunctions, localProgramVariables);
062: }
063:
064: public abstract CatchAllStatement getCatchAllStatement();
065:
066: protected abstract void instantiateAuxiliarySymbols(
067: Map replacementMap, Namespace localFunctions,
068: Namespace localProgramVariables, Services services);
069:
070: /**
071: * @param insts
072: * @param replacementMap
073: * @param localProgramVariables
074: * @param localFunctions
075: */
076: protected abstract void instantiateMethodReturnVariable(
077: MethodContractInstantiation insts, Map replacementMap,
078: Namespace localFunctions, Namespace localProgramVariables);
079:
080: /**
081: * @param localProgramVariables
082: * @param replacementMap
083: * @param ca
084: * @return
085: */
086: protected ProgramVariable instantiateCatchAllStatement(
087: CatchAllStatement ca, Map replacementMap,
088: Namespace localFunctions, Namespace localProgramVariables,
089: Services services) {
090:
091: ProgramVariable excVar = null;
092: if (ca != null) {
093: final ProgramVariable paramPV = (ProgramVariable) ca
094: .getParameterDeclaration()
095: .getVariableSpecification().getProgramVariable();
096:
097: final ProgramElementName catchAllInstantiadParameterName = services
098: .getVariableNamer().getTemporaryNameProposal(
099: paramPV.name().toString());
100:
101: excVar = new LocationVariable(
102: catchAllInstantiadParameterName, paramPV
103: .getKeYJavaType());
104: replacementMap.put(paramPV, excVar);
105: localProgramVariables.add(excVar);
106: }
107: return excVar;
108: }
109:
110: /**
111: * @param insts
112: * @param replacementMap
113: * @param localProgramVariables
114: * @param localFunctions
115: */
116: protected abstract void instantiateMethodReceiver(
117: MethodContractInstantiation insts, Map replacementMap,
118: Namespace localFunctions, Namespace localProgramVariables);
119:
120: /**
121: * @param insts
122: * @param replacementMap
123: * @param localProgramVariables
124: * @param localFunctions
125: */
126: protected abstract void instantiateMethodParameters(
127: MethodContractInstantiation insts, Map replacementMap,
128: Namespace localFunctions, Namespace localProgramVariables);
129:
130: protected abstract void instantiateAtPreSymbols(Map replacementMap,
131: Namespace localFunctions, Namespace localProgramVariables);
132:
133: }
|