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:
018: package de.uka.ilkd.key.proof.mgt;
019:
020: import de.uka.ilkd.key.java.Services;
021: import de.uka.ilkd.key.java.Statement;
022: import de.uka.ilkd.key.java.StatementBlock;
023: import de.uka.ilkd.key.java.statement.Desugarable;
024: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
025: import de.uka.ilkd.key.logic.*;
026: import de.uka.ilkd.key.logic.op.Modality;
027: import de.uka.ilkd.key.logic.op.Op;
028: import de.uka.ilkd.key.proof.Proof;
029: import de.uka.ilkd.key.proof.ProofAggregate;
030: import de.uka.ilkd.key.proof.init.*;
031: import de.uka.ilkd.key.util.KeYExceptionHandler;
032:
033: /**
034: * represents a proof obligation input to the prover for a DLMethodContract
035: */
036: public class DLHoareTriplePO implements ProofOblInput {
037:
038: private ProofAggregate res;
039: private Term term;
040: private InitConfig initConfig;
041: private String name;
042: private Contractable[] contractable;
043: private String header; // needed to loaded the proof later
044: DLMethodContract ct;
045:
046: public DLHoareTriplePO(Term t, Modality mod, String header,
047: String name, Services services, DLMethodContract ct) {
048: this .ct = ct;
049: this .term = desugar(t, mod);
050: this .name = name;
051: this .header = header;
052: Statement pe = (Statement) t.sub(1).javaBlock().program();
053: Statement unwrapped = DLMethodContract.unwrapBlocks(pe, false);
054: if (unwrapped instanceof MethodBodyStatement) {
055: contractable = new Contractable[] { ((MethodBodyStatement) unwrapped)
056: .getProgramMethod(services) };
057: } else if (unwrapped instanceof Contractable) {
058: contractable = new Contractable[] { (Contractable) unwrapped };
059: } else {
060: throw new IllegalStateException(
061: "DL Hoare Triple Contract defined "
062: + "on illegal statement " + unwrapped);
063: }
064: }
065:
066: private static Term desugar(Term fma, Modality mod) {
067: TermFactory tf = TermFactory.DEFAULT;
068: StatementBlock sta = (StatementBlock) fma.sub(1).javaBlock()
069: .program();
070: Statement unwrapped = DLMethodContract.unwrapBlocks(sta, true);
071: if (unwrapped instanceof Desugarable) {
072: sta = (StatementBlock) ((Desugarable) unwrapped).desugar();
073: }
074: Term result = tf.createJunctorTerm(Op.IMP, fma.sub(0), tf
075: .createProgramTerm(mod, JavaBlock.createJavaBlock(sta),
076: fma.sub(1).sub(0)));
077:
078: return result.equals(fma) ? fma : result;
079: }
080:
081: /** returns the proof obligation term as result of the proof obligation
082: * input. If there is still no input available because nothing has
083: * been read yet null is returned.
084: */
085: public ProofAggregate getPO() {
086: return res;
087: }
088:
089: // public void setSettings(ProofSettings settings) {
090: // this.settings = settings;
091: // }
092:
093: /** starts reading the input and modifies the InitConfig of this
094: * object with respect to the given modification
095: * strategy.
096: */
097: public void readProblem(ModStrategy mod) throws ProofInputException {
098: initConfig.getServices().getNamespaces().programVariables()
099: .add(ct.getProgramVariables());
100:
101: Proof p = new Proof(name(), term, header, initConfig
102: .createTacletIndex(), initConfig
103: .createBuiltInRuleIndex(), initConfig.getServices(),
104: initConfig.mergedProofSettings());
105: res = ProofAggregate.createProofAggregate(p, name());
106:
107: }
108:
109: public void setExceptionHandler(KeYExceptionHandler keh) {
110: }
111:
112: public boolean askUserForEnvironment() {
113: return false;
114: }
115:
116: /** reads the Java model that belongs to this input.
117: */
118: public String readModel() throws ProofInputException {
119: return "";
120: }
121:
122: /** returns the path to the Java model.
123: */
124: public String getJavaPath() {
125: return "";
126: }
127:
128: /** set the initial configuration used to read an input. It may become
129: * modified during reading depending on the modification strategy used
130: * for reading.
131: */
132: public void setInitConfig(InitConfig i) {
133: this .initConfig = i;
134: }
135:
136: public void readSpecs() {
137: }
138:
139: public void readActivatedChoices() throws ProofInputException {
140: //nothing to do
141: }
142:
143: public SetOfChoice getActivatedChoices() throws ProofInputException {
144: return initConfig.getActivatedChoices();
145: }
146:
147: /** reads the include section and returns an Includes object.
148: */
149: public Includes readIncludes() throws ProofInputException {
150: return null;
151: }
152:
153: /** returns the name of the proof obligation input.
154: */
155: public String name() {
156: return name;
157: }
158:
159: /**
160: * returns the object for which this proof obligation proves a contract on.
161: * In this case we assume that the first program element of the second
162: * subterm of the
163: * proof obligation is a method body statement of which the according program
164: * method is returned.
165: */
166: public Contractable[] getObjectOfContract() {
167: return contractable;
168: }
169:
170: /**
171: * initialises the contract, that is, it adds the proof created by this PO input
172: * to the contract if the given contract is the same as that of the PO. Then true
173: * is returned. Otherwise nothing is done and false is returned.
174: */
175: public boolean initContract(Contract ct) {
176: if (ct == this .ct) {
177: ct.addCompoundProof(getPO());
178: return true;
179: } else {
180: return false;
181: }
182: }
183:
184: public void startProtocol() {
185: // do nothing
186: }
187:
188: public Term getTerm() {
189: return term;
190: }
191:
192: public void setPO(ProofAggregate po) {
193: res = po;
194: }
195: }
|