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: //
010: package de.uka.ilkd.key.proof.init;
011:
012: import java.util.Vector;
013: import java.util.HashMap;
014:
015: import de.uka.ilkd.key.java.declaration.ArrayOfParameterDeclaration;
016: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
017: import de.uka.ilkd.key.jml.JMLMethodSpec;
018: import de.uka.ilkd.key.jml.JMLSpec;
019: import de.uka.ilkd.key.jml.UsefulTools;
020: import de.uka.ilkd.key.logic.*;
021: import de.uka.ilkd.key.logic.op.Op;
022: import de.uka.ilkd.key.logic.op.ProgramVariable;
023: import de.uka.ilkd.key.proof.Proof;
024: import de.uka.ilkd.key.proof.ProofAggregate;
025: import de.uka.ilkd.key.proof.mgt.Contract;
026: import de.uka.ilkd.key.proof.mgt.Contractable;
027: import de.uka.ilkd.key.util.Debug;
028:
029: /** Represents a proof obligation for the assignable clause of a certain
030: * (jml) method specification case.
031: * @deprecated Replaced by RespectsModifiesPO.
032: */
033: public class AssignableCheckProofOblInput extends
034: ModifiesCheckProofOblInput implements JMLProofOblInput {
035:
036: private JMLMethodSpec spec;
037: private String javaPath;
038:
039: private boolean allInv = false;
040:
041: public AssignableCheckProofOblInput(JMLMethodSpec spec,
042: String javaPath) {
043: super ("Assignable PO for: " + spec, null);
044: this .javaPath = javaPath;
045: this .spec = spec;
046: location2descriptor = new HashMap();
047: }
048:
049: public void setAllInvariants(boolean allInv) {
050: this .allInv = allInv;
051: }
052:
053: public JMLSpec getSpec() {
054: return spec;
055: }
056:
057: private void createModifiesElements() {
058: modifiesElements = SetAsListOfTerm.EMPTY_SET;
059: SetOfLocationDescriptor locs = spec
060: .replaceModelFieldsInAssignable();
061: IteratorOfLocationDescriptor it = locs.iterator();
062: while (it.hasNext()) {
063: BasicLocationDescriptor bloc = (BasicLocationDescriptor) it
064: .next();
065: // Debug.assertTrue(bloc.getFormula().equals(tf.createJunctorTerm(Op.TRUE)));
066: // Debug.assertTrue(bloc.getLocTerm().freeVars().size() == 0);
067: location2descriptor.put(bloc.getLocTerm(), bloc);
068: modifiesElements = modifiesElements.add(bloc.getLocTerm());
069: }
070: }
071:
072: public void readProblem(ModStrategy mod) {
073: createModifiesElements();
074: MethodDeclaration md = spec.getMethodDeclaration();
075: initConfig.progVarNS().add(UsefulTools.buildParamNamespace(md));
076: initConfig.progVarNS().add(
077: spec.getProgramVariableNS().allElements());
078: if (spec.getMethodDeclaration().isStatic()) {
079: self = null;
080: } else {
081: self = (ProgramVariable) spec.getPrefix();
082: }
083: javaInfo = initConfig.getServices().getJavaInfo();
084: createModifiesElements();
085: pvVector = new Vector(md.getParameterDeclarationCount());
086: ArrayOfParameterDeclaration ap = md.getParameters();
087: for (int i = 0; i < ap.size(); i++) {
088: pvVector.add(ap.getParameterDeclaration(i)
089: .getVariableSpecification().getProgramVariable());
090: }
091: m = spec.getProgramMethod();
092:
093: // puts all occuring classes into the set occuringClasses
094: collectOccuringClasses(initConfig.getServices().getJavaInfo()
095: .getKeYJavaType(spec.getClassDeclaration()));
096:
097: proofObl = TermFactory.DEFAULT.createJunctorTermAndSimplify(
098: Op.IMP, spec.getCompletePre(true, allInv, false),
099: createProofStart());
100: proofObl = UsefulTools.quantifyProgramVariables(proofObl,
101: UsefulTools.buildParamNamespace(md).allElements()
102: .iterator(), Op.ALL, initConfig.getServices());
103: proofObl = spec.bindSpecVars(proofObl);
104: }
105:
106: public boolean checkPurity() {
107: return proofObl != null ? (UsefulTools.purityCheck(proofObl,
108: initConfig.getServices().getImplementation2SpecMap()) == null)
109: : true;
110: }
111:
112: /**
113: * The Java Model is already initialized;
114: */
115: public String readModel() {
116: return null;
117: }
118:
119: /** returns the path to the Java model.
120: */
121: public String getJavaPath() {
122: return javaPath;
123: }
124:
125: public Contractable[] getObjectOfContract() {
126: return new Contractable[] { spec.getProgramMethod() };
127: }
128:
129: public boolean initContract(Contract ct) {
130: return false; //%%
131: }
132:
133: public void startProtocol() {
134: // do nothing
135: }
136:
137: public String createProgramVarsSection() {
138: IteratorOfNamed it = initConfig.progVarNS().allElements()
139: .iterator();
140: String result = "\\programVariables {\n";
141: while (it.hasNext()) {
142: ProgramVariable pv = (ProgramVariable) it.next();
143: result += pv.sort() + " " + pv.name() + ";\n";
144: }
145: result += "}\n";
146: return result;
147: }
148:
149: public String createJavaSection() {
150: return "\\javaSource \"" + getJavaPath() + "\";\n";
151: }
152:
153: public String createProblemHeader() {
154: return createJavaSection() + "\n" + createProgramVarsSection()
155: + "\n";
156: }
157:
158: public ProofAggregate getPO() {
159: return ProofAggregate.createProofAggregate(new Proof(name(),
160: proofObl, createProblemHeader(), initConfig
161: .createTacletIndex(), initConfig
162: .createBuiltInRuleIndex(), initConfig
163: .getServices()), name());
164: }
165:
166: public String toString() {
167: return name();
168: }
169:
170: public String name() {
171: return "Assignable PO ("
172: + (allInv ? "all invariants" : "only invariants from "
173: + spec.getClassDeclaration().getName())
174: + ") for: " + spec;
175: }
176:
177: }
|