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.proof.mgt;
019:
020: import java.util.*;
021:
022: import de.uka.ilkd.key.casetool.ModelMethod;
023: import de.uka.ilkd.key.java.*;
024: import de.uka.ilkd.key.java.abstraction.ArrayType;
025: import de.uka.ilkd.key.java.abstraction.Type;
026: import de.uka.ilkd.key.java.statement.Catch;
027: import de.uka.ilkd.key.java.statement.CatchAllStatement;
028: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
029: import de.uka.ilkd.key.logic.*;
030: import de.uka.ilkd.key.logic.op.*;
031: import de.uka.ilkd.key.logic.sort.Sort;
032: import de.uka.ilkd.key.logic.sort.AbstractSort;
033: import de.uka.ilkd.key.pp.LogicPrinter;
034: import de.uka.ilkd.key.proof.Proof;
035: import de.uka.ilkd.key.proof.ProofSaver;
036: import de.uka.ilkd.key.proof.VariableNameProposer;
037: import de.uka.ilkd.key.proof.init.ProofOblInput;
038: import de.uka.ilkd.key.util.Debug;
039:
040: /**
041: * represents a contract on the DynamicLogic level, that is pre-condition,
042: * program, post-condition, and modifies clause. It is the starting point to
043: * create both proof obligation (to ensure that the contract is valid) as well
044: * as a taclet (that allows to use the contract in a proof). DLMethodContracts
045: * are created from UserKeYProblemFiles using the \contract section. Moreover
046: * they are created when a contract of another input like JML or OCL is
047: * configured.
048: * @deprecated
049: *
050: */
051: public class DLMethodContract extends DefaultOperationContract {
052:
053: private Term pre;
054: private Term atPreAxioms;
055: private Collection atPreFunctions;
056: private Modality modality;
057: private ModelMethod modelMethod;
058: private Statement stmt;
059: private Term post;
060: private SetOfLocationDescriptor modifies;
061: private NamespaceSet namespaces;
062: private String displayName;
063: private String name;
064: private Services services;
065:
066: private static Statement extractStatement(Term fma) {
067: JavaProgramElement pe = fma.javaBlock().program();
068: return (Statement) ((NonTerminalProgramElement) pe)
069: .getChildAt(0);
070: }
071:
072: static Statement unwrapBlocks(Statement s, boolean stopAtCatchAll) {
073: while (s instanceof StatementBlock
074: || (s instanceof CatchAllStatement && !stopAtCatchAll)
075: || s instanceof Catch) {
076: s = ((StatementContainer) s).getStatementAt(0);
077: }
078: return s;
079: }
080:
081: /**
082: * Creates a DLMethodContract with one implication formula of the form
083: * <code>pre -> \<p\> post</code> and a modifies clause
084: *
085: * @param fma
086: * the implication formula
087: * @param modifies
088: * a set of location descriptors defining the modifies clause for
089: * this DLMethodContract
090: * @param name
091: * a unique identifying name for a contract in the proof
092: * @param displayName
093: * the name displayed for this contract
094: * @param services
095: * the services object
096: * @param namespaces
097: * the namespaces for looking up atpre functions
098: */
099: public DLMethodContract(Term fma, SetOfLocationDescriptor modifies,
100: String name, String displayName, Services services,
101: NamespaceSet namespaces) {
102:
103: this (fma.sub(0), fma.sub(1).sub(0), null, null,
104: extractStatement(fma.sub(1)), modifies, (Modality) fma
105: .sub(1).op(), name, displayName, services,
106: namespaces.copy());
107:
108: setupAtPreFunctions(fma, namespaces);
109: }
110:
111: /**
112: * Creates a DLMethodContract with separate parts and possible additional
113: * preconditions which are not to be proven in the precondition branch of
114: * the created proof.
115: *
116: * @param pre
117: * the precondition of the contract
118: * @param post
119: * the postcondition of the contract
120: * @param extraPre
121: * the additional preconditions
122: * @param atPreFunctions
123: * a Collection with all functions used to model <tt>@pre</tt> for function symbols
124: * @param mbs
125: * the statement of the proof, either this is a method body
126: * statement or a catch all statement
127: * @param modifies
128: * a set of location descriptors defining the modifies clause for
129: * this DLMethodContract
130: * @param name
131: * a unique identifying name for a contract in the proof
132: * @param displayName
133: * the name displayed for this contract
134: * @param services
135: * the services object
136: * @param namespaces
137: * the namespaces for looking up atpre functions
138: */
139: public DLMethodContract(Term pre, Term post, Term extraPre,
140: Collection atPreFunctions, Statement mbs,
141: SetOfLocationDescriptor modifies, Modality modality,
142: String name, String displayName, Services services,
143: NamespaceSet namespaces) {
144:
145: assert pre != null && post != null;
146:
147: this .pre = pre;
148: this .post = post;
149: this .atPreAxioms = extraPre;
150: this .atPreFunctions = atPreFunctions == null ? new HashSet()
151: : atPreFunctions;
152: this .stmt = mbs;
153: this .modifies = modifies;
154: this .modality = modality;
155: this .name = name;
156: this .displayName = displayName;
157: this .services = services;
158: this .namespaces = namespaces;
159: this .modelMethod = new JavaModelMethod(getProgramMethod(),
160: services.getJavaInfo().getJavaSourcePath(), services);
161: }
162:
163: /**
164: * @param namespaces
165: * @param map
166: */
167: private void addAtPreFunctions(Namespace namespace, Map map) {
168: if (namespace instanceof AtPreNamespace) {
169: final Map atPreMapping = ((AtPreNamespace) namespace)
170: .getAtPreMapping();
171: map.putAll(atPreMapping);
172: atPreFunctions.addAll(atPreMapping.values());
173: }
174: }
175:
176: public void addPost(Term t) {
177: post = TermBuilder.DF.and(t, post);
178: }
179:
180: public void addPre(Term t) {
181: pre = TermBuilder.DF.and(t, pre);
182: }
183:
184: public boolean applicableForModality(Modality mod) {
185: return getModality().equals(
186: ModalityClass.getNormReprModality(mod));
187: }
188:
189: private ProgramVariable clone(ProgramVariable pv, Services services) {
190: final ProgramElementName name = services.getVariableNamer()
191: .getTemporaryNameProposal(pv.name().toString());
192: return new LocationVariable(name, pv.getKeYJavaType());
193: }
194:
195: private RigidFunction clone(RigidFunction rf) {
196: String basename = rf.name().toString().replaceAll("@pre",
197: "AtPre");
198: final String name = VariableNameProposer.DEFAULT
199: .getNameProposal(basename, services, null);
200: return new RigidFunction(new Name(name), rf.sort(), rf
201: .argSort());
202: }
203:
204: public DLMethodContract copy() {
205: return new DLMethodContract(pre, post, atPreAxioms,
206: getAtPreFunctions(), stmt, modifies, modality, name,
207: displayName, services, namespaces);
208: }
209:
210: public DLMethodContract createDLMethodContract(Proof proof) {
211: final DLMethodContract c = copy();
212: c.displayName = c.displayName + " (derived)";
213: return c;
214: }
215:
216: private Term createImplication() {
217: final TermBuilder tb = TermBuilder.DF;
218: final Term modalityTerm = tb.tf().createProgramTerm(
219: modality,
220: JavaBlock.createJavaBlock(new StatementBlock(
221: getStatement())), getPost());
222: return tb.imp(tb.and(getAdditionalAxioms(), getPre()),
223: modalityTerm);
224: }
225:
226: public String createProgramVarsSection() {
227: final IteratorOfNamed it = namespaces.programVariables()
228: .allElements().iterator();
229: String result = "\n\n\\programVariables {\n";
230: while (it.hasNext()) {
231: ProgramVariable pv = (ProgramVariable) it.next();
232: final Type javaType = pv.getKeYJavaType().getJavaType();
233:
234: final String typeName = javaType instanceof ArrayType ? ((ArrayType) javaType)
235: .getAlternativeNameRepresentation()
236: : javaType.getFullName();
237:
238: result += " " + typeName + " " + pv.name() + ";\n";
239: }
240: result += "}\n";
241: return result;
242: }
243:
244: public boolean equals(Object cmp) {
245: if (!(cmp instanceof OldOperationContract)) {
246: return false;
247: }
248: if (!(cmp instanceof DLMethodContract)) {
249: return cmp.equals(this );
250: }
251: DLMethodContract cmpHoare = (DLMethodContract) cmp;
252: // TODO: This does not work if functions for @pre are introduced
253: boolean b = cmpHoare.modelMethod.equals(modelMethod)
254: && cmpHoare.atPreAxioms.equalsModRenaming(atPreAxioms)
255: && cmpHoare.post.equalsModRenaming(post)
256: && cmpHoare.pre.equalsModRenaming(pre)
257: && cmpHoare.modality.equals(modality);
258: if (!b || cmpHoare.modifies.size() != modifies.size())
259: return false;
260: return modifies.equals(cmpHoare.modifies);
261: }
262:
263: protected Term getAdditionalAxioms() {
264: return atPreAxioms;
265: }
266:
267: private Collection getAtPreFunctions() {
268: return atPreFunctions;
269: }
270:
271: public CatchAllStatement getCatchAllStatement() {
272: Statement s = unwrapBlocks(getStatement(), true);
273: return (s instanceof CatchAllStatement) ? (CatchAllStatement) s
274: : null;
275: }
276:
277: public String getHTMLText() {
278: return "<html>pre: "
279: + getPreText()
280: + "<br>post: "
281: + getPostText()
282: + "<br>modifies: "
283: + getModifiesText()
284: + "<br>termination: "
285: + (getModality() == Op.DIA ? "total" : getModality()
286: .toString()) + "</html>";
287: }
288:
289: public MethodBodyStatement getMethodBodyStatement() {
290: return (MethodBodyStatement) unwrapBlocks(getStatement(), false);
291: }
292:
293: public Modality getModality() {
294: return ModalityClass.getNormReprModality(modality);
295: }
296:
297: public ModelMethod getModelMethod() {
298: return modelMethod;
299: }
300:
301: public SetOfLocationDescriptor getModifies() {
302: return modifies;
303: }
304:
305: public String getModifiesText() {
306: return LogicPrinter.quickPrintLocationDescriptors(
307: getModifies(), services);
308: }
309:
310: public String getName() {
311: return name;
312: }
313:
314: /**
315: * returns the object on which this contract is, in this case it is the
316: * program statement of the contract; or in case that this is a method body
317: * statement the according program method is returned.
318: */
319: public Object getObjectOfContract() {
320: return getProgramMethod();
321: }
322:
323: public Term getPost() {
324: return post;
325: }
326:
327: public String getPostText() {
328: return ProofSaver.printTerm(getPost(), services).toString();
329: }
330:
331: public Term getPre() {
332: return pre;
333: }
334:
335: public String getPreText() {
336: return ProofSaver.printTerm(getPre(), services).toString();
337: }
338:
339: public ProgramMethod getProgramMethod() {
340: Object o = unwrapBlocks(getStatement(), false);
341: if (o instanceof MethodBodyStatement) {
342: return ((MethodBodyStatement) o).getProgramMethod(services);
343: }
344: Debug.fail();
345: return null;
346: }
347:
348: /**
349: * returns a proof obligation input needed to show the corretcness of this
350: * contract.
351: *
352: */
353: public ProofOblInput getProofOblInput(Proof proof) {
354: return new DLHoareTriplePO(createImplication(), getModality(),
355: header, getName(), services, this );
356: }
357:
358: public Statement getStatement() {
359: return stmt;
360: }
361:
362: public int hashCode() {
363: int result = 0;
364: result = 37 * result + modelMethod.hashCode();
365: result = 37 * result + modality.hashCode();
366: result = 37 * result + atPreAxioms.hashCode();
367: result = 37 * result + post.hashCode();
368: result = 37 * result + pre.hashCode();
369: result = 37 * result + modifies.hashCode();
370: return result;
371: }
372:
373: /**
374: * @param replacementMap
375: * @param localFunctions
376: * @param localProgramVariables
377: */
378: protected void instantiateAtPreSymbols(Map replacementMap,
379: Namespace localFunctions, Namespace localProgramVariables) {
380: final Iterator it = getAtPreFunctions().iterator();
381: while (it.hasNext()) {
382: final RigidFunction rf = (RigidFunction) it.next();
383: final RigidFunction newRf = clone(rf);
384: localFunctions.addSafely(newRf);
385: replacementMap.put(rf, newRf);
386: }
387: }
388:
389: protected void instantiateAuxiliarySymbols(Map replacementMap,
390: Namespace localFunctions, Namespace localProgramVariables,
391: Services services) {
392: instantiateDLContractPV(replacementMap, localProgramVariables);
393: }
394:
395: private void instantiateDLContractPV(Map replacementMap,
396: Namespace programVariables) {
397: final IteratorOfNamed it = namespaces.programVariables()
398: .elements().iterator();
399: while (it.hasNext()) {
400: final ProgramVariable pv = (ProgramVariable) it.next();
401: assert !pv.isMember();
402: if (!replacementMap.containsKey(pv)) {
403: final ProgramVariable newPV = clone(pv, services);
404: programVariables.addSafely(newPV);
405: replacementMap.put(pv, newPV);
406: }
407: }
408: }
409:
410: /**
411: * @param insts
412: * @param replacementMap
413: * @param localProgramVariables
414: * @param localFunctions
415: */
416: protected void instantiateMethodParameters(
417: MethodContractInstantiation insts,
418: final Map replacementMap, Namespace localFunctions,
419: Namespace localProgramVariables) {
420: for (int i = 0, methodParameterSize = insts.getArgumentCount(); i < methodParameterSize; i++) {
421: replacementMap.put(getMethodBodyStatement().getArguments()
422: .getExpression(i), insts.getArgumentAt(i));
423: }
424: }
425:
426: /**
427: * @param insts
428: * @param replacementMap
429: * @param localProgramVariables
430: * @param localFunctions
431: */
432: protected void instantiateMethodReceiver(
433: MethodContractInstantiation insts,
434: final Map replacementMap, Namespace localFunctions,
435: Namespace localProgramVariables) {
436: if (!getMethodBodyStatement().isStatic(services)) {
437: // this can be a field reference for instance
438: Term rec = services.getTypeConverter()
439: .convertToLogicElement(insts.getReceiver());
440: Sort recSort = rec.sort();
441: MethodBodyStatement mbs = null;
442: if (stmt instanceof CatchAllStatement) {
443: mbs = (MethodBodyStatement) ((StatementBlock) ((CatchAllStatement) stmt)
444: .getBody()).getBody().getStatement(0);
445: } else {
446: mbs = (MethodBodyStatement) stmt;
447: }
448: Sort actSort = mbs.getBodySource().getSort();
449: if (!recSort.equals(actSort)) {
450: rec = TermFactory.DEFAULT.createFunctionTerm(
451: ((AbstractSort) actSort).getCastSymbol(), rec);
452: }
453: replacementMap.put(getMethodBodyStatement()
454: .getDesignatedContext(), rec);
455: }
456: }
457:
458: /**
459: * @param insts
460: * @param replacementMap
461: * @param localProgramVariables
462: * @param localFunctions
463: */
464: protected void instantiateMethodReturnVariable(
465: MethodContractInstantiation insts,
466: final Map replacementMap, Namespace localFunctions,
467: Namespace localProgramVariables) {
468: replacementMap.put(
469: getMethodBodyStatement().getResultVariable(), insts
470: .getResult());
471: }
472:
473: public void setHeader(String s) {
474: if (s == null)
475: return;
476: // 1. Check if there is a \programVariables section (I can
477: // imagine an unlikely situation where it's actually missing),
478: // if so, replace it with a "fresh" one
479: int start = s.indexOf("\\programVariables");
480: int end = -1;
481: if (start != -1) {
482: end = s.indexOf("}", start);
483: header = s.substring(0, start) + createProgramVarsSection()
484: + s.substring(end + 1);
485: } else {
486: // 2. No? Then put it somewhere "on top"
487: start = s.indexOf("\\withOptions");
488: if (start != -1) {
489: // Put it after \withOptions
490: start = s.indexOf(";", start) + 1;
491: } else {
492: // Put it after \javaSource
493: start = s.indexOf("\\javaSource");
494: if (start != -1) {
495: start = s.indexOf(";", start) + 1;
496: } else {
497: Debug
498: .fail("Your .key file is missing vital sections as far as this situation is concerned.");
499: }
500: }
501: header = s.substring(0, start) + createProgramVarsSection()
502: + s.substring(start + 1);
503: }
504: }
505:
506: public String getHeader() {
507: return header;
508: }
509:
510: private void setupAtPreFunctions(Term fma, NamespaceSet namespaces) {
511: final TermBuilder tb = TermBuilder.DF;
512: final Map map = new TreeMap(new NameComparator());
513: atPreFunctions = new HashSet();
514:
515: addAtPreFunctions(namespaces.programVariables(), map);
516: addAtPreFunctions(namespaces.functions(), map);
517:
518: Term conj = tb.tt();
519:
520: final Iterator it = map.entrySet().iterator();
521:
522: while (it.hasNext()) {
523: Map.Entry e = (Map.Entry) it.next();
524: TermSymbol atPost = (TermSymbol) e.getKey();
525: Function atPre = (Function) e.getValue();
526: LogicVariable[] vars = new LogicVariable[atPost.arity()];
527:
528: if (atPost instanceof ProgramVariable
529: && ((ProgramVariable) atPost).isMember()
530: && !((ProgramVariable) atPost).isStatic()) {
531: vars = new LogicVariable[] { new LogicVariable(
532: new Name("x"), atPre.argSort(0)) };
533: } else {
534: for (int i = 0; i < vars.length; i++) {
535: vars[i] = new LogicVariable(new Name("x" + i),
536: ((Function) atPost).argSort(i));
537: }
538: }
539:
540: final Term[] varTerms = new Term[vars.length];
541: for (int i = 0; i < vars.length; i++) {
542: varTerms[i] = tb.var(vars[i]);
543: }
544:
545: final Term atPostTerm;
546: if ((atPost instanceof ProgramVariable)
547: && ((ProgramVariable) atPost).isMember()
548: && !((ProgramVariable) atPost).isStatic()) {
549: atPostTerm = tb.dot(varTerms[0],
550: (ProgramVariable) atPost);
551: } else {
552: atPostTerm = tb.func(atPost, varTerms);
553: }
554:
555: final Term atPreTerm = tb.func(atPre, varTerms);
556: conj = tb.and(conj, tb.all(vars, tb.equals(atPreTerm,
557: atPostTerm)));
558: }
559:
560: atPreAxioms = conj;
561:
562: }
563:
564: public Namespace getProgramVariables() {
565: return namespaces.programVariables();
566: }
567:
568: public String toString() {
569: return "[DL Hoare Triple Contract] " + getName();
570: }
571:
572: private class NameComparator implements Comparator {
573: public int compare(Object o1, Object o2) {
574: return ((Named) o1).name().compareTo(((Named) o2).name());
575: }
576: }
577:
578: }
|