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.casetool.IteratorOfModelClass;
022: import de.uka.ilkd.key.casetool.ListOfModelClass;
023: import de.uka.ilkd.key.casetool.ModelClass;
024: import de.uka.ilkd.key.casetool.ModelMethod;
025: import de.uka.ilkd.key.gui.DependsClauseDialog;
026: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
027: import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
028: import de.uka.ilkd.key.logic.*;
029: import de.uka.ilkd.key.logic.op.*;
030: import de.uka.ilkd.key.logic.sort.Sort;
031: import de.uka.ilkd.key.speclang.ClassInvariant;
032: import de.uka.ilkd.key.speclang.IteratorOfClassInvariant;
033: import de.uka.ilkd.key.speclang.ListOfClassInvariant;
034: import de.uka.ilkd.key.speclang.SLTranslationError;
035: import de.uka.ilkd.key.util.Debug;
036:
037: /**
038: * The "PreservesGuard" proof obligation.
039: */
040: public class PreservesGuardPO extends EnsuresPO {
041:
042: private final ListOfClassInvariant guardedInvs;
043: private final ListOfModelClass guard;
044: private Term encapsulationFormula = null;
045: private ListOfProofOblInput dependsPOs = SLListOfProofOblInput.EMPTY_LIST;
046:
047: public PreservesGuardPO(ModelMethod modelMethod,
048: ListOfClassInvariant guardedInvs, ListOfModelClass guard,
049: InvariantSelectionStrategy invStrategy) {
050: super ("PreservesGuard", modelMethod, Op.BOX, invStrategy, false);
051: this .guardedInvs = guardedInvs;
052: this .guard = guard;
053: }
054:
055: /**
056: * Retrieves the "Acc" predicate.
057: */
058: private Function getAccPred() throws ProofInputException {
059: Function accFunc = (Function) initConfig.funcNS().lookup(
060: new Name("Acc"));
061:
062: if (accFunc == null) {
063: throw new ProofInputException(
064: "Could not find the \"Acc\" predicate.\n"
065: + "Please make sure the corresponding library is active.");
066: }
067:
068: return accFunc;
069: }
070:
071: /**
072: * Extracts a depends clause syntactically from a term
073: * (helper for getDependsClauseForInv()).
074: */
075: private SetOfLocationDescriptor extractDependsClauseFromTerm(
076: Term term) {
077: SetOfLocationDescriptor result = SetAsListOfLocationDescriptor.EMPTY_SET;
078:
079: for (int i = 0; i < term.arity(); i++) {
080: result = result.union(extractDependsClauseFromTerm(term
081: .sub(i)));
082: }
083:
084: if (term.op() instanceof NonRigid) {
085: result = result.add(new BasicLocationDescriptor(term));
086: }
087:
088: return result;
089: }
090:
091: /**
092: * Removes elements from a depends clause whose top level operator is
093: * declared in a guard class (helper for getDependsClauseForInv()).
094: */
095: private SetOfLocationDescriptor filterDependsClause(
096: SetOfLocationDescriptor clause) {
097: IteratorOfLocationDescriptor it = clause.iterator();
098: while (it.hasNext()) {
099: LocationDescriptor loc = it.next();
100:
101: if (loc instanceof BasicLocationDescriptor) {
102: Operator op = ((BasicLocationDescriptor) loc)
103: .getLocTerm().op();
104:
105: KeYJavaType containingKjt = null;
106: if (op instanceof ProgramVariable) {
107: containingKjt = ((ProgramVariable) op)
108: .getContainerType();
109: } else if (op instanceof AttributeOp) {
110: AttributeOp aop = (AttributeOp) op;
111: if (aop.attribute() instanceof ProgramVariable) {
112: containingKjt = ((ProgramVariable) aop
113: .attribute()).getContainerType();
114: }
115: }
116:
117: if (containingKjt != null) {
118: IteratorOfModelClass it2 = guard.iterator();
119: while (it2.hasNext()) {
120: ModelClass guardClass = it2.next();
121: KeYJavaType guardKjt = javaInfo
122: .getKeYJavaType(guardClass
123: .getFullClassName());
124: if (containingKjt.equals(guardKjt)) {
125: clause = clause.remove(loc);
126: }
127: }
128: }
129: }
130: }
131:
132: return clause;
133: }
134:
135: /**
136: * Compares two sets of location descriptors
137: * (helper for getDependsClauseForInv()).
138: */
139: private boolean equalsModRenaming(SetOfLocationDescriptor locs1,
140: SetOfLocationDescriptor locs2) {
141: if (locs1.size() != locs2.size()) {
142: return false;
143: }
144:
145: Function pred = new RigidFunction(new Name(""), Sort.FORMULA,
146: new Sort[] { Sort.ANY });
147:
148: IteratorOfLocationDescriptor it1 = locs1.iterator();
149: while (it1.hasNext()) {
150: LocationDescriptor loc1 = it1.next();
151: if (!(loc1 instanceof BasicLocationDescriptor)) {
152: continue;
153: }
154: BasicLocationDescriptor bloc1 = (BasicLocationDescriptor) loc1;
155:
156: Term predLoc1Term = tf.createFunctionTerm(pred, bloc1
157: .getLocTerm());
158: Term freeLoc1Term = tf.createJunctorTerm(Op.AND, bloc1
159: .getFormula(), predLoc1Term);
160: Term boundLoc1Term = tf.createQuantifierTerm(Op.ALL,
161: freeLoc1Term.freeVars().toArray(), freeLoc1Term);
162:
163: IteratorOfLocationDescriptor it2 = locs2.iterator();
164: boolean found = false;
165: while (it2.hasNext()) {
166: LocationDescriptor loc2 = it2.next();
167: if (!(loc2 instanceof BasicLocationDescriptor)) {
168: continue;
169: }
170: BasicLocationDescriptor bloc2 = (BasicLocationDescriptor) loc2;
171:
172: Term predLoc2Term = tf.createFunctionTerm(pred, bloc2
173: .getLocTerm());
174: Term freeLoc2Term = tf.createJunctorTerm(Op.AND, bloc2
175: .getFormula(), predLoc2Term);
176: Term boundLoc2Term = tf
177: .createQuantifierTerm(Op.ALL, freeLoc2Term
178: .freeVars().toArray(), freeLoc2Term);
179:
180: if (boundLoc1Term.equalsModRenaming(boundLoc2Term)) {
181: locs2 = locs2.remove(loc2);
182: found = true;
183: break;
184: }
185: }
186:
187: if (!found) {
188: return false;
189: }
190: }
191:
192: return locs2.size() == 0;
193: }
194:
195: /**
196: * Determines a depends clause for an invariant
197: * (helper for buildEncapsulationFormula).
198: */
199: private SetOfLocationDescriptor getDependsClauseForInv(
200: ClassInvariant inv) {
201: Term invTerm = null;
202:
203: try {
204: invTerm = translateInv(inv);
205: } catch (SLTranslationError e) {
206: e.printStackTrace();
207: }
208:
209: SetOfLocationDescriptor extractedClause = extractDependsClauseFromTerm(invTerm);
210: extractedClause = filterDependsClause(extractedClause);
211:
212: DependsClauseDialog dlg = new DependsClauseDialog(inv,
213: initConfig, extractedClause);
214: SetOfLocationDescriptor result = extractedClause;
215: if (dlg.wasSuccessful()) {
216: result = dlg.getDependsClause();
217:
218: if (!equalsModRenaming(result, extractedClause)) {
219: ProofOblInput dependsPO = new CorrectDependsPO(result,
220: inv);
221: dependsPOs = dependsPOs.prepend(dependsPO);
222: }
223: }
224:
225: return result;
226: }
227:
228: private Term createInstanceOf(ModelClass modelClass, Term term) {
229: Name name = new Name(modelClass.getFullClassName()
230: + "::instance");
231: Function instanceFunc = (Function) initConfig.funcNS().lookup(
232: name);
233: Term instanceTerm = tf.createFunctionTerm(instanceFunc, term);
234: Term trueLitTerm = services.getTypeConverter()
235: .convertToLogicElement(BooleanLiteral.TRUE);
236: return tf.createEqualityTerm(instanceTerm, trueLitTerm);
237: }
238:
239: /**
240: * Creates the proof obligation's main formula and saves it in a field.
241: */
242: private void buildEncapsulationFormula() throws ProofInputException {
243: if (encapsulationFormula != null) {
244: return;
245: }
246:
247: Sort javaLangObjectSort = javaInfo.getJavaLangObjectAsSort();
248: Function accPred = getAccPred();
249:
250: //get a depends clause
251: SetOfLocationDescriptor dependsClause = SetAsListOfLocationDescriptor.EMPTY_SET;
252: IteratorOfClassInvariant it = guardedInvs.iterator();
253: while (it.hasNext()) {
254: ClassInvariant inv = it.next();
255: dependsClause = dependsClause
256: .union(getDependsClauseForInv(inv));
257: }
258:
259: //create the formula
260: encapsulationFormula = tf.createJunctorTerm(Op.TRUE);
261: IteratorOfLocationDescriptor it2 = dependsClause.iterator();
262: while (it2.hasNext()) {
263: LocationDescriptor loc = it2.next();
264: Debug.assertTrue(loc instanceof BasicLocationDescriptor);
265: BasicLocationDescriptor bloc = (BasicLocationDescriptor) loc;
266:
267: if (bloc.getLocTerm().arity() == 0) {
268: continue;
269: }
270:
271: LogicVariable y = new LogicVariable(new Name("y"),
272: javaLangObjectSort);
273: Term yTerm = tf.createVariableTerm(y);
274: Term dTerm = bloc.getLocTerm().sub(0);
275: Term phiTerm = bloc.getFormula();
276:
277: //create "Acc(y, d_k') & phi_k"
278: Term accTerm = tf.createFunctionTerm(accPred, yTerm, dTerm);
279: Term premiseTerm = tf.createJunctorTermAndSimplify(Op.AND,
280: accTerm, phiTerm);
281:
282: //create disjunction of "C::Instance(y)" for all guards C
283: Term isGuardTerm = tf.createJunctorTerm(Op.FALSE);
284: IteratorOfModelClass it3 = guard.iterator();
285: while (it3.hasNext()) {
286: ModelClass guardClass = it3.next();
287: Term instanceOfTerm = createInstanceOf(guardClass,
288: yTerm);
289: isGuardTerm = tf.createJunctorTermAndSimplify(Op.OR,
290: isGuardTerm, instanceOfTerm);
291: }
292:
293: //create "phi_k & y = d_k'"
294: Term yEqualTerm = tf.createEqualityTerm(yTerm, dTerm);
295: Term isWithinTerm = tf.createJunctorTermAndSimplify(Op.AND,
296: phiTerm, yEqualTerm);
297:
298: //create implication
299: Term impTerm = tf.createJunctorTerm(Op.IMP, premiseTerm,
300: tf.createJunctorTerm(Op.OR, isWithinTerm,
301: isGuardTerm));
302:
303: //create quantification
304: Term quantifierTerm = CreatedAttributeTermFactory.INSTANCE
305: .createCreatedNotNullQuantifierTerm(services,
306: Op.ALL, new LogicVariable[] { y }, impTerm);
307: SetOfQuantifiableVariable freeVars = bloc.getLocTerm()
308: .freeVars();
309: quantifierTerm = (freeVars.size() == 0 ? quantifierTerm
310: : tf.createQuantifierTerm(Op.ALL, freeVars
311: .toArray(), quantifierTerm));
312:
313: encapsulationFormula = tf.createJunctorTermAndSimplify(
314: Op.AND, encapsulationFormula, quantifierTerm);
315: }
316: }
317:
318: /**
319: * Creates the term "ex x. Acc(x, v)".
320: */
321: private Term createAccessedTerm(ProgramVariable v,
322: Sort javaLangObjectSort, Function accPred) {
323: LogicVariable x = new LogicVariable(new Name("x"),
324: javaLangObjectSort);
325: Term accTerm = tf.createFunctionTerm(accPred, tf
326: .createVariableTerm(x), tf.createVariableTerm(v));
327: return tf.createQuantifierTerm(Op.EX, x, accTerm);
328: }
329:
330: protected Term getPreTerm(ProgramVariable selfVar,
331: ListOfProgramVariable paramVars, ProgramVariable resultVar,
332: ProgramVariable exceptionVar, Map atPreFunctions)
333: throws ProofInputException {
334: Term result = tf.createJunctorTerm(Op.TRUE);
335: Function accPred = getAccPred();
336: Sort javaLangObjectSort = javaInfo.getJavaLangObjectAsSort();
337:
338: //create and conjoin "ex x . Acc(x, p)" for all parameters p of an
339: //object sort
340: IteratorOfProgramVariable it = paramVars.iterator();
341: while (it.hasNext()) {
342: ProgramVariable paramVar = it.next();
343: Term paramAccTerm = createAccessedTerm(paramVar,
344: javaLangObjectSort, accPred);
345: result = tf.createJunctorTermAndSimplify(Op.AND, result,
346: paramAccTerm);
347: }
348:
349: //add "ex x . Acc(x, self)"
350: if (selfVar != null) {
351: Term selfAccTerm = createAccessedTerm(selfVar,
352: javaLangObjectSort, accPred);
353: result = tf.createJunctorTermAndSimplify(Op.AND, result,
354: selfAccTerm);
355: }
356:
357: //add main formula
358: buildEncapsulationFormula();
359: result = tf.createJunctorTermAndSimplify(Op.AND, result,
360: encapsulationFormula);
361:
362: return result;
363: }
364:
365: protected Term getPostTerm(ProgramVariable selfVar,
366: ListOfProgramVariable paramVars, ProgramVariable resultVar,
367: ProgramVariable exceptionVar, Map atPreFunctions)
368: throws ProofInputException {
369: Term result = tf.createJunctorTerm(Op.TRUE);
370: Function accPred = getAccPred();
371: Sort javaLangObjectSort = javaInfo.getJavaLangObjectAsSort();
372:
373: //create "ex x . Acc(x, result)"
374: if (resultVar != null) {
375: result = createAccessedTerm(resultVar, javaLangObjectSort,
376: accPred);
377: }
378:
379: //add main formula
380: buildEncapsulationFormula();
381: result = tf.createJunctorTermAndSimplify(Op.IMP, result,
382: encapsulationFormula);
383:
384: return result;
385: }
386:
387: //-------------------------------------------------------------------------
388: //methods of ProofOblInput interface
389: //-------------------------------------------------------------------------
390:
391: public void readProblem(ModStrategy mod) throws ProofInputException {
392: super .readProblem(mod);
393: setInitConfig(initConfig);
394:
395: Debug.assertTrue(poTerms.length == 1);
396: Debug.assertTrue(poNames == null);
397: Term poTerm = poTerms[0];
398:
399: int numPOs = 1 + dependsPOs.size();
400: poTerms = new Term[numPOs];
401: poNames = new String[numPOs];
402: poTerms[0] = poTerm;
403: poNames[0] = name();
404:
405: IteratorOfProofOblInput it = dependsPOs.iterator();
406: int i = 1;
407: while (it.hasNext()) {
408: CorrectDependsPO dependsPO = ((CorrectDependsPO) it.next());
409: dependsPO.readProblem(mod);
410: poTerms[i] = dependsPO.getTerm();
411: poNames[i] = dependsPO.name();
412: }
413: }
414:
415: public void setInitConfig(InitConfig conf) {
416: super .setInitConfig(conf);
417: IteratorOfProofOblInput it = dependsPOs.iterator();
418: while (it.hasNext()) {
419: it.next().setInitConfig(conf);
420: }
421: }
422: }
|