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.init;
019:
020: import java.io.File;
021: import java.util.HashMap;
022: import java.util.Iterator;
023:
024: import de.uka.ilkd.key.gui.Main;
025: import de.uka.ilkd.key.logic.*;
026: import de.uka.ilkd.key.logic.op.Function;
027: import de.uka.ilkd.key.logic.op.ProgramVariable;
028: import de.uka.ilkd.key.proof.Proof;
029: import de.uka.ilkd.key.proof.ProofAggregate;
030: import de.uka.ilkd.key.proof.SingleProof;
031: import de.uka.ilkd.key.proof.mgt.*;
032: import de.uka.ilkd.key.rule.*;
033: import de.uka.ilkd.key.rule.soundness.POBuilder;
034: import de.uka.ilkd.key.rule.soundness.POSelectionDialog;
035: import de.uka.ilkd.key.rule.soundness.SVSkolemFunction;
036: import de.uka.ilkd.key.util.ProgressMonitor;
037:
038: public class TacletSoundnessPO extends KeYUserProblemFile implements
039: ProofOblInput {
040:
041: public boolean askUserForEnvironment() {
042: return false;
043: }
044:
045: private ProofAggregate proof;
046:
047: private NoPosTacletApp[] app;
048:
049: public TacletSoundnessPO(String name, File file,
050: ProgressMonitor monitor) {
051: super (name, file, monitor);
052: this .tacletFile = true;
053: }
054:
055: /** returns the proof obligation term as result of the proof obligation
056: * input. If there is still no input available because nothing has
057: * been read yet null is returned.
058: */
059: public ProofAggregate getPO() {
060: return proof;
061: }
062:
063: public NoPosTacletApp[] getTaclets() {
064: return app;
065: }
066:
067: /** starts reading the input and modifies the InitConfig of this
068: * object with respect to the given modification
069: * strategy.
070: */
071: public void readProblem(ModStrategy mod) throws ProofInputException {
072:
073: final InitConfig old = initConfig;
074: initConfig = old.copy();
075:
076: // ensure that only the new taclets of the lemma file are presented to
077: // the user
078: initConfig.setTaclets(SetAsListOfTaclet.EMPTY_SET);
079: initConfig.setTaclet2Builder(new HashMap());
080:
081: SetOfTaclet newTaclets = null;
082: try {
083: super .read(ModStrategy.NO_VARS_FUNCS); // actually this
084: // reads the
085: // complete
086: // problem, which is not really
087: // needed; could be optimized
088: newTaclets = initConfig.getTaclets();
089: } finally {
090: initConfig = old;
091: }
092: // this ensures that necessary Java types are loaded
093: initConfig.getServices().getJavaInfo().readJavaBlock("{}");
094:
095: IteratorOfTaclet it = newTaclets.iterator();
096: SetOfNoPosTacletApp newTacApps = SetAsListOfNoPosTacletApp.EMPTY_SET;
097: while (it.hasNext()) {
098: newTacApps = newTacApps.add(NoPosTacletApp
099: .createNoPosTacletApp(it.next()));
100: }
101:
102: final POSelectionDialog dialog = new POSelectionDialog(Main
103: .getInstance().mediator(), newTacApps);
104:
105: app = dialog.getSelectedTaclets();
106:
107: if (app == null || app.length == 0)
108: throw new ProofInputException("No taclet was selected");
109:
110: ProofAggregate[] singleProofs = new ProofAggregate[app.length];
111: ProofEnvironment env = initConfig.getProofEnv();
112: for (int i = 0; i < app.length; i++) {
113: final POBuilder pob = new POBuilder(app[i], initConfig
114: .getServices());
115: pob.build();
116:
117: updateNamespaces(pob);
118: String name = app.length == 1 ? name() : app[i].taclet()
119: .name().toString();
120: singleProofs[i] = ProofAggregate.createProofAggregate(
121: new Proof(name, pob.getPOTerm(),
122: createProofHeader(), initConfig
123: .createTacletIndex(), initConfig
124: .createBuiltInRuleIndex(),
125: initConfig.getServices()), name);
126: }
127: if (app.length == 1) {
128: proof = singleProofs[0];
129: } else {
130: proof = ProofAggregate.createProofAggregate(singleProofs,
131: name());
132: }
133: for (int i = 0; i < app.length; i++) {
134: LemmaSpec lemmaSpec = new LemmaSpec(app[i]);
135: env.addContract(lemmaSpec);
136: env.registerRule(app[i], new RuleJustificationBySpec(
137: lemmaSpec));
138: env.addToAllProofs(app[i], file);
139: }
140: env.registerProof(this , proof);
141: }
142:
143: private void updateNamespaces(POBuilder p_pob) {
144: NamespaceSet globalNss = initConfig.namespaces();
145: Namespace funcNs = globalNss.functions();
146:
147: {
148: final IteratorOfNamed it = p_pob.getFunctions()
149: .allElements().iterator();
150: while (it.hasNext())
151: funcNs.add(it.next());
152: }
153:
154: // {
155: // final IteratorOfTacletApp it = p_pob.getTaclets ().iterator ();
156: // while ( it.hasNext () )
157: // p_tacletIndex.add((NoPosTacletApp)it.next ());
158: // }
159: }
160:
161: /** set the initial configuration used to read an input. It may become
162: * modified during reading depending on the modification strategy used
163: * for reading.
164: */
165: public void setInitConfig(InitConfig i) {
166: initConfig = i;
167: }
168:
169: public void readActivatedChoices() throws ProofInputException {
170: //nothing to do
171: }
172:
173: /** reads the include section and returns an Includes object.
174: */
175: public Includes readIncludes() throws ProofInputException {
176: return new Includes();
177: }
178:
179: /** returns the name of the proof obligation input.
180: */
181: public String name() {
182: if (app == null)
183: return "Taclet proof obligation";
184: return "Proof obligation(s) for " + file;
185: }
186:
187: public Contractable[] getObjectOfContract() {
188: return app;
189: }
190:
191: public boolean initContract(Contract ct) {
192: if (!(ct instanceof LemmaSpec)) {
193: return false;
194: }
195: LemmaSpec lct = (LemmaSpec) ct;
196: Contractable[] objs = getObjectOfContract();
197: boolean found = false;
198: for (int i = 0; i < objs.length; i++) {
199: if (objs[i].equals(lct.getObjectOfContract())) {
200: if (getPO() instanceof SingleProof) {
201: ct.addCompoundProof(getPO());
202: } else {
203: ct.addCompoundProof(getPO().getChildren()[i]);
204: }
205: found = true;
206: }
207: }
208: return found;
209: }
210:
211: /**
212: * Creates declarations necessary to save/load proof in textual form.
213: */
214: private String createProofHeader() throws ProofInputException {
215: String result = "";
216:
217: //includes of taclet file must be copied
218: Iterator it = super .readIncludes().getIncludes().iterator();
219: while (it.hasNext()) {
220: String fileName = (String) it.next();
221: result += "\\include \"" + fileName + "\";\n";
222: }
223:
224: //created SVSkolemFunctions must be declared
225: result += "\n\\functions {\n";
226: IteratorOfNamed it2 = initConfig.namespaces().functions()
227: .allElements().iterator();
228: while (it2.hasNext()) {
229: Function f = (Function) it2.next();
230: if (f instanceof SVSkolemFunction) {
231: result += f.proofToString();
232: }
233: }
234: result += "}\n\n";
235:
236: return result;
237: }
238: }
|