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.casetool.ModelMethod;
22: import de.uka.ilkd.key.logic.Term;
23: import de.uka.ilkd.key.logic.op.ListOfProgramVariable;
24: import de.uka.ilkd.key.logic.op.Op;
25: import de.uka.ilkd.key.logic.op.ProgramVariable;
26: import de.uka.ilkd.key.speclang.ListOfClassInvariant;
27: import de.uka.ilkd.key.speclang.SLTranslationError;
28:
29: /**
30: * The "PreservesInv" proof obligation.
31: */
32: public class PreservesInvPO extends EnsuresPO {
33:
34: private final ListOfClassInvariant ensuredInvs;
35:
36: protected PreservesInvPO(String name, ModelMethod modelMethod,
37: InvariantSelectionStrategy invStrategy,
38: ListOfClassInvariant ensuredInvs) {
39: super (name, modelMethod, Op.BOX, invStrategy, false);
40: this .ensuredInvs = ensuredInvs;
41: }
42:
43: public PreservesInvPO(ModelMethod modelMethod,
44: InvariantSelectionStrategy invStrategy,
45: ListOfClassInvariant ensuredInvs) {
46: this ("PreservesInv", modelMethod, invStrategy, ensuredInvs);
47: }
48:
49: protected Term getPreTerm(ProgramVariable selfVar,
50: ListOfProgramVariable paramVars, ProgramVariable resultVar,
51: ProgramVariable exceptionVar, Map atPreFunctions) {
52: return tb.tt();
53: }
54:
55: protected Term getPostTerm(ProgramVariable selfVar,
56: ListOfProgramVariable paramVars, ProgramVariable resultVar,
57: ProgramVariable exceptionVar, Map atPreFunctions)
58: throws SLTranslationError {
59: return translateInvs(ensuredInvs);
60: }
61: }
|