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.init;
019:
020: import java.util.*;
021:
022: import de.uka.ilkd.key.casetool.ModelClass;
023: import de.uka.ilkd.key.casetool.ModelMethod;
024: import de.uka.ilkd.key.casetool.UMLModelClass;
025: import de.uka.ilkd.key.java.JavaInfo;
026: import de.uka.ilkd.key.java.Services;
027: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
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.proof.OpReplacer;
032: import de.uka.ilkd.key.proof.Proof;
033: import de.uka.ilkd.key.proof.ProofAggregate;
034: import de.uka.ilkd.key.rule.SetOfTaclet;
035: import de.uka.ilkd.key.rule.UpdateSimplifier;
036: import de.uka.ilkd.key.speclang.*;
037:
038: /**
039: * An abstract proof obligation implementing common functionality.
040: */
041: public abstract class AbstractPO implements ProofOblInput {
042:
043: protected static final TermFactory tf = TermFactory.DEFAULT;
044: protected static final CreatedAttributeTermFactory createdFactory = CreatedAttributeTermFactory.INSTANCE;
045: protected static final TermBuilder tb = TermBuilder.DF;
046:
047: private final String name;
048: protected final ModelClass modelClass;
049:
050: protected InitConfig initConfig = null;
051: protected Services services = null;
052: protected JavaInfo javaInfo = null;
053:
054: private Map /*Operator -> Term*/axioms = new HashMap();
055: private String header = null;
056: private ProofAggregate proofAggregate = null;
057:
058: protected Term[] poTerms = null;
059: protected String[] poNames = null;
060: protected SetOfTaclet[] poTaclets = null;
061:
062: //-------------------------------------------------------------------------
063: //constructors
064: //-------------------------------------------------------------------------
065:
066: public AbstractPO(String name, ModelClass modelClass) {
067: this .name = name;
068: this .modelClass = modelClass;
069: }
070:
071: //-------------------------------------------------------------------------
072: //helper methods for subclasses
073: //-------------------------------------------------------------------------
074:
075: protected ProgramVariable buildSelfVarAsProgVar() {
076: String className = modelClass.getFullClassName();
077: KeYJavaType classType = javaInfo.getTypeByClassName(className);
078:
079: ProgramElementName classPEN = new ProgramElementName("self");
080:
081: return new LocationVariable(classPEN, classType);
082: }
083:
084: protected LogicVariable buildSelfVarAsLogicVar() {
085: String className = modelClass.getFullClassName();
086: KeYJavaType classType = javaInfo.getTypeByClassName(className);
087:
088: ProgramElementName classPEN = new ProgramElementName("self");
089: return new LogicVariable(classPEN, classType.getSort());
090: }
091:
092: protected ListOfProgramVariable buildParamVars(
093: ModelMethod modelMethod) {
094: int numPars = modelMethod.getNumParameters();
095: ListOfProgramVariable result = SLListOfProgramVariable.EMPTY_LIST;
096:
097: for (int i = 0; i < numPars; i++) {
098: KeYJavaType parType = javaInfo
099: .getTypeByClassName(modelMethod
100: .getParameterTypeAt(i));
101: assert parType != null;
102: ProgramElementName parPEN = new ProgramElementName(
103: modelMethod.getParameterNameAt(i));
104: result = result
105: .append(new LocationVariable(parPEN, parType));
106: }
107:
108: return result;
109: }
110:
111: protected ProgramVariable buildResultVar(ModelMethod modelMethod) {
112: ProgramVariable result = null;
113:
114: if (!modelMethod.isVoid()) {
115: KeYJavaType resultType = javaInfo
116: .getTypeByClassName(modelMethod.getResultType());
117: assert resultType != null;
118: ProgramElementName resultPEN = new ProgramElementName(
119: "result");
120: result = new LocationVariable(resultPEN, resultType);
121: }
122:
123: return result;
124: }
125:
126: protected ProgramVariable buildExcVar() {
127: KeYJavaType excType = javaInfo
128: .getTypeByClassName("java.lang.Throwable");
129: ProgramElementName excPEN = new ProgramElementName("exc");
130: return new LocationVariable(excPEN, excType);
131: }
132:
133: /**
134: * Translates a precondition out of an operation contract.
135: * @throws SLTranslationError
136: */
137: protected Term translatePre(OperationContract contract,
138: ParsableVariable selfVar, ListOfParsableVariable paramVars)
139: throws SLTranslationError {
140: FormulaWithAxioms fwa = contract.getPre(selfVar, paramVars,
141: services);
142: axioms.putAll(fwa.getAxioms());
143: return fwa.getFormula();
144: }
145:
146: /**
147: * Translates a postcondition out of an operation contract.
148: * @throws SLTranslationError
149: */
150: protected Term translatePost(OperationContract contract,
151: ParsableVariable selfVar, ListOfParsableVariable paramVars,
152: ParsableVariable resultVar, ParsableVariable excVar)
153: throws SLTranslationError {
154: FormulaWithAxioms fwa = contract.getPost(selfVar, paramVars,
155: resultVar, excVar, services);
156: axioms.putAll(fwa.getAxioms());
157: return fwa.getFormula();
158: }
159:
160: /**
161: * Translates a modifies clause out of an operation contract.
162: */
163: protected Term translateModifies(OperationContract contract,
164: Term targetTerm, ParsableVariable selfVar,
165: ListOfParsableVariable paramVars) throws SLTranslationError {
166: final SetOfLocationDescriptor locations = contract.getModifies(
167: selfVar, paramVars, services);
168:
169: final UpdateFactory uf = new UpdateFactory(services,
170: new UpdateSimplifier());
171: final AnonymisingUpdateFactory auf = new AnonymisingUpdateFactory(
172: uf);
173: return auf.createAnonymisingUpdateTerm(locations, targetTerm,
174: services);
175: }
176:
177: /**
178: * Translates a class invariant.
179: * @throws SLTranslationError
180: */
181: protected Term translateInv(ClassInvariant inv)
182: throws SLTranslationError {
183: final FormulaWithAxioms fwa = inv.getInv(services);
184: axioms.putAll(fwa.getAxioms());
185: return fwa.getFormula();
186: }
187:
188: /**
189: * Translates a list of class invariants.
190: * @throws SLTranslationError
191: */
192: protected Term translateInvs(ListOfClassInvariant invs)
193: throws SLTranslationError {
194: Term result = tb.tt();
195:
196: IteratorOfClassInvariant it = invs.iterator();
197: while (it.hasNext()) {
198: result = tb.and(result, translateInv(it.next()));
199: }
200:
201: return result;
202: }
203:
204: /**
205: * Translates a class invariant as an open formula.
206: * @throws SLTranslationError
207: */
208: protected Term translateInvOpen(ClassInvariant inv,
209: ParsableVariable selfVar) throws SLTranslationError {
210: FormulaWithAxioms fwa = inv.getOpenInv(selfVar, services);
211: axioms.putAll(fwa.getAxioms());
212: return fwa.getFormula();
213: }
214:
215: protected Term translateInvsOpen(ListOfClassInvariant invs,
216: ParsableVariable selfVar) throws SLTranslationError {
217: Term result = tb.tt();
218:
219: IteratorOfClassInvariant it = invs.iterator();
220: while (it.hasNext()) {
221: result = tb.and(result,
222: translateInvOpen(it.next(), selfVar));
223: }
224:
225: return result;
226: }
227:
228: protected ListOfParsableVariable toPV(ListOfProgramVariable vars) {
229: ListOfParsableVariable result = SLListOfParsableVariable.EMPTY_LIST;
230: final IteratorOfProgramVariable it = vars.iterator();
231: while (it.hasNext()) {
232: result = result.append(it.next());
233: }
234: return result;
235: }
236:
237: /**
238: * Replaces operators in a term by other operators with the same signature.
239: */
240: protected Term replaceOps(Map /*Operator -> Operator*/map,
241: Term term) {
242: return new OpReplacer(map).replace(term);
243: }
244:
245: /**
246: * Creates atPre-functions for all relevant operators in the passed term.
247: */
248: public static void createAtPreFunctionsForTerm(Term term,
249: /*inout*/Map /*Operator -> Function*/atPreFunctions) {
250: int arity = term.arity();
251: Sort[] subSorts = new Sort[arity];
252: for (int i = 0; i < arity; i++) {
253: Term subTerm = term.sub(i);
254: createAtPreFunctionsForTerm(subTerm, atPreFunctions);
255: subSorts[i] = subTerm.sort();
256: }
257:
258: if (term.op() instanceof AccessOp
259: || term.op() instanceof ProgramVariable
260: || term.op() instanceof ProgramMethod) {
261: Function atPreFunc = (Function) (atPreFunctions.get(term
262: .op()));
263: if (atPreFunc == null) {
264: String atPreName = term.op().name().toString() + "@pre";
265: if (atPreName.startsWith(".")) {
266: atPreName = atPreName.substring(1);
267: }
268: atPreFunc = new RigidFunction(new Name(atPreName), term
269: .sort(), subSorts);
270: atPreFunctions.put(term.op(), atPreFunc);
271: }
272: }
273: }
274:
275: /**
276: * Helper for buildAtPreDefinitions().
277: */
278: private static Term[] getTerms(ArrayOfQuantifiableVariable vars) {
279: int numVars = vars.size();
280: Term[] result = new Term[numVars];
281:
282: for (int i = 0; i < numVars; i++) {
283: LogicVariable var = (LogicVariable) (vars
284: .getQuantifiableVariable(i));
285: result[i] = tb.var(var);
286: }
287:
288: return result;
289: }
290:
291: /**
292: * Creates the necessary definitions for the passed @pre-functions.
293: */
294: public static Term buildAtPreDefinitions(
295: /*in*/Map /*Operator -> Function */atPreFunctions) {
296: Term result = tb.tt();
297:
298: Iterator it = atPreFunctions.entrySet().iterator();
299: while (it.hasNext()) {
300: Map.Entry entry = (Map.Entry) (it.next());
301: Operator f1 = (Operator) (entry.getKey());
302: Function f2 = (Function) (entry.getValue());
303:
304: int arity = f1.arity();
305: assert arity == f2.arity();
306: LogicVariable[] args = new LogicVariable[arity];
307: for (int i = 0; i < arity; i++) {
308: args[i] = new LogicVariable(new Name("x" + i), f2
309: .argSort(i));
310: }
311:
312: Term[] argTerms = getTerms(new ArrayOfQuantifiableVariable(
313: args));
314:
315: Term f1Term = tf.createTerm(f1, argTerms,
316: (ArrayOfQuantifiableVariable) null, null);
317: Term f2Term = tb.func(f2, argTerms);
318: Term equalsTerm = tf.createJunctorTerm(Op.EQUALS, f1Term,
319: f2Term);
320: Term quantifTerm;
321: if (arity > 0) {
322: quantifTerm = tb.all(args, equalsTerm);
323: } else {
324: quantifTerm = equalsTerm;
325: }
326: result = tb.and(result, quantifTerm);
327: }
328:
329: return result;
330: }
331:
332: protected void registerInNamespaces(ProgramVariable pv) {
333: if (pv != null) {
334: initConfig.progVarNS().add(pv);
335: }
336: }
337:
338: protected void registerInNamespaces(ListOfProgramVariable pvs) {
339: final IteratorOfProgramVariable it = pvs.iterator();
340: while (it.hasNext()) {
341: initConfig.progVarNS().add(it.next());
342: }
343: }
344:
345: protected void registerInNamespaces(/*in*/Map atPreFunctions) {
346: final Iterator it = atPreFunctions.values().iterator();
347: while (it.hasNext()) {
348: initConfig.funcNS().add((Function) it.next());
349: }
350: }
351:
352: //-------------------------------------------------------------------------
353: //methods of ProofOblInput interface
354: //-------------------------------------------------------------------------
355:
356: public String name() {
357: return name;
358: }
359:
360: public boolean askUserForEnvironment() {
361: return false;
362: }
363:
364: public void setInitConfig(InitConfig initConfig) {
365: this .initConfig = initConfig;
366: this .services = initConfig.getServices();
367: this .javaInfo = initConfig.getServices().getJavaInfo();
368: }
369:
370: public void readActivatedChoices() throws ProofInputException {
371: initConfig.setActivatedChoices(SetAsListOfChoice.EMPTY_SET);
372: }
373:
374: /**
375: * Computes the method specifications and stores the results in the
376: * SpecificationRepository which belongs to the ProofEnvironment of InitCfg.
377: */
378: public void readSpecs() {
379: // specifications from model
380: Vector reprMethods = null;
381: Iterator reprMethodsIter = null;
382: UMLModelClass reprClass = null;
383: Set allClasses = modelClass.getAllClasses();
384: Iterator allClassesIter = allClasses.iterator();
385: while (allClassesIter.hasNext()) {
386: reprClass = (UMLModelClass) allClassesIter.next();
387: reprMethods = reprClass.getOps();
388: reprMethodsIter = reprMethods.iterator();
389: while (reprMethodsIter.hasNext()) {
390: ListOfOperationContract l = ((ModelMethod) reprMethodsIter
391: .next()).getMyOperationContracts();
392: IteratorOfOperationContract it = l.iterator();
393: /*TODO
394: while (it.hasNext()) {
395: initConfig.getProofEnv().addMethodContract(it.next());
396: }*/
397: }
398: }
399: }
400:
401: /**
402: * Creates declarations necessary to save/load proof in textual form
403: * (helper for createProof()).
404: */
405: private String createProofHeader(String javaPath) {
406: if (header != null) {
407: return header;
408: }
409:
410: String s;
411: s = "\\javaSource \"" + javaPath + "\";\n\n";
412:
413: IteratorOfNamed it;
414:
415: /* program sorts need not be declared and
416: * there are no user-defined sorts with this kind of PO (yes?)
417: s += "sorts {\n"; // create declaration header for the proof
418: it = initConfig.sortNS().getProtocolled();
419: while (it.hasNext()) {
420: String n=it.next().toString();
421: int i;
422: if ((i=n.indexOf("."))<0 ||
423: initConfig.sortNS().lookup(new Name(n.substring(0,i)))==null) {
424: //the line above is for inner classes.
425: //KeY does not want to handle them anyway...
426: s = s+"object "+n+";\n";
427: }
428: }
429: s+="}
430: */
431: s += "\n\n\\programVariables {\n";
432: it = initConfig.progVarNS().allElements().iterator();
433: while (it.hasNext())
434: s = s + ((ProgramVariable) (it.next())).proofToString();
435:
436: s += "}\n\n\\functions {\n";
437: it = initConfig.funcNS().allElements().iterator();
438: while (it.hasNext()) {
439: Function f = (Function) it.next();
440: // only declare @pre-functions, others will be generated automat.
441: if (f.name().toString().indexOf("@pre") != -1) {
442: s += f.proofToString();
443: }
444: }
445:
446: s += "}\n\n";
447:
448: header = s;
449: return s;
450: }
451:
452: /**
453: * Creates a Proof (helper for getPO()).
454: */
455: private Proof createProof(String name, Term poTerm) {
456: if (header == null) {
457: header = createProofHeader(modelClass.getRootDirectory());
458: }
459: return new Proof(name, poTerm, header, initConfig
460: .createTacletIndex(), initConfig
461: .createBuiltInRuleIndex(), initConfig.getServices());
462: }
463:
464: /**
465: * Returns those axioms from the SLDL-Translation which are required for
466: * the passed term (helper for getPO()).
467: */
468: private Term getRequiredAxioms(Term t) {
469: Term result = tb.tt();
470:
471: Set axiomSet = getRequiredAxiomsAsSet(t);
472:
473: Iterator it = axiomSet.iterator();
474: while (it.hasNext()) {
475: result = tb.and(result, (Term) it.next());
476: }
477: /*
478: if(axioms.containsKey(t.op())) {
479: result = tb.and(result, (Term)axioms.get(t.op()));
480: }
481:
482: for(int i = 0; i < t.arity(); i++) {
483: result = tb.and(result, getRequiredAxioms(t.sub(i)));
484: }
485: */
486: return result;
487: }
488:
489: /**
490: * Returns those axioms from the SLDL-Translation which are required for
491: * the passed term (helper for getRequiredAxioms(Term t)).
492: */
493: private Set getRequiredAxiomsAsSet(Term t) {
494: Set result = new HashSet();
495:
496: if (axioms.containsKey(t.op())) {
497: result.add(axioms.get(t.op()));
498: }
499:
500: for (int i = 0; i < t.arity(); i++) {
501: result.addAll(getRequiredAxiomsAsSet(t.sub(i)));
502: }
503:
504: return result;
505: }
506:
507: public ProofAggregate getPO() {
508: if (proofAggregate != null) {
509: return proofAggregate;
510: }
511:
512: if (poTerms == null) {
513: throw new IllegalStateException(
514: "No proof obligation terms.");
515: }
516:
517: Proof[] proofs = new Proof[poTerms.length];
518: for (int i = 0; i < proofs.length; i++) {
519: proofs[i] = createProof(
520: poNames != null ? poNames[i] : name, tb.imp(
521: getRequiredAxioms(poTerms[i]), poTerms[i]));
522:
523: if (poTaclets != null) {
524: proofs[i].getGoal(proofs[i].root()).indexOfTaclets()
525: .addTaclets(poTaclets[i]);
526: }
527: }
528:
529: return proofAggregate = ProofAggregate.createProofAggregate(
530: proofs, name);
531: }
532: }
|