001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
011: // and Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016:
017: package de.uka.ilkd.key.proof.init;
018:
019: import de.uka.ilkd.key.jml.JMLMethodSpec;
020: import de.uka.ilkd.key.jml.UsefulTools;
021: import de.uka.ilkd.key.logic.Term;
022: import de.uka.ilkd.key.proof.Proof;
023: import de.uka.ilkd.key.proof.ProofAggregate;
024: import de.uka.ilkd.key.proof.mgt.Contract;
025: import de.uka.ilkd.key.proof.mgt.Contractable;
026: import de.uka.ilkd.key.proof.mgt.JMLMethodContract;
027: import de.uka.ilkd.key.proof.mgt.JavaModelMethod;
028:
029: public class JMLPostAndInvPO extends JMLProofOblInputImpl {
030:
031: private Term po = null;
032: private JavaModelMethod jmm = null;
033: private ProofAggregate result;
034:
035: public JMLPostAndInvPO(JMLMethodSpec spec, String javaPath,
036: boolean allInv) {
037: super (spec, javaPath, allInv);
038: pm = spec.getProgramMethod();
039: jmm = new JavaModelMethod(spec.getProgramMethod(), javaPath,
040: null); //TODO
041: }
042:
043: public ProofAggregate getPO() {
044: if (result != null)
045: return result;
046: return result = ProofAggregate.createProofAggregate(new Proof(
047: name(), po, createProblemHeader(), initConfig
048: .createTacletIndex(), initConfig
049: .createBuiltInRuleIndex(), initConfig
050: .getServices()), name());
051: }
052:
053: public void readProblem(ModStrategy mod) throws ProofInputException {
054: initConfig.progVarNS().add(
055: UsefulTools.buildParamNamespace(pm
056: .getMethodDeclaration()));
057: po = ((JMLMethodSpec) spec).createDLFormula(true, allInv);
058: initConfig.progVarNS().add(
059: spec.getProgramVariableNS().allElements());
060: if (allInv) {
061: initConfig.progVarNS().add(
062: initConfig.getServices()
063: .getImplementation2SpecMap()
064: .getAllInvPVNS().allElements());
065: }
066: }
067:
068: public boolean initContract(Contract ct) {
069: if (!(ct instanceof JMLMethodContract)
070: || allInv != JMLMethodContract.allInvariants) {
071: return false;
072: }
073: if (((JMLMethodContract) ct).getSpec() != spec) {
074: return false;
075: }
076: ct.addCompoundProof(getPO());
077: return true;
078: }
079:
080: public boolean checkPurity() {
081: return po != null ? (UsefulTools.purityCheck(po, initConfig
082: .getServices().getImplementation2SpecMap()) == null)
083: : true;
084: }
085:
086: public Contractable[] getObjectOfContract() {
087: return new Contractable[] { jmm };
088: }
089:
090: public String name() {
091: return "Post, Invariant "
092: + (allInv ? "(including all invariants)"
093: : "(only invariants for "
094: + ((JMLMethodSpec) spec)
095: .getClassDeclaration()
096: .getName() + ")")
097: + " and Constraint PO for spec:\n " + spec.toString();
098: }
099:
100: }
|