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: //
009: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
011: // Universitaet Koblenz-Landau, Germany
012: // Chalmers University of Technology, Sweden
013: //
014: // The KeY system is protected by the GNU General Public License.
015: // See LICENSE.TXT for details.
016:
017: //
018: //
019:
020: package de.uka.ilkd.key.proof;
021:
022: import java.util.*;
023:
024: import de.uka.ilkd.key.logic.*;
025: import de.uka.ilkd.key.logic.op.*;
026: import de.uka.ilkd.key.logic.sort.Sort;
027: import de.uka.ilkd.key.util.Debug;
028:
029: /**
030: * Transformation according to Sect. 3.3.2 of "Eine modifies-Klausel in
031: * KeY" by Bastian Katz
032: */
033: public class MethodSpecTransformation {
034:
035: private final Term hoare;
036:
037: /**
038: * Maps from <code>Term</code> to <code>LogicVariable</code> describing
039: * the flattening of pre and postconditions
040: */
041: private final Map preFunctions = new HashMap();
042: private final Map postFunctions = new HashMap();
043:
044: private final Map logicVariableTerms = new HashMap();
045: private final Map operators = new HashMap();
046: private final Set postsubterms = new HashSet();
047:
048: private final TermFactory tf = TermFactory.DEFAULT;
049:
050: private void putPreFunction(Term t, LogicVariable var) {
051: preFunctions.put(t, var);
052: }
053:
054: private void putPostFunction(Term t, LogicVariable var) {
055: postFunctions.put(t, var);
056: }
057:
058: private LogicVariable getPreFunctionVar(Term t) {
059: return (LogicVariable) preFunctions.get(t);
060: }
061:
062: private LogicVariable getPostFunctionVar(Term t) {
063: return (LogicVariable) postFunctions.get(t);
064: }
065:
066: private void putOperator(Operator op, Term t) {
067: operators.put(op, t);
068: }
069:
070: private Term getTermFor(LogicVariable var) {
071: Term res = (Term) logicVariableTerms.get(var);
072: if (res == null) {
073: res = tf.createVariableTerm(var);
074: logicVariableTerms.put(var, res);
075: }
076: return res;
077: }
078:
079: private JavaBlock getJavablock() {
080: return (hoare.sub(1)).javaBlock();
081: }
082:
083: private Term getPostcondition() {
084: return hoare.sub(1).sub(0);
085: }
086:
087: private Term getPrecondition() {
088: return hoare.sub(0);
089: }
090:
091: public static Term getTransformedHoare(Term hoare) {
092: // refactoring "method object"
093: return new MethodSpecTransformation(hoare).transformHoare();
094: }
095:
096: private MethodSpecTransformation(Term hoare) {
097: this .hoare = hoare;
098: }
099:
100: private Term transformHoare() {
101: setupPostSubTerms(getPostcondition());
102:
103: final Term purePrecondition = purifyPrecondition(getPrecondition());
104:
105: final Set neededTermsLeft = new HashSet();
106: final Set neededTermsRight = new HashSet();
107:
108: // The next three calls are performed only to find out about terms that
109: // are needed (update <code>neededTermsLeft</code>,
110: // <code>neededTermsRight</code>)
111: getConjunction(preFunctions, neededTermsLeft);
112: getConjunction(postFunctions, neededTermsRight);
113: substitute(getPostcondition(), neededTermsRight);
114:
115: removeUnneededTerms(neededTermsLeft, neededTermsRight);
116:
117: final Term prefix2 = removePres(getConjunction(preFunctions,
118: neededTermsLeft));
119: final Term suffix = getConjunction(postFunctions,
120: neededTermsRight);
121: final Term substPostcondition = substitute(getPostcondition(),
122: neededTermsRight);
123:
124: // <code>createJunctorTermAndSimplify</code> cannot be used for the
125: // following formulas, because the resulting term is expected to have a
126: // particular shape
127: final Term prefix = tf.createJunctorTerm(Op.AND,
128: purePrecondition, prefix2);
129: final Term postImplication = tf.createJunctorTerm(Op.IMP,
130: suffix, substPostcondition);
131: final Term diamondTerm = tf.createDiamondTerm(getJavablock(),
132: postImplication);
133:
134: Term res = tf.createJunctorTerm(Op.IMP, prefix, diamondTerm);
135:
136: // add necessary quantifiers
137: res = addAllQuantifiers(res, preFunctions.values());
138: res = addAllQuantifiers(res, postFunctions.values());
139:
140: return res;
141: }
142:
143: private Term addAllQuantifiers(Term res, Collection variables) {
144: final Iterator it = variables.iterator();
145: while (it.hasNext())
146: res = tf.createQuantifierTerm(Op.ALL,
147: (QuantifiableVariable) it.next(), res);
148: return res;
149: }
150:
151: private void removeUnneededTerms(Set neededTermsLeft,
152: Set neededTermsRight) {
153: final Set remove = new HashSet();
154: findUnneededTerms(neededTermsLeft, postFunctions, remove);
155: findUnneededTerms(neededTermsRight, preFunctions, remove);
156:
157: postFunctions.keySet().removeAll(remove);
158: preFunctions.keySet().removeAll(remove);
159: }
160:
161: /**
162: * Given a set <code>neededVarTerms</code> of variable terms that are
163: * needed, determine all related original terms (as given by the mapping
164: * <code>termsToVars</code>) and insert them into the collection
165: * <code>unneeded</code>
166: */
167: private void findUnneededTerms(Set neededVarTerms, Map termsToVars,
168: Collection unneeded) {
169: final Iterator it = termsToVars.entrySet().iterator();
170: while (it.hasNext()) {
171: final Map.Entry entry = (Map.Entry) it.next();
172: final Term t = (Term) entry.getKey();
173: final LogicVariable var = (LogicVariable) entry.getValue();
174: if (!neededVarTerms.contains(getTermFor(var)))
175: unneeded.add(t);
176: }
177: }
178:
179: private Term removePres(Term t) {
180: checkForBoundVariables(t);
181:
182: Term[] subs = new Term[t.arity()];
183: boolean changed = false;
184: for (int i = 0; i < subs.length; i++) {
185: subs[i] = removePres(t.sub(i));
186: if (subs[i] != t.sub(i))
187: changed = true;
188: }
189:
190: if (operators.containsKey(t.op())) {
191: t = (Term) operators.get(t.op());
192: if (t.op() instanceof AttributeOp)
193: subs = new Term[] { subs[0] };
194: changed = true;
195: }
196:
197: if (changed)
198: return buildTerm(t.op(), subs, t.javaBlock());
199:
200: return t;
201: }
202:
203: private Term substitute(Term from, Set notifyUsage) {
204:
205: // test if term <code>from</code> is contained in one of the mappings;
206: // in this case return the variable the term is mapped to
207: LogicVariable varForFrom = getPreFunctionVar(from);
208: if (varForFrom == null)
209: varForFrom = getPostFunctionVar(from);
210: if (varForFrom != null) {
211: final Term t = getTermFor(varForFrom);
212: notifyUsage.add(t);
213: return t;
214: }
215:
216: checkForBoundVariables(from);
217:
218: final BooleanContainer changed = new BooleanContainer();
219: final Term subTerms[] = substituteSubterms(from, notifyUsage,
220: changed);
221:
222: Operator top = from.op();
223: if (operators.containsKey(top)) {
224: top = ((Term) operators.get(top)).op();
225: changed.setVal(true);
226: }
227:
228: if (changed.val())
229: return buildTerm(top, subTerms, from.javaBlock());
230: return from;
231: }
232:
233: private void checkForBoundVariables(Term t) {
234: for (int i = 0; i != t.arity(); ++i)
235: Debug.assertTrue(t.varsBoundHere(i).size() == 0,
236: "MethodSpecTransformation does not support "
237: + "quantifiers at this point!\n" + "Term "
238: + t + " cannot be handled");
239: }
240:
241: /**
242: * Given a mapping <code>termsToVars</code> of terms to variables, create
243: * a conjunction of equations <code>x=t</code>, where <code>t</code> is
244: * obtained by replacing the direct subterms of a term of the mapping with
245: * the related variables
246: */
247: private Term getConjunction(Map termsToVars, Set needed) {
248: Term result = tf.createJunctorTerm(Op.TRUE);
249:
250: final Iterator it = termsToVars.entrySet().iterator();
251: while (it.hasNext()) {
252: final Map.Entry entry = (Map.Entry) it.next();
253: final Term term = (Term) entry.getKey();
254: final Term varTerm = getTermFor((LogicVariable) entry
255: .getValue());
256:
257: needed.add(varTerm);
258: final Term changedMap = tf.createTerm(term.op(),
259: substituteSubterms(term, needed, null),
260: new QuantifiableVariable[0], term.javaBlock());
261: final Term resPart = tf.createEqualityTerm(varTerm,
262: changedMap);
263:
264: result = tf.createJunctorTermAndSimplify(Op.AND, result,
265: resPart);
266: }
267:
268: return result;
269: }
270:
271: /**
272: * Invoke the method <code>substitute</code> on all direct subterms of
273: * <code>term</code>
274: *
275: * @param changed
276: * if a non-null boolean container is given, store
277: * <code>true</code> iff one of the subterms was changed by the
278: * invocation
279: */
280: private Term[] substituteSubterms(Term term, Set needed,
281: BooleanContainer changed) {
282: if (changed != null)
283: changed.setVal(false);
284: final Term[] subTerms = new Term[term.arity()];
285: for (int i = 0; i < term.arity(); i++) {
286: subTerms[i] = substitute(term.sub(i), needed);
287: if (changed != null && !subTerms[i].equals(term.sub(i)))
288: changed.setVal(true);
289: }
290: return subTerms;
291: }
292:
293: /**
294: * Store all subterms of <code>t</code> in the attribute
295: * <code>postsubterms</code>
296: *
297: * @param t
298: * Term whose subterms are supposed to be determined
299: */
300: private void setupPostSubTerms(Term t) {
301: if (!postsubterms.contains(t)) {
302: postsubterms.add(t);
303:
304: if (t.sort() != Sort.FORMULA) {
305: final LogicVariable subst = new LogicVariable(new Name(
306: "_tauV" + postsubterms.size()), t.sort());
307:
308: if (opIsAtPre(t))
309: putPreFunction(t, subst);
310: else
311: putPostFunction(t, subst);
312: }
313:
314: for (int i = 0; i < t.arity(); i++)
315: setupPostSubTerms(t.sub(i));
316: }
317: }
318:
319: public static boolean opIsAtPre(Term t) {
320: return t.op() instanceof Function
321: && ((Function) t.op()).name().toString()
322: .indexOf("@pre") > -1;
323: }
324:
325: public static boolean isAtPreDefinition(final Term pre) {
326: return pre.op() == Op.ALL
327: && pre.sub(0).op() instanceof de.uka.ilkd.key.logic.op.Equality
328: && opIsAtPre(pre.sub(0).sub(0));
329: }
330:
331: /**
332: * Remove premisses defining the helper functions for
333: * @pre from the precondition
334: */
335: private Term purifyPrecondition(final Term pre) {
336: if (isAtPreDefinition(pre)) {
337: // replace formulas
338: // all x. f@pre(...) = t
339: // with TRUE
340: putOperator(pre.sub(0).sub(0).op(), pre.sub(0).sub(1));
341: return tf.createJunctorTerm(Op.TRUE);
342: }
343:
344: checkForBoundVariables(pre);
345:
346: boolean changed = false;
347: final Term subTerms[] = new Term[pre.arity()];
348: for (int i = 0; i < pre.arity(); i++) {
349: subTerms[i] = purifyPrecondition(pre.sub(i));
350: if (!subTerms[i].equals(pre.sub(i)))
351: changed = true;
352: }
353:
354: if (changed)
355: return buildTerm(pre.op(), subTerms, pre.javaBlock());
356:
357: return pre;
358: }
359:
360: private final static ArrayOfQuantifiableVariable EMPTY_ARRAY_OF_VARIABLES = new ArrayOfQuantifiableVariable();
361:
362: private Term buildTerm(Operator op, Term[] subTerms,
363: JavaBlock javaBlock) {
364: if (op instanceof Junctor && subTerms.length == 2)
365: return tf.createJunctorTermAndSimplify((Junctor) op,
366: subTerms[0], subTerms[1]);
367: return tf.createTerm(op, subTerms, EMPTY_ARRAY_OF_VARIABLES,
368: javaBlock);
369: }
370: }
|