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: // This file is part of KeY - Integrated Deductive Software Design
009: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // 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.mgt;
018:
019: import java.util.List;
020: import java.util.Map;
021:
022: import de.uka.ilkd.key.casetool.ModelMethod;
023: import de.uka.ilkd.key.java.Services;
024: import de.uka.ilkd.key.java.Statement;
025: import de.uka.ilkd.key.java.statement.CatchAllStatement;
026: import de.uka.ilkd.key.jml.JMLLemmaMethodSpec;
027: import de.uka.ilkd.key.jml.JMLMethodSpec;
028: import de.uka.ilkd.key.logic.*;
029: import de.uka.ilkd.key.logic.op.*;
030: import de.uka.ilkd.key.pp.LogicPrinter;
031: import de.uka.ilkd.key.proof.Proof;
032: import de.uka.ilkd.key.proof.ProofAggregate;
033: import de.uka.ilkd.key.proof.ProofSaver;
034: import de.uka.ilkd.key.proof.init.JMLPostAndInvPO;
035: import de.uka.ilkd.key.proof.init.ProofOblInput;
036:
037: /**
038: * @deprecated
039: */
040: public class JMLMethodContract extends DefaultOperationContract {
041:
042: //iff true all existing invariants are added to the pre- and postcondition
043: //of the method contract, iff false only the invariants of the containing
044: //type and the instance invariants (if meth is not static) for the
045: //corresponding object are added. History constraints of the current type
046: //are always added.
047: public static final boolean allInvariants = true;
048: private ModelMethod meth;
049: private Modality modality;
050:
051: private JMLMethodSpec spec;
052:
053: public JMLMethodContract(ModelMethod meth, JMLMethodSpec spec,
054: Modality modality) {
055: this .meth = meth;
056: this .spec = spec;
057: this .modality = modality;
058: }
059:
060: public void addCompoundProof(ProofAggregate pl) {
061: proofs.add(pl);
062: }
063:
064: public boolean applicableForModality(Modality mod) {
065: return getModality().equals(
066: ModalityClass.getNormReprModality(mod));
067: }
068:
069: public DLMethodContract createDLMethodContract(Proof proof) {
070: return new DLMethodContract(getPre(), getPost(), spec
071: .getPi1Functional(), spec.introducedConstants(),
072: (Statement) spec.getProofStatement(), spec
073: .getAssignable(), modality,
074: "Derived JML Method Contract",
075: "Derived JML Method Contract", spec.getServices(), spec
076: .getNamespaces());
077: }
078:
079: public boolean equals(Object cmp) {
080: if (!(cmp instanceof JMLMethodContract))
081: return false;
082: final JMLMethodContract mc = (JMLMethodContract) cmp;
083: return meth.equals(getObjectOfContract())
084: && getModality() == mc.getModality()
085: && getSpec().equals(mc.getSpec());
086: }
087:
088: protected Term getAdditionalAxioms() {
089: return spec.getPi1Functional();
090: }
091:
092: public CatchAllStatement getCatchAllStatement() {
093: return spec.getCatchAllStatement();
094: }
095:
096: public String getHTMLText() {
097: return "<html>pre: "
098: + getPreText()
099: + "<br>post: "
100: + getPostText()
101: + "<br>modifies: "
102: + getModifiesText()
103: + "<br>termination: "
104: + (getModality() == Op.DIA ? "total" : getModality()
105: .toString()) + "</html>";
106: }
107:
108: public Modality getModality() {
109: return ModalityClass.getNormReprModality(modality);
110: }
111:
112: public ModelMethod getModelMethod() {
113: return meth;
114: }
115:
116: public SetOfLocationDescriptor getModifies() {
117: return spec.getAssignable();
118: }
119:
120: public String getModifiesText() {
121: return LogicPrinter.quickPrintLocationDescriptors(
122: getModifies(), spec.getServices());
123: }
124:
125: public String getName() {
126: return "JML Method Contract: "
127: + spec.getMethodDeclaration().getFullName()
128: + " (spec id:" + spec.id() + ")";
129: }
130:
131: public Object getObjectOfContract() {
132: return spec.getProgramMethod();
133: }
134:
135: public Term getPost() {
136: return spec.getCompletePostFunctional(false, false);
137: }
138:
139: public String getPostText() {
140: return ProofSaver.printTerm(getPost(), spec.getServices())
141: .toString();
142: }
143:
144: public Term getPre() {
145: return spec.getCompletePre(false, false, modality == Op.DIA);
146: }
147:
148: public String getPreText() {
149: return ProofSaver.printTerm(getPre(), spec.getServices())
150: .toString();
151: }
152:
153: public ProofEnvironment getProofEnv() {
154: return env;
155: }
156:
157: public ProofOblInput getProofOblInput(Proof proof) {
158: return new JMLPostAndInvPO(spec, env.getJavaModel()
159: .getModelDir(), allInvariants); //TODO
160: }
161:
162: public List getProofs() {
163: return proofs;
164: }
165:
166: public JMLMethodSpec getSpec() {
167: return spec;
168: }
169:
170: public Statement getStatement() {
171: return (Statement) spec.getProofStatement();
172: }
173:
174: public int hashCode() {
175: int result = 0;
176: result = 37 * result + meth.hashCode();
177: result = 37 * result + getModality().hashCode();
178: result = 37 * result + getSpec().hashCode();
179: return result;
180: }
181:
182: private static Name getNewName(Services services, Name baseName) {
183: NamespaceSet namespaces = services.getNamespaces();
184:
185: int i = 0;
186: Name name;
187: do {
188: name = new Name(baseName + "_" + i++);
189: } while (namespaces.lookup(name) != null);
190:
191: return name;
192: }
193:
194: protected void instantiateAtPreSymbols(Map replacementMap,
195: Namespace localFunctions, Namespace localProgramVariables) {
196: }
197:
198: protected void instantiateAuxiliarySymbols(Map replacementMap,
199: Namespace localFunctions, Namespace localProgramVariables,
200: Services services) {
201: IteratorOfQuantifierPrefixEntry it = spec.getOldLVs()
202: .iterator();
203: while (it.hasNext()) {
204: LogicVariable lv = (LogicVariable) it.next().getVariable();
205:
206: RigidFunction rf = (RigidFunction) spec.getLv2Const().get(
207: lv);
208: if (rf != null) {
209: Name name = getNewName(services, rf.name());
210: RigidFunction newRf = new RigidFunction(name,
211: rf.sort(), rf.argSort());
212: localFunctions.add(newRf);
213: replacementMap.put(rf, newRf);
214: }
215: }
216: IteratorOfOperator ito = spec.getOldFuncSymbols().iterator();
217: while (ito.hasNext()) {
218: Operator op = ito.next();
219: Name name = getNewName(services, op.name());
220: Operator newOp;
221: if (op instanceof RigidFunction) {
222: RigidFunction rf = (RigidFunction) op;
223: newOp = new RigidFunction(name, rf.sort(), rf.argSort());
224: } else {
225: LocationVariable lv = (LocationVariable) op;
226: newOp = new LocationVariable(new ProgramElementName(
227: name.toString()), lv.getKeYJavaType());
228: }
229: localFunctions.add(newOp);
230: replacementMap.put(op, newOp);
231: }
232: }
233:
234: /**
235: * adds programvariables used as instantiations for the method parameters
236: * to the corresponding map
237: * @param insts the {@link MethodContractInstantiation} with the concrete instantiation
238: * of the method body statement
239: * @param replacementMap the Map with all instantiations
240: */
241: protected void instantiateMethodParameters(
242: MethodContractInstantiation insts, Map replacementMap,
243: Namespace localFunctions, Namespace localProgramVariables) {
244: for (int i = 0; i < insts.getArgumentCount(); i++) {
245: replacementMap.put(spec.getParameterAt(i), insts
246: .getArgumentAt(i));
247: }
248: }
249:
250: /**
251: * @param insts
252: * @param replacementMap
253: */
254: protected void instantiateMethodReceiver(
255: MethodContractInstantiation insts, Map replacementMap,
256: Namespace localFunctions, Namespace localProgramVariables) {
257: if (spec.getSelf() != null) { // otherwise this is a static method call
258: replacementMap.put(spec.getSelf(), spec.getServices()
259: .getTypeConverter().convertToLogicElement(
260: insts.getReceiver()));
261: }
262: }
263:
264: /**
265: * @param insts
266: * @param replacementMap
267: */
268: protected void instantiateMethodReturnVariable(
269: MethodContractInstantiation insts, Map replacementMap,
270: Namespace localFunctions, Namespace localProgramVariables) {
271: replacementMap.put(spec.getResultVar(), insts.getResult());
272: }
273:
274: public void removeCompoundProof(ProofAggregate pl) {
275: proofs.remove(pl);
276: }
277:
278: public void setProofEnv(ProofEnvironment env) {
279: if (this .env == null) {
280: this .env = env;
281: } else if (this .env != env) {
282: throw new IllegalStateException(
283: "Method Contract may belong to "
284: + "only one environment.");
285: }
286: }
287:
288: public String toString() {
289: return "[JML] context "
290: + meth
291: + (spec == null ? "" : "\npre: "
292: + spec.getCompletePre(true, allInvariants,
293: modality == Op.DIA) + "\npost: "
294: + spec.getCompletePost(true, allInvariants)
295: + "\nmodifies: "
296: + spec.replaceModelFieldsInAssignable()
297: + "\npi1: "
298: + ((JMLLemmaMethodSpec) spec).getPi1()
299: + "\nmodality: " + modality);
300: }
301:
302: }
|