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.speclang;
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.java.Services;
025: import de.uka.ilkd.key.logic.BasicLocationDescriptor;
026: import de.uka.ilkd.key.logic.EverythingLocationDescriptor;
027: import de.uka.ilkd.key.logic.IteratorOfLocationDescriptor;
028: import de.uka.ilkd.key.logic.LocationDescriptor;
029: import de.uka.ilkd.key.logic.SetAsListOfLocationDescriptor;
030: import de.uka.ilkd.key.logic.SetOfLocationDescriptor;
031: import de.uka.ilkd.key.logic.Term;
032: import de.uka.ilkd.key.logic.op.IteratorOfParsableVariable;
033: import de.uka.ilkd.key.logic.op.ListOfParsableVariable;
034: import de.uka.ilkd.key.logic.op.Modality;
035: import de.uka.ilkd.key.logic.op.ParsableVariable;
036: import de.uka.ilkd.key.proof.OpReplacer;
037:
038: public class DLOperationContract extends AbstractOperationContract {
039: private final Term originalPre;
040: private final Term originalPost;
041: private final SetOfLocationDescriptor originalModifies;
042: private final ParsableVariable originalSelfVar;
043: private final ListOfParsableVariable originalParamVars;
044: private final ParsableVariable originalResultVar;
045: private final ParsableVariable originalExcVar;
046: private final Map /*Operator -> Term*/axioms;
047:
048: public DLOperationContract(ModelMethod modelMethod,
049: Modality modality, Term originalPre, Term originalPost,
050: SetOfLocationDescriptor originalModifies,
051: ParsableVariable originalSelfVar,
052: ListOfParsableVariable originalParamVars,
053: ParsableVariable originalResultVar,
054: ParsableVariable originalExcVar,
055: Map /*Operator -> Term*/axioms) {
056: super (modelMethod, modality);
057: this .originalPre = originalPre;
058: this .originalPost = originalPost;
059: this .originalModifies = originalModifies;
060: this .originalSelfVar = originalSelfVar;
061: this .originalParamVars = originalParamVars;
062: this .originalResultVar = originalResultVar;
063: this .originalExcVar = originalExcVar;
064: this .axioms = axioms;
065: }
066:
067: private Map /*Operator -> Operator*/getReplaceMap(
068: ParsableVariable selfVar, ListOfParsableVariable paramVars,
069: ParsableVariable resultVar, ParsableVariable excVar) {
070: Map result = new HashMap();
071:
072: if (selfVar != null) {
073: assert originalSelfVar.sort().equals(selfVar.sort());
074: result.put(originalSelfVar, selfVar);
075: }
076:
077: if (paramVars != null) {
078: assert originalParamVars.size() == paramVars.size();
079: IteratorOfParsableVariable it1 = originalParamVars
080: .iterator();
081: IteratorOfParsableVariable it2 = paramVars.iterator();
082: while (it1.hasNext()) {
083: ParsableVariable originalParamVar = it1.next();
084: ParsableVariable paramVar = it2.next();
085: assert originalParamVar.sort().equals(paramVar.sort());
086: result.put(originalParamVar, paramVar);
087: }
088: }
089:
090: if (resultVar != null) {
091: assert originalResultVar.sort().equals(resultVar.sort());
092: result.put(originalResultVar, resultVar);
093: }
094:
095: if (excVar != null) {
096: assert originalExcVar.sort().equals(excVar.sort());
097: result.put(originalExcVar, excVar);
098: }
099:
100: return result;
101: }
102:
103: public FormulaWithAxioms getPre(ParsableVariable selfVar,
104: ListOfParsableVariable paramVars, Services services) {
105: Map replaceMap = getReplaceMap(selfVar, paramVars, null, null);
106: OpReplacer or = new OpReplacer(replaceMap);
107:
108: return new FormulaWithAxioms(or.replace(originalPre), axioms);
109: }
110:
111: public FormulaWithAxioms getPost(ParsableVariable selfVar,
112: ListOfParsableVariable paramVars,
113: ParsableVariable resultVar, ParsableVariable excVar,
114: Services services) {
115: Map replaceMap = getReplaceMap(selfVar, paramVars, resultVar,
116: excVar);
117: OpReplacer or = new OpReplacer(replaceMap);
118:
119: return new FormulaWithAxioms(or.replace(originalPost), axioms);
120: }
121:
122: public SetOfLocationDescriptor getModifies(
123: ParsableVariable selfVar, ListOfParsableVariable paramVars,
124: Services services) {
125: Map replaceMap = getReplaceMap(selfVar, paramVars, null, null);
126: OpReplacer or = new OpReplacer(replaceMap);
127:
128: SetOfLocationDescriptor result = SetAsListOfLocationDescriptor.EMPTY_SET;
129: IteratorOfLocationDescriptor it = originalModifies.iterator();
130: while (it.hasNext()) {
131: LocationDescriptor loc = it.next();
132: if (loc instanceof BasicLocationDescriptor) {
133: BasicLocationDescriptor bloc = (BasicLocationDescriptor) loc;
134: Term unifiedFormula = or.replace(bloc.getFormula());
135: Term unifiedLocTerm = or.replace(bloc.getLocTerm());
136: result = result.add(new BasicLocationDescriptor(
137: unifiedFormula, unifiedLocTerm));
138: } else {
139: assert loc instanceof EverythingLocationDescriptor;
140: result = result.add(loc);
141: }
142: }
143:
144: return result;
145: }
146: }
|