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: package de.uka.ilkd.key.visualdebugger;
009:
010: import de.uka.ilkd.key.gui.configuration.ProofSettings;
011: import de.uka.ilkd.key.logic.*;
012: import de.uka.ilkd.key.logic.op.Op;
013: import de.uka.ilkd.key.proof.BuiltInRuleIndex;
014: import de.uka.ilkd.key.proof.Proof;
015: import de.uka.ilkd.key.proof.ProofAggregate;
016: import de.uka.ilkd.key.proof.TacletIndex;
017: import de.uka.ilkd.key.proof.init.*;
018: import de.uka.ilkd.key.proof.mgt.Contract;
019: import de.uka.ilkd.key.proof.mgt.Contractable;
020: import de.uka.ilkd.key.visualdebugger.executiontree.ITNode;
021:
022: public class DebuggerPO implements ProofOblInput {
023:
024: private BuiltInRuleIndex builtInRules;
025:
026: /** the init config of the mainof */
027: private InitConfig initConfig;
028:
029: /** the name of the po */
030: private String name;
031:
032: /** the proof aggregate for this proof obligation */
033: private ProofAggregate po;
034:
035: private Sequent sequent = null;
036:
037: private ProofSettings settings;
038:
039: /** the formula used for specification computation of the body */
040: private Term specFormula = null;// TermFactory.DEFAULT.createJunctorTerm(Op.TRUE);
041:
042: private TacletIndex taclets;
043:
044: /**
045: * creates an instance of this proof obligation
046: *
047: * @param name
048: * a String with a short describing name what is computed
049: */
050: public DebuggerPO(String name) {
051: this .name = name;
052: }
053:
054: public boolean askUserForEnvironment() {
055: return false;
056: }
057:
058: private Term createConjunction(ListOfTerm list) {
059: Term result = null;
060: for (IteratorOfTerm it = list.iterator(); it.hasNext();) {
061: Term t = it.next();
062: if (result == null)
063: result = t;
064: else
065: result = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
066: result, t);
067:
068: }
069: if (result == null)
070: result = TermFactory.DEFAULT.createJunctorTerm(Op.TRUE);
071: return result;
072:
073: }
074:
075: public String getJavaPath() throws ProofInputException {
076: return null;
077: }
078:
079: public Contractable[] getObjectOfContract() {
080: return new Contractable[0];
081: }
082:
083: /**
084: * returns the proof to be loaded in the prover
085: */
086: public ProofAggregate getPO() {
087: if (po == null) {
088: if ((specFormula == null && sequent == null)
089: || taclets == null || builtInRules == null
090: || initConfig == null || settings == null) {
091: throw new IllegalStateException(
092: "Loop specification proof "
093: + "obligation is not initialized completely.");
094: }
095:
096: Proof proof = null;
097: if (specFormula != null)
098: proof = new Proof(name, specFormula, "", taclets,
099: builtInRules, initConfig.getServices(),
100: settings);
101: else if (sequent != null) {
102: proof = new Proof(name, sequent, "", taclets,
103: builtInRules, initConfig.getServices(),
104: settings);
105: }
106: proof.setSimplifier(settings
107: .getSimultaneousUpdateSimplifierSettings()
108: .getSimplifier());
109: po = ProofAggregate.createProofAggregate(proof, name);
110:
111: }
112: return po;
113: }
114:
115: private ListOfTerm getTerms(ListOfConstrainedFormula list) {
116: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
117: for (IteratorOfConstrainedFormula it = list.iterator(); it
118: .hasNext();) {
119: result = result.append(it.next().formula());
120: }
121: return result;
122: }
123:
124: public boolean initContract(Contract ct) {
125: // TODO Auto-generated method stub
126: return false;
127: }
128:
129: public void initJavaModelSettings(String classPath) {
130:
131: }
132:
133: private Term list2term(ListOfTerm list) {
134: Term result = null;
135: for (IteratorOfTerm it = list.iterator(); it.hasNext();) {
136: Term t = it.next();
137: t = TermFactory.DEFAULT.createJunctorTerm(Op.NOT, t);
138: if (result == null)
139: result = t;
140: else
141: result = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
142: result, t);
143:
144: }
145: if (result == null)
146: result = TermFactory.DEFAULT.createJunctorTerm(Op.TRUE);
147: return result;
148:
149: }
150:
151: public String name() {
152: return name;
153: }
154:
155: // all below are not used for this proof obligation
156: public void read(ModStrategy mod) {
157: }
158:
159: public void readActivatedChoices() {
160: }
161:
162: public Includes readIncludes() throws ProofInputException {
163: return null;
164: }
165:
166: public String readModel() throws ProofInputException {
167: return null;
168: }
169:
170: public void readProblem(ModStrategy mod) {
171: }
172:
173: public void readSpecs() {
174: }
175:
176: /**
177: * the initial config containing for example the services which provide
178: * access to the Java model
179: */
180: public void setConfig(InitConfig i) {
181: this .initConfig = i;
182: }
183:
184: /**
185: * the indices with the rules to be used for specification computation
186: *
187: * @param taclets
188: * the TacletIndex with the taclet rule base to be used
189: * @param builtInRules
190: * the BuiltInRuleIndex with all available built-in rules
191: */
192: public void setIndices(TacletIndex taclets,
193: BuiltInRuleIndex builtInRules) {
194: this .taclets = taclets;
195: this .builtInRules = builtInRules;
196: }
197:
198: public void setInitConfig(InitConfig i) {
199: // TODO Auto-generated method stub
200:
201: }
202:
203: public void setPCImpl(ListOfTerm l1, ListOfTerm l2) {
204: Term t1 = list2term(l1);
205: Term t2 = list2term(l2);
206: specFormula = TermFactory.DEFAULT.createJunctorTerm(Op.IMP,
207: new Term[] { t1, t2 });
208: }
209:
210: /**
211: * the proof settings to be used
212: *
213: * @param settings
214: * the ProofSettings to be used for e.g. the update
215: * simplifier to be taken
216: */
217: public void setProofSettings(ProofSettings settings) {
218: this .settings = settings;
219: }
220:
221: public void setSequent(Sequent s) {
222: this .sequent = s;
223: }
224:
225: public void setSpecFormula(ListOfTerm specFormula) {
226: Term result = null;
227: for (IteratorOfTerm it = specFormula.iterator(); it.hasNext();) {
228: Term t = it.next();
229: t = TermFactory.DEFAULT.createJunctorTerm(Op.NOT, t);
230: if (result == null)
231: result = t;
232: else
233: result = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
234: result, t);
235: }
236: this .specFormula = result;
237: }
238:
239: public void setSpecFormula(Sequent s) {
240: Semisequent ant = s.antecedent();
241: Semisequent succ = s.succedent();
242:
243: Term a = TermFactory.DEFAULT.createJunctorTerm(Op.AND,
244: getTerms(ant.toList()).toArray());
245: Term b = TermFactory.DEFAULT.createJunctorTerm(Op.OR, getTerms(
246: succ.toList()).toArray());
247: specFormula = TermFactory.DEFAULT.createJunctorTerm(Op.IMP, a,
248: b);
249: }
250:
251: /**
252: * the formula with the program whose specification has to be computed
253: *
254: * @param specFormula
255: * the Term to be loaded
256: */
257: public void setSpecFormula(Term specFormula) {
258: this .specFormula = specFormula;
259: }
260:
261: public void setTerms(ListOfTerm terms) {
262: this .specFormula = this .createConjunction(terms);
263: specFormula = TermFactory.DEFAULT.createJunctorTerm(Op.NOT,
264: specFormula);
265: }
266:
267: public void setUp(Sequent precondition, ITNode n) {
268: Sequent result = precondition;
269: for (IteratorOfTerm it = n.getPc(true).iterator(); it.hasNext();) {
270: Term t = it.next();
271: if (t.op() == Op.NOT)
272: result = result.addFormula(
273: new ConstrainedFormula(t.sub(0),
274: Constraint.BOTTOM), false, true)
275: .sequent();
276: else
277: result = result.addFormula(
278: new ConstrainedFormula(t, Constraint.BOTTOM),
279: true, true).sequent();
280:
281: }
282: this .sequent = result;
283: }
284:
285: public void setUp(Sequent precondition, ITNode n,
286: SetOfTerm indexConf) {
287: this .setUp(precondition, n);
288: for (IteratorOfTerm it = indexConf.iterator(); it.hasNext();) {
289: Term t = it.next();
290: if (t.op() == Op.NOT)
291: this .sequent = sequent.addFormula(
292: new ConstrainedFormula(t.sub(0),
293: Constraint.BOTTOM), false, true)
294: .sequent();
295: else
296: sequent = sequent.addFormula(
297: new ConstrainedFormula(t, Constraint.BOTTOM),
298: true, true).sequent();
299: }
300: }
301:
302: public void setUp(Sequent precondition, ITNode n,
303: SetOfTerm indexConf, Term post) {
304: this .setUp(precondition, n, indexConf);
305: sequent = sequent.addFormula(
306: new ConstrainedFormula(post, Constraint.BOTTOM), false,
307: true).sequent();
308:
309: }
310:
311: public void startProtocol() {
312: }
313:
314: }
|