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 "PreservesThroughout" proof obligation.
31: */
32: public class PreservesThroughoutPO extends EnsuresPO {
33:
34: private ListOfClassInvariant invs;
35:
36: public PreservesThroughoutPO(ModelMethod modelMethod,
37: ListOfClassInvariant invs,
38: InvariantSelectionStrategy invStrategy) {
39: super ("PreservesThroughout", modelMethod, Op.TOUT, invStrategy,
40: true);
41: this .invs = invs;
42: }
43:
44: protected Term getPreTerm(ProgramVariable selfVar,
45: ListOfProgramVariable paramVars, ProgramVariable resultVar,
46: ProgramVariable exceptionVar, Map atPreFunctions) {
47: return tb.tt();
48: }
49:
50: protected Term getPostTerm(ProgramVariable selfVar,
51: ListOfProgramVariable paramVars, ProgramVariable resultVar,
52: ProgramVariable exceptionVar, Map atPreFunctions)
53: throws SLTranslationError {
54: return translateInvs(invs);
55: }
56: }
|