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.Map;
011:
012: import de.uka.ilkd.key.logic.*;
013: import de.uka.ilkd.key.logic.op.Modality;
014: import de.uka.ilkd.key.logic.op.ProgramVariable;
015: import de.uka.ilkd.key.proof.SymbolReplacer;
016:
017: /**
018: * @deprecated
019: */
020: public class InstantiatedMethodContract {
021:
022: private Term pre;
023: private Term post;
024: private Term atPreAxioms;
025: private SetOfLocationDescriptor modifies;
026: private Modality modality;
027: private ProgramVariable exc;
028: private Namespace functions;
029: private Namespace programVariables;
030:
031: public static InstantiatedMethodContract create(Map m, Term pre,
032: Term post, Term atPreAxioms, SetOfLocationDescriptor mods,
033: Modality modality, ProgramVariable exc,
034: Namespace functions, Namespace programVariables) {
035: assert modality != null;
036:
037: final SymbolReplacer pvr = new SymbolReplacer(m);
038: return new InstantiatedMethodContract(replace(pvr, pre),
039: replace(pvr, post), replace(pvr, atPreAxioms), replace(
040: pvr, mods), modality, exc, functions,
041: programVariables);
042: }
043:
044: /**
045: * replaces the template locations in term <tt>t</tt> by the concrete ones
046: * contained in the instantiation map of pvr
047: * @param pvr the SymbolReplacer
048: * @param t the Term whose location templates are instantiated
049: * @return the instantiated term <tt>t</tt>
050: */
051: private static Term replace(SymbolReplacer pvr, Term t) {
052: return pvr.replace(t);
053: }
054:
055: /**
056: * used to replace the template locations used in LocationDescriptor by the one
057: * in the replacement map of <tt>pvr</tt>
058: * @param pvr the SymbolReplacer
059: * @param mods the SetOfLocationDescriptor to be instantiated
060: * @return the instantiated set of location descriptors
061: */
062: private static SetOfLocationDescriptor replace(SymbolReplacer pvr,
063: SetOfLocationDescriptor mods) {
064: SetOfLocationDescriptor result = SetAsListOfLocationDescriptor.EMPTY_SET;
065: final IteratorOfLocationDescriptor it = mods.iterator();
066: while (it.hasNext()) {
067: result = result.add(pvr.replace(it.next()));
068: }
069: return result;
070: }
071:
072: private InstantiatedMethodContract(Term pre, Term post,
073: Term atPreAxioms, SetOfLocationDescriptor mods,
074: Modality modality, ProgramVariable exc,
075: Namespace functions, Namespace programVariables) {
076: this .pre = pre;
077: this .atPreAxioms = atPreAxioms;
078: this .post = post;
079: this .modifies = mods;
080: this .modality = modality;
081: this .exc = exc;
082: this .functions = functions;
083: this .programVariables = programVariables;
084: }
085:
086: public Term getPre() {
087: return pre;
088: }
089:
090: public Term getPost() {
091: return post;
092: }
093:
094: public Term getAtPreAxioms() {
095: return atPreAxioms;
096: }
097:
098: public SetOfLocationDescriptor getModifies() {
099: return modifies;
100: }
101:
102: public Modality getModality() {
103: return modality;
104: }
105:
106: public ProgramVariable getExceptionVariable() {
107: return exc;
108: }
109:
110: public Namespace getAdditionalProgramVariables() {
111: return programVariables;
112: }
113:
114: public Namespace getAdditionalFunctions() {
115: return functions;
116: }
117:
118: }
|