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: //
09: //
10: package de.uka.ilkd.key.proof.init;
11:
12: import de.uka.ilkd.key.jml.JMLClassSpec;
13: import de.uka.ilkd.key.jml.UsefulTools;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.logic.op.ProgramMethod;
16: import de.uka.ilkd.key.proof.Proof;
17: import de.uka.ilkd.key.proof.ProofAggregate;
18: import de.uka.ilkd.key.proof.mgt.Contract;
19:
20: /** the proofobligation for invariants and historyconstraints*/
21: public class JMLInvPO extends JMLProofOblInputImpl {
22:
23: private Term po = null;
24:
25: public JMLInvPO(JMLClassSpec spec, ProgramMethod pm,
26: String javaPath, boolean allInv) {
27: super (spec, javaPath, allInv);
28: this .pm = pm;
29: }
30:
31: public ProofAggregate getPO() {
32: return ProofAggregate.createProofAggregate(new Proof(name(),
33: po, createProblemHeader(), initConfig
34: .createTacletIndex(), initConfig
35: .createBuiltInRuleIndex(), initConfig
36: .getServices()), name());
37: }
38:
39: public void readProblem(ModStrategy mod) throws ProofInputException {
40: initConfig.progVarNS().add(
41: UsefulTools.buildParamNamespace(pm
42: .getMethodDeclaration()));
43: po = ((JMLClassSpec) spec).getPreservesInvariantBehavior(pm,
44: allInv);
45: initConfig.progVarNS().add(
46: spec.getProgramVariableNS().allElements());
47: if (allInv) {
48: initConfig.progVarNS().add(
49: initConfig.getServices()
50: .getImplementation2SpecMap()
51: .getAllInvPVNS().allElements());
52: }
53: }
54:
55: public boolean initContract(Contract ct) {
56: return false;
57: }
58:
59: public String name() {
60: return "Invariant "
61: + (allInv ? "(including all invariants)"
62: : "(only invariants for "
63: + ((JMLClassSpec) spec)
64: .getClassDeclaration()
65: .getName() + ")")
66: + " and History Constraint PO for "
67: + pm.getMethodDeclaration().getName();
68: }
69:
70: public boolean checkPurity() {
71: return po != null ? (UsefulTools.purityCheck(po, initConfig
72: .getServices().getImplementation2SpecMap()) == null)
73: : true;
74: }
75:
76: }
|