01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
09: // Universitaet Koblenz-Landau, Germany
10: // Chalmers University of Technology, Sweden
11: //
12: // The KeY system is protected by the GNU General Public License.
13: // See LICENSE.TXT for details.
14: //
15: //
16:
17: package de.uka.ilkd.key.proof.init;
18:
19: import java.util.Map;
20:
21: import de.uka.ilkd.key.logic.Term;
22: import de.uka.ilkd.key.logic.ldt.AbstractIntegerLDT;
23: import de.uka.ilkd.key.logic.ldt.LDT;
24: import de.uka.ilkd.key.logic.op.Function;
25: import de.uka.ilkd.key.logic.op.ListOfProgramVariable;
26: import de.uka.ilkd.key.logic.op.Modality;
27: import de.uka.ilkd.key.logic.op.ProgramVariable;
28: import de.uka.ilkd.key.logic.sort.ObjectSort;
29: import de.uka.ilkd.key.speclang.OperationContract;
30: import de.uka.ilkd.key.speclang.SLTranslationError;
31:
32: /**
33: * The "EnsuresPost" proof obligation.
34: */
35: public class EnsuresPostPO extends EnsuresPO {
36:
37: private final OperationContract contract;
38:
39: public EnsuresPostPO(OperationContract contract, Modality modality,
40: InvariantSelectionStrategy invStrategy) {
41: super ("EnsuresPost of " + contract.getModelMethod(), contract
42: .getModelMethod(), modality, invStrategy, true);
43: this .contract = contract;
44: }
45:
46: protected Term getPreTerm(ProgramVariable selfVar,
47: ListOfProgramVariable paramVars, ProgramVariable resultVar,
48: ProgramVariable exceptionVar, Map atPreFunctions)
49: throws SLTranslationError {
50: return translatePre(contract, selfVar, toPV(paramVars));
51: }
52:
53: protected Term getPostTerm(ProgramVariable selfVar,
54: ListOfProgramVariable paramVars, ProgramVariable resultVar,
55: ProgramVariable exceptionVar, Map atPreFunctions)
56: throws SLTranslationError {
57: Term result = translatePost(contract, selfVar, toPV(paramVars),
58: resultVar, exceptionVar);
59:
60: //add implicit postcondition
61: Term implicitPostTerm = tb.tt();
62: if (resultVar != null) {
63: if (resultVar.sort() instanceof ObjectSort) {
64: implicitPostTerm = createdFactory
65: .createCreatedOrNullTerm(services, tb
66: .var(resultVar));
67: } else {
68: LDT ldt = services.getTypeConverter().getModelFor(
69: resultVar.sort());
70: if (ldt instanceof AbstractIntegerLDT) {
71: Function inBoundsPredicate = ((AbstractIntegerLDT) ldt)
72: .getInBoundsPredicate();
73: if (inBoundsPredicate != null) {
74: implicitPostTerm = tb.func(inBoundsPredicate,
75: tb.var(resultVar));
76: }
77: }
78: }
79: }
80: final Term excNotNullTerm = tb.not(tb.equals(tb
81: .var(exceptionVar), tb.NULL(services)));
82: implicitPostTerm = tb.or(implicitPostTerm, excNotNullTerm);
83: result = tb.and(result, implicitPostTerm);
84:
85: return result;
86: }
87: }
|