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.JMLMethodSpec;
13: import de.uka.ilkd.key.jml.UsefulTools;
14: import de.uka.ilkd.key.logic.Term;
15: import de.uka.ilkd.key.proof.Proof;
16: import de.uka.ilkd.key.proof.ProofAggregate;
17:
18: public class JMLPostPO extends JMLProofOblInputImpl {
19:
20: private Term po = null;
21:
22: public JMLPostPO(JMLMethodSpec spec, String javaPath, boolean allInv) {
23: super (spec, javaPath, allInv);
24: pm = spec.getProgramMethod();
25: }
26:
27: public ProofAggregate getPO() {
28: return ProofAggregate.createProofAggregate(new Proof(name(),
29: po, createProblemHeader(), initConfig
30: .createTacletIndex(), initConfig
31: .createBuiltInRuleIndex(), initConfig
32: .getServices()), name());
33: }
34:
35: public void readProblem(ModStrategy mod) throws ProofInputException {
36: initConfig.progVarNS().add(
37: UsefulTools.buildParamNamespace(pm
38: .getMethodDeclaration()));
39:
40: po = ((JMLMethodSpec) spec).createDLFormula(false, allInv);
41:
42: initConfig.progVarNS().add(
43: spec.getProgramVariableNS().allElements());
44: if (allInv) {
45: initConfig.progVarNS().add(
46: initConfig.getServices()
47: .getImplementation2SpecMap()
48: .getAllInvPVNS().allElements());
49: }
50: }
51:
52: public boolean checkPurity() {
53: return UsefulTools.purityCheck((JMLMethodSpec) spec, initConfig
54: .getServices().getImplementation2SpecMap()) == null;
55: }
56:
57: public String name() {
58: return "Ensures Post Condition PO (using "
59: + (allInv ? "all invariants" : "only invariants from "
60: + ((JMLMethodSpec) spec).getClassDeclaration()
61: .getName())
62: + " for the precondition) Condition PO for:\n "
63: + spec.toString();
64: }
65:
66: }
|