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:
011: package de.uka.ilkd.key.cspec;
012:
013: import java.util.Iterator;
014: import java.util.LinkedList;
015: import java.util.List;
016:
017: import de.uka.ilkd.key.gui.AutoModeListener;
018: import de.uka.ilkd.key.gui.KeYMediator;
019: import de.uka.ilkd.key.logic.*;
020: import de.uka.ilkd.key.logic.op.Junctor;
021: import de.uka.ilkd.key.logic.op.LocationVariable;
022: import de.uka.ilkd.key.logic.op.Op;
023: import de.uka.ilkd.key.logic.op.ProgramVariable;
024: import de.uka.ilkd.key.proof.IteratorOfGoal;
025: import de.uka.ilkd.key.proof.Proof;
026: import de.uka.ilkd.key.proof.ProofEvent;
027: import de.uka.ilkd.key.util.Debug;
028:
029: /**
030: * This class is the <em>central</em> facade for computing the specification of a
031: * program. It contains algorithms for and controls the computation of specifications.
032: * <h3>Internals</h3>
033: * Usually, the method {@link
034: * de.uka.ilkd.key.casetool.FunctionalityOnModel#computeSpecification(ReprModelMethod)}
035: * is triggered by the user interface, and will start the
036: * specification construction process and thereby invoke {@link
037: * de.uka.ilkd.key.proof.init.ComputeSpecificationPO} to construct the
038: * specification computation proof obligation. Finally, the whole
039: * system relies on the functionality of this class to
040: * {@link #createSpecificationComputationTerm(JavaBlock,Namespace) construct the
041: * specification computation obligation} initially, and
042: * {@link #computeSpecification(Proof) excerpt the
043: * specification} at the end of the proof attempt.
044: *
045: * @author André Platzer
046: * @version 0.1, 2003-01-28
047: * @version-revision $Revision: 1.16.3.1.2.1.3.1.1.3.2.1 $, $Date: Wed, 17 Jan 2007 20:17:31 +0100 $
048: * @see de.uka.ilkd.key.gui.ComputeSpecificationView
049: * @see de.uka.ilkd.key.casetool.FunctionalityOnModel#computeSpecification(ReprModelMethod)
050: */
051: public class ComputeSpecification {
052: /**
053: * Only remember prestate, implicitly.
054: * Thus use proof obligations like <program> (xpost=x).
055: */
056: public static final int PRESTATE_REMEMBER_IMPLICIT = 0;
057: /**
058: * Use explicit prestate remembrance equations.
059: * Thus use proof obligations like x=xpre ← <program> (xpost=x).
060: */
061: public static final int PRESTATE_REMEMBER_EQUATIONS = 1;
062: /**
063: * Use updates for prestate remembrance.
064: * Thus use proof obligations like {x:=xpre} <program> (xpost=x).
065: */
066: public static final int PRESTATE_REMEMBER_UPDATES = 2;
067: /**
068: * Which variant to use for remembering the prestate of the program
069: * invocation.
070: * @see #PRESTATE_REMEMBER_EQUATIONS
071: * @see #PRESTATE_REMEMBER_UPDATES
072: * @see #PRESTATE_REMEMBER_IMPLICIT
073: */
074: private static int prestateRemember = PRESTATE_REMEMBER_UPDATES;
075: /**
076: * set prestate remember kind by property
077: */
078: static {
079: String property = ComputeSpecification.class.getName()
080: + ".prestateRemember";
081: try {
082: String desc = System.getProperty(property, prestateRemember
083: + "");
084: try {
085: setPrestateRemember(java.lang.Integer.parseInt(desc));
086: } catch (NumberFormatException nonumber) {
087: Debug.out("invalid property setting", property, desc);
088: }
089: } catch (SecurityException nevertheless) {
090: // especially catch SecurityExceptions if we were not allowed to read properties
091: Debug
092: .out("Exception thrown by class ComputeSpecification at getProperty()");
093: } catch (Exception nevertheless) {
094: Debug.out("use default property setting for ", property,
095: nevertheless);
096: }
097: Debug.out("property setting ", property, new Integer(
098: prestateRemember));
099: }
100:
101: /**
102: * Use explicit poststate remember equations
103: * (x1=x1@post & ...& xn=xn@post).
104: * Requires knowledge of the modifies list.
105: */
106: public static final int POSTSTATE_REMEMBER_EQUATIONS = 1;
107: /**
108: * Use state change accumulatorr ^true alias scripted C for remembering
109: * the poststate.
110: * Does not require knowledge of the modifies list.
111: * <code>false</code> for explicit poststate remember terms
112: * (x1=x1@post & ...& xn=xn@post) which requires knowledge of the modifies list.
113: */
114: public static final int POSTSTATE_REMEMBER_STATE_CHANGE_ACCUMULATION = 2;
115:
116: /**
117: * Which variant to use for remembering the poststate of the program
118: * invocation.
119: * @see #POSTSTATE_REMEMBER_EQUATIONS
120: * @see #POSTSTATE_REMEMBER_STATE_CHANGE_ACCUMULATION
121: */
122: private static int poststateRemember = POSTSTATE_REMEMBER_STATE_CHANGE_ACCUMULATION;
123:
124: private static final TermFactory termFactory = TermFactory.DEFAULT;
125:
126: /**
127: * Which variant to use for remembering the prestate of the program
128: * invocation.
129: * @see #PRESTATE_REMEMBER_EQUATIONS
130: * @see #PRESTATE_REMEMBER_UPDATES
131: * @see #PRESTATE_REMEMBER_IMPLICIT
132: */
133: public static final void setPrestateRemember(
134: int prestateRememberMode) {
135: if (PRESTATE_REMEMBER_IMPLICIT <= prestateRememberMode
136: && prestateRememberMode <= PRESTATE_REMEMBER_UPDATES) {
137: prestateRemember = prestateRememberMode;
138: } else {
139: throw new IllegalArgumentException(
140: "illegal prestate remember mode: "
141: + prestateRememberMode);
142: }
143: }
144:
145: public static final int getPrestateRemember() {
146: return prestateRemember;
147: }
148:
149: /**
150: * Which variant to use for remembering the poststate of the program
151: * invocation.
152: * @see #POSTSTATE_REMEMBER_EQUATIONS
153: * @see #POSTSTATE_REMEMBER_STATE_CHANGE_ACCUMULATION
154: */
155: public static final void setPoststateRemember(
156: int poststateRememberMode) {
157: if (POSTSTATE_REMEMBER_EQUATIONS <= poststateRememberMode
158: && poststateRememberMode <= POSTSTATE_REMEMBER_STATE_CHANGE_ACCUMULATION) {
159: poststateRemember = poststateRememberMode;
160: } else {
161: throw new IllegalArgumentException(
162: "illegal poststate remember mode: "
163: + poststateRememberMode);
164: }
165: }
166:
167: public static final int getPoststateRemember() {
168: return poststateRemember;
169: }
170:
171: public ComputeSpecification() {
172:
173: }
174:
175: // term constructor method
176:
177: /**
178: * Creates the term to analyse for computing the specification of
179: * a program. Feeding this term into a proof passed to {@link
180: * #computeSpecification(KeYMediator)}, or {@link
181: * #computeSpecification(Proof)} will result in the specification.
182: * @param program the program of which to compute a specification.
183: * @param programVariables the variables that program possibly modifies.
184: * @return the term required for constructing the specification.
185: */
186: public static Term createSpecificationComputationTerm(
187: JavaBlock program, Namespace programVariables) {
188: // Construct a proof obligation of a form like
189: // x = xpre & y = ypre -> <{program}> (xpost = x & ypost = y)
190: Term precondition = termFactory.createJunctorTerm(Op.TRUE);
191: Term postcondition = termFactory.createJunctorTerm(Op.TRUE);
192:
193: ListOfTerm prestateLocations = SLListOfTerm.EMPTY_LIST;
194: ListOfTerm prestateValues = SLListOfTerm.EMPTY_LIST;
195: for (IteratorOfNamed i = programVariables.elements().iterator(); i
196: .hasNext();) {
197: final ProgramVariable v = (ProgramVariable) i.next();
198: final Term v_term = termFactory.createVariableTerm(v);
199: Debug.out("program variable ", v, v.getKeYJavaType());
200: if ("self".equals(v.name().toString())) {
201: // @xxx currently ignore modifications of object state, so no need to remember
202: } else {
203: final Term vpre = termFactory
204: .createVariableTerm(new LocationVariable(
205: new ProgramElementName(v.name() + "pre"),
206: v.getKeYJavaType()));
207: final Term vpost = termFactory
208: .createVariableTerm(new LocationVariable(
209: new ProgramElementName(v.name()
210: + "post"), v.getKeYJavaType()));
211:
212: if ("result".equals(v.name().toString())) {
213: // ignore result at prestate
214: } else {
215: // prestate = prestate union {v:=vpre}
216: prestateLocations = prestateLocations
217: .append(v_term);
218: prestateValues = prestateValues.append(vpre);
219: // remember prestate of v
220: precondition = termFactory
221: .createJunctorTermAndSimplify(
222: Op.AND,
223: precondition,
224: termFactory
225: .createEqualityTerm(
226: v
227: .sort()
228: .getEqualitySymbol(),
229: termFactory
230: .createVariableTerm(v),
231: vpre));
232: }
233:
234: // construct poststate of v
235: postcondition = termFactory
236: .createJunctorTermAndSimplify(Op.AND,
237: postcondition,
238: termFactory.createEqualityTerm(v.sort()
239: .getEqualitySymbol(), vpost,
240: termFactory
241: .createVariableTerm(v)));
242: }
243: }
244:
245: switch (getPoststateRemember()) {
246: case POSTSTATE_REMEMBER_EQUATIONS:
247: /* already assigned postcondition above */
248: break;
249: case POSTSTATE_REMEMBER_STATE_CHANGE_ACCUMULATION:
250: /* alter already assigned postcondition */
251: postcondition = termFactory.createJunctorTerm(
252: Op.COMPUTE_SPEC_OP, termFactory
253: .createJunctorTerm(Op.TRUE));
254: break;
255: default:
256: throw new IllegalStateException(
257: "illegal kind of poststate remembering terms: "
258: + getPoststateRemember());
259: }
260:
261: final Term diamondTerm = termFactory.createDiamondTerm(program,
262: postcondition);
263: switch (getPrestateRemember()) {
264: case PRESTATE_REMEMBER_IMPLICIT:
265: return diamondTerm;
266:
267: case PRESTATE_REMEMBER_UPDATES:
268: return prestateLocations.size() == 0
269: //@internal createUpdateTerm does not work for empty update lists
270: ? diamondTerm
271: // updates prestate (diamondTerm)
272: : termFactory.createUpdateTerm(prestateLocations
273: .toArray(), prestateValues.toArray(),
274: diamondTerm);
275:
276: case PRESTATE_REMEMBER_EQUATIONS:
277: return termFactory.createJunctorTermAndSimplify(Op.IMP,
278: precondition, diamondTerm);
279: default:
280: throw new IllegalStateException(
281: "illegal kind of prestate remembering terms: "
282: + getPrestateRemember());
283: }
284: }
285:
286: // specification computation
287:
288: /**
289: * Extracts the specification of a program from a failed attempt
290: * to prove its correctness.
291: * Will continue the proof automatically as far as possible.
292: * @param mediatorContainingProof The mediator containing
293: * the specification computation proof as selected proof.
294: * Its proof obligation usually stems from
295: * {@link #createSpecificationComputationTerm(JavaBlock,Namespace)}.
296: */
297: public Term computeSpecification(KeYMediator mediatorContainingProof) {
298: final KeYMediator mediator = mediatorContainingProof;
299: //@internal we could also use a "Future" as synchronization means. Perhaps also a Z modulo 2=1 semaphore.
300: final PersistentCondition proofStopped = new PersistentCondition();
301: mediator.addAutoModeListener(new AutoModeListener() {
302:
303: public void autoModeStarted(ProofEvent param1) {
304: }
305:
306: public void autoModeStopped(ProofEvent param1) {
307: Debug.out("proof finished signalled");
308: proofStopped.signal();
309: }
310: });
311:
312: mediator.getInteractiveProver().startAutoMode();
313:
314: try {
315: // let's wait until the prover finishes
316: proofStopped.waitFor();
317: Debug.out("proof finished heard");
318:
319: return computeSpecification(mediator.getSelectedProof());
320: } catch (InterruptedException interrupt) {
321: Thread.currentThread().interrupt();
322: throw new Error(
323: "cannot compute specification since construction process has been interrupted");
324: }
325: }
326:
327: /**
328: * Extracts the specification of a program from a failed attempt
329: * to prove its correctness.
330: * @preconditions proof has no more applicable inference rules.
331: * @param proof The specification computation proof driven as far as possible.
332: * Its proof obligation usually stems from
333: * {@link #createSpecificationComputationTerm(JavaBlock,Namespace)}.
334: */
335: public Term computeSpecification(Proof proof) {
336: Debug.out("Compute specification:\n");
337: List caseSpecs = new LinkedList();
338: for (IteratorOfGoal i = proof.openGoals().iterator(); i
339: .hasNext();) {
340: Sequent open = i.next().sequent();
341: Term caseSpec = computeSpecification(open);
342: Debug.out("Goal Case", caseSpec);
343: caseSpecs.add(caseSpec);
344: }
345: return createJunctorTermNAry(termFactory
346: .createJunctorTerm(Op.TRUE), Op.AND, caseSpecs
347: .iterator());
348: }
349:
350: /**
351: * Constructs the specification resulting of a single open-goal
352: * sequent.
353: * @internal to be precise, we would have to distinguish pure
354: * first-order open-goals, from open-goals still containing
355: * dynamic logic.
356: */
357: private Term computeSpecification(Sequent seq) {
358: Semisequent ante = seq.antecedent();
359: Debug.out("\nCase ");
360: Term ante2 = createJunctorTermNAry(termFactory
361: .createJunctorTerm(Op.TRUE), Op.AND, ante.iterator());
362: Debug.out("", ante2);
363: Debug.out(" => ");
364: Semisequent succ = seq.succedent();
365: Term succ2 = createJunctorTermNAry(termFactory
366: .createJunctorTerm(Op.FALSE), Op.OR, succ.iterator());
367: Debug.out("", succ2);
368:
369: return termFactory.createJunctorTermAndSimplify(Op.IMP, ante2,
370: succ2);
371: }
372:
373: // trivial helper methods
374:
375: /**
376: * Explicit n-ary-fied version of {@link
377: * de.uka.ilkd.logic.TermFactory#createJunctorTerm(Junctor,Term[])}.
378: * @see orbital.logic.functor.Functionals#foldRight
379: * @internal almost identical to @see #createJunctorTermNAry(Term,Junctor,IteratorOfTerm)
380: */
381: private static final Term createJunctorTermNAry(Term c, Junctor op,
382: IteratorOfConstrainedFormula i) {
383: Term construct = c;
384: while (i.hasNext()) {
385: ConstrainedFormula f = i.next();
386: Term t = f.formula();
387: // ignore tautological constraints, since they do not contribute to the specification
388: // but report others
389: if (!f.constraint().isBottom())
390: throw new IllegalArgumentException(
391: "there is a non-tautological constraint on "
392: + f + ". lower constraints, first");
393: construct = termFactory.createJunctorTermAndSimplify(op,
394: construct, t);
395: }
396: return construct;
397: }
398:
399: /**
400: * Explicit n-ary-fied version of {@link
401: * de.uka.ilkd.logic.TermFactory#createJunctorTerm(Junctor,Term[])}.
402: * @see orbital.logic.functor.Functionals#foldRight
403: */
404: private static final Term createJunctorTermNAry(Term c, Junctor op,
405: Iterator i) {
406: Term construct = c;
407: while (i.hasNext()) {
408: construct = termFactory.createJunctorTermAndSimplify(op,
409: construct, (Term) i.next());
410: }
411: return construct;
412: }
413: }// ComputeSpecification
|