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: //
010:
011: package de.uka.ilkd.key.proof.init;
012:
013: import java.util.HashMap;
014: import java.util.Iterator;
015: import java.util.Map;
016: import java.util.Set;
017:
018: import de.uka.ilkd.key.casetool.ModelClass;
019: import de.uka.ilkd.key.casetool.ModelMethod;
020: import de.uka.ilkd.key.java.ArrayOfExpression;
021: import de.uka.ilkd.key.java.Statement;
022: import de.uka.ilkd.key.java.StatementBlock;
023: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
024: import de.uka.ilkd.key.java.declaration.Modifier;
025: import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
026: import de.uka.ilkd.key.java.declaration.VariableSpecification;
027: import de.uka.ilkd.key.java.expression.literal.NullLiteral;
028: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
029: import de.uka.ilkd.key.java.expression.operator.New;
030: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
031: import de.uka.ilkd.key.java.reference.TypeReference;
032: import de.uka.ilkd.key.java.statement.Branch;
033: import de.uka.ilkd.key.java.statement.Catch;
034: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
035: import de.uka.ilkd.key.java.statement.Try;
036: import de.uka.ilkd.key.logic.*;
037: import de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT;
038: import de.uka.ilkd.key.logic.ldt.LDT;
039: import de.uka.ilkd.key.logic.op.*;
040: import de.uka.ilkd.key.logic.sort.ObjectSort;
041: import de.uka.ilkd.key.proof.mgt.AxiomJustification;
042: import de.uka.ilkd.key.proof.mgt.Contract;
043: import de.uka.ilkd.key.proof.mgt.Contractable;
044: import de.uka.ilkd.key.proof.mgt.OldOperationContract;
045: import de.uka.ilkd.key.rule.*;
046: import de.uka.ilkd.key.speclang.*;
047: import de.uka.ilkd.key.util.Debug;
048:
049: /**
050: * The "Ensures" proof obligation.
051: */
052: public abstract class EnsuresPO extends AbstractPO {
053:
054: public final ModelMethod modelMethod;
055: public final Modality modality;
056: private final InvariantSelectionStrategy invStrategy;
057: private final boolean skipPreconditions;
058:
059: private SetOfTaclet invTaclets = SetAsListOfTaclet.EMPTY_SET;
060:
061: //-------------------------------------------------------------------------
062: //constructors
063: //-------------------------------------------------------------------------
064:
065: public EnsuresPO(String name, ModelMethod modelMethod,
066: Modality modality, InvariantSelectionStrategy invStrategy,
067: boolean skipPreconditions) {
068: super (name + " of " + modelMethod, modelMethod
069: .getContainingClass());
070: this .modelMethod = modelMethod;
071: this .modality = modality;
072: this .invStrategy = invStrategy;
073: this .skipPreconditions = skipPreconditions;
074: }
075:
076: //-------------------------------------------------------------------------
077: //template methods to be implemented by subclasses
078: //-------------------------------------------------------------------------
079:
080: protected abstract Term getPreTerm(ProgramVariable selfVar,
081: ListOfProgramVariable paramVars, ProgramVariable resultVar,
082: ProgramVariable exceptionVar, Map atPreFunctions)
083: throws ProofInputException, SLTranslationError;
084:
085: protected abstract Term getPostTerm(ProgramVariable selfVar,
086: ListOfProgramVariable paramVars, ProgramVariable resultVar,
087: ProgramVariable exceptionVar, Map atPreFunctions)
088: throws ProofInputException, SLTranslationError;
089:
090: //-------------------------------------------------------------------------
091: //local helper methods
092: //-------------------------------------------------------------------------
093:
094: /**
095: * Returns the program method associated with this proof obligation.
096: */
097: private ProgramMethod getProgramMethod(
098: ListOfProgramVariable paramVars) {
099: //get class type
100: String className = modelClass.getFullClassName();
101: KeYJavaType classType = javaInfo.getTypeByClassName(className);
102: Debug.assertTrue(classType != null);
103:
104: //get program method
105: return javaInfo.getProgramMethod(classType, modelMethod
106: .getName(), paramVars.toArray(), classType);
107: }
108:
109: /**
110: * (helper for buildAssumedInvs())
111: * @throws SLTranslationError
112: * @throws ProofInputException
113: */
114: private Term buildInvariantsForClass(ModelClass modelClass)
115: throws SLTranslationError {
116: String className = modelClass.getFullClassName();
117: KeYJavaType classType = javaInfo.getTypeByClassName(className);
118:
119: //add "C.<classErroneous> = FALSE"
120: ProgramVariable erroneousField = javaInfo.getAttribute(
121: ImplicitFieldAdder.IMPLICIT_CLASS_ERRONEOUS, classType);
122: Term result = tb.equals(tb.var(erroneousField), tb
123: .FALSE(services));
124:
125: //add "C.<classInitialisationInProgress> = FALSE"
126: ProgramVariable initField = javaInfo.getAttribute(
127: ImplicitFieldAdder.IMPLICIT_CLASS_INIT_IN_PROGRESS,
128: classType);
129: Term initFalseTerm = tb.equals(tb.var(initField), tb
130: .FALSE(services));
131: result = tb.and(result, initFalseTerm);
132:
133: //add explicit invariants
134: ListOfClassInvariant invs = modelClass.getMyClassInvariants();
135: invs = invs.append(modelClass.getMyThroughoutClassInvariants());
136: Term invTerm = translateInvs(invs);
137: result = tb.and(result, invTerm);
138:
139: return result;
140: }
141:
142: /**
143: * (helper for buildAssumedInvs())
144: * @throws SLTranslationError
145: */
146: private void buildInvariantTacletsForClass(ModelClass modelClass)
147: throws SLTranslationError {
148: Term invTerm = buildInvariantsForClass(modelClass);
149: ConstrainedFormula cf = new ConstrainedFormula(invTerm);
150: Semisequent ante = Semisequent.EMPTY_SEMISEQUENT.insertLast(cf)
151: .semisequent();
152: Sequent sequent = Sequent.createAnteSequent(ante);
153:
154: TacletGoalTemplate template = new TacletGoalTemplate(sequent,
155: SLListOfTaclet.EMPTY_LIST);
156:
157: NoFindTacletBuilder tacletBuilder = new NoFindTacletBuilder();
158: String name = "Insert invariants of "
159: + modelClass.getClassName();
160: tacletBuilder.setName(new Name(name));
161: tacletBuilder.addTacletGoalTemplate(template);
162: Taclet taclet = tacletBuilder.getNoFindTaclet();
163: invTaclets = invTaclets.add(taclet);
164: initConfig.getProofEnv().registerRule(taclet,
165: AxiomJustification.INSTANCE);
166: }
167:
168: private Term buildAssumedInvs() throws SLTranslationError {
169: Debug.assertTrue(invStrategy != null);
170: String ownFullName = modelClass.getFullClassName();
171: String ownPackageName = modelClass.getContainingPackage();
172: if (ownPackageName == null) {
173: ownPackageName = "";
174: }
175:
176: //inReachableState
177: Term result = tb.func(javaInfo.getInReachableState());
178:
179: //collect all translated invariants of all classes
180: Set allClasses = modelClass.getAllClasses();
181: Iterator it = allClasses.iterator();
182: while (it.hasNext()) {
183: ModelClass mc = (ModelClass) (it.next());
184:
185: //display only those designated by the invariant display strategy
186: if (invStrategy.preselectAll()
187: || (invStrategy.preselectPackage() && ownPackageName
188: .equals(mc.getContainingPackage()))
189: || (invStrategy.preselectClass() && ownFullName
190: .equals(mc.getFullClassName()))) {
191: Term classInvTerm = buildInvariantsForClass(mc);
192: result = tb.and(result, classInvTerm);
193: } else {
194: buildInvariantTacletsForClass(mc);
195: }
196: }
197:
198: return result;
199: }
200:
201: /**
202: * Builds the "general assumption" for a set of assumed invariants.
203: * @throws SLTranslationError
204: */
205: private Term buildGeneralAssumption(ProgramVariable selfVar,
206: ListOfProgramVariable paramVars) throws SLTranslationError {
207: Term result = null;
208:
209: //build conjunction of invariants
210: Term assumedInvsTerm = buildAssumedInvs();
211: result = assumedInvsTerm;
212:
213: //build disjunction of preconditions
214: if (!skipPreconditions) {
215: Term anyPreTerm = tb.ff();
216: ListOfOperationContract contracts = modelMethod
217: .getMyOperationContracts();
218: IteratorOfOperationContract it = contracts.iterator();
219: while (it.hasNext()) {
220: OperationContract contract = it.next();
221: Term term = translatePre(contract, selfVar,
222: toPV(paramVars));
223: anyPreTerm = tb.or(anyPreTerm, term);
224: }
225: result = tb.and(result, anyPreTerm);
226: }
227:
228: //build "self.<created> = TRUE & self != null"
229: if (selfVar != null) {
230: Term selfCreatedAndNotNullTerm = createdFactory
231: .createCreatedAndNotNullTerm(services, tb
232: .var(selfVar));
233: result = tb.and(result, selfCreatedAndNotNullTerm);
234: }
235:
236: //build conjunction of...
237: //- "p_i.<created> = TRUE | p_i = null" for object parameters, and
238: //- "inBounds(p_i)" for integer parameters
239: Term paramsLegalTerm = tb.tt();
240: IteratorOfProgramVariable it2 = paramVars.iterator();
241: while (it2.hasNext()) {
242: ProgramVariable paramVar = it2.next();
243: Term paramLegalTerm = tb.tt();
244: if (paramVar.sort() instanceof ObjectSort) {
245: paramLegalTerm = createdFactory
246: .createCreatedOrNullTerm(services, tb
247: .var(paramVar));
248: } else {
249: LDT ldt = services.getTypeConverter().getModelFor(
250: paramVar.sort());
251: if (ldt instanceof AbstractIntegerLDT) {
252: Function inBoundsPredicate = ((AbstractIntegerLDT) ldt)
253: .getInBoundsPredicate();
254: if (inBoundsPredicate != null) {
255: paramLegalTerm = tb.func(inBoundsPredicate, tb
256: .var(paramVar));
257: }
258: }
259: }
260: paramsLegalTerm = tb.and(paramsLegalTerm, paramLegalTerm);
261: }
262: result = tb.and(result, paramsLegalTerm);
263: return result;
264: }
265:
266: private JavaBlock buildJavaBlock(ProgramVariable[] formalParVars,
267: ProgramMethod programMethod, ProgramVariable selfVar,
268: ProgramVariable resultVar, ProgramVariable exceptionVar) {
269: //create method call
270: StatementBlock sb;
271: if (programMethod == null) {
272: //constructor
273: assert resultVar != null;
274: TypeReference typeRef = javaInfo
275: .createTypeReference(resultVar.getKeYJavaType());
276: New n = new New(formalParVars, typeRef, typeRef);
277: CopyAssignment copy = new CopyAssignment(resultVar, n);
278: sb = new StatementBlock(copy);
279: } else {
280: MethodBodyStatement call = new MethodBodyStatement(
281: programMethod, selfVar, resultVar,
282: new ArrayOfExpression(formalParVars));
283: sb = new StatementBlock(call);
284: }
285:
286: //create variables for try statement
287: KeYJavaType eType = javaInfo
288: .getTypeByClassName("java.lang.Throwable");
289: TypeReference excTypeRef = javaInfo.createTypeReference(eType);
290: ProgramElementName ePEN = new ProgramElementName("e");
291: ProgramVariable eVar = new LocationVariable(ePEN, eType);
292:
293: //create try statement
294: CopyAssignment nullStat = new CopyAssignment(exceptionVar,
295: NullLiteral.NULL);
296: VariableSpecification eSpec = new VariableSpecification(eVar);
297: ParameterDeclaration excDecl = new ParameterDeclaration(
298: new Modifier[0], excTypeRef, eSpec, false);
299: CopyAssignment assignStat = new CopyAssignment(exceptionVar,
300: eVar);
301: Catch catchStat = new Catch(excDecl, new StatementBlock(
302: assignStat));
303: Try tryStat = new Try(sb, new Branch[] { catchStat });
304: sb = new StatementBlock(new Statement[] { nullStat, tryStat });
305:
306: //create java block
307: JavaBlock result = JavaBlock.createJavaBlock(sb);
308:
309: return result;
310: }
311:
312: private Term buildProgramTerm(ProgramVariable[] parVars,
313: ProgramMethod programMethod, ProgramVariable selfVar,
314: ProgramVariable resultVar, ProgramVariable exceptionVar,
315: Term postTerm) {
316: //create formal parameters
317: ProgramVariable[] formalParVars = new ProgramVariable[parVars.length];
318: for (int i = 0; i < parVars.length; i++) {
319: ProgramElementName name = new ProgramElementName("_"
320: + parVars[i].name());
321: formalParVars[i] = new LocationVariable(name, parVars[i]
322: .getKeYJavaType());
323: registerInNamespaces(formalParVars[i]);
324: }
325:
326: //create java block
327: JavaBlock jb = buildJavaBlock(formalParVars, programMethod,
328: selfVar, resultVar, exceptionVar);
329:
330: //create program term
331: Term programTerm = tf.createProgramTerm(modality, jb, postTerm);
332:
333: //add updates
334: Term[] locs = new Term[parVars.length];
335: Term[] values = new Term[parVars.length];
336: for (int i = 0; i < parVars.length; i++) {
337: locs[i] = tb.var(formalParVars[i]);
338: values[i] = tb.var(parVars[i]);
339: }
340: Term updateTerm = tf
341: .createUpdateTerm(locs, values, programTerm);
342:
343: return updateTerm;
344: }
345:
346: //-------------------------------------------------------------------------
347: //methods of ProofOblInput interface
348: //-------------------------------------------------------------------------
349:
350: public void readProblem(ModStrategy mod) throws ProofInputException {
351: //make sure initConfig has been set
352: if (initConfig == null) {
353: throw new IllegalStateException("InitConfig not set.");
354: }
355:
356: //prepare variables, program method and container for @pre-functions
357: ListOfProgramVariable paramVars = buildParamVars(modelMethod);
358: ProgramMethod programMethod = getProgramMethod(paramVars);
359: ProgramVariable selfVar = null;
360: if (programMethod != null && !programMethod.isStatic()) {
361: selfVar = buildSelfVarAsProgVar();
362: }
363: ProgramVariable resultVar = buildResultVar(modelMethod);
364: ProgramVariable exceptionVar = buildExcVar();
365: Map atPreFunctions = new HashMap();
366:
367: try {
368: //build general assumption
369: Term gaTerm = buildGeneralAssumption(selfVar, paramVars);
370:
371: //get precondition defined by subclass
372: Term preTerm = getPreTerm(selfVar, paramVars, resultVar,
373: exceptionVar, atPreFunctions);
374:
375: //get postcondition defined by subclass
376: Term postTerm = getPostTerm(selfVar, paramVars, resultVar,
377: exceptionVar, atPreFunctions);
378:
379: //build program term
380: Term programTerm = buildProgramTerm(paramVars.toArray(),
381: programMethod, selfVar, resultVar, exceptionVar,
382: postTerm);
383:
384: //build definitions for @pre-functions
385: Term atPreDefinitionsTerm = buildAtPreDefinitions(atPreFunctions);
386:
387: //put everything together
388: Term result = tb.and(atPreDefinitionsTerm, gaTerm);
389: result = tb.and(result, preTerm);
390: result = tb.imp(result, programTerm);
391:
392: //save in field
393: poTerms = new Term[] { result };
394: poTaclets = new SetOfTaclet[] { invTaclets };
395:
396: } catch (SLTranslationError e) {
397: throw new ProofInputException(e);
398: }
399:
400: //register everything in namespaces
401: registerInNamespaces(selfVar);
402: registerInNamespaces(paramVars);
403: registerInNamespaces(resultVar);
404: registerInNamespaces(exceptionVar);
405: registerInNamespaces(atPreFunctions);
406: }
407:
408: public Contractable[] getObjectOfContract() {
409: return new Contractable[] { modelMethod };
410: }
411:
412: public boolean initContract(Contract ct) {
413: if (!(ct instanceof OldOperationContract)) {
414: return false;
415: }
416:
417: OldOperationContract mct = (OldOperationContract) ct;
418:
419: if (!(mct.getModelMethod().equals(modelMethod) && mct
420: .getModality().equals(modality))) {
421: return false;
422: }
423:
424: ct.addCompoundProof(getPO());
425: return true;
426: }
427: }
|