de.uka.ilkd.key.macros

Class DoWhileFinallyMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.DoWhileFinallyMacro

All Implemented Interfaces:

ProofMacro

Direct Known Subclasses:

FullInformationFlowAutoPilotMacro

public abstract class DoWhileFinallyMacro
extends AbstractProofMacro

The abstract class DoWhileFinallyMacro can be used to create compound macros which apply the macro given by getProofMacro() as long the given bound of steps is not reached yet, the condition given by getCondition() holds, and the macro is applicable. When this becomes false and the step bound is not reached yet, the macro given by getAltProofMacro() is applied.

Author:

Michael Kirsten

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.macros.ProofMacro

ProofMacro.ProgressBarListener

Constructor Summary

Constructors

Constructor and Description
DoWhileFinallyMacro()

Method Summary

Modifier and Type	Method and Description
ProofMacroFinishedInfo	applyTo(UserInterfaceControl uic, Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc, ProverTaskListener listener) Apply this macro on the given goals.
boolean	canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc) Can this macro be applied on the given goals?
protected abstract ProofMacro	getAltProofMacro() Gets the alternative proof macro for the else-branch.
protected abstract boolean	getCondition()
java.lang.String	getDescription() Gets the description of this macro.
java.lang.String	getName() Gets the name of this macro.
protected abstract ProofMacro	getProofMacro() Gets the proof macro.

Methods inherited from class de.uka.ilkd.key.macros.AbstractProofMacro

applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.macros.ProofMacro

getCategory

Constructor Detail

DoWhileFinallyMacro

public DoWhileFinallyMacro()

Method Detail

getName

public java.lang.String getName()

Description copied from interface: ProofMacro

Gets the name of this macro. Used as menu entry

Returns:

a non-null constant string

getDescription

public java.lang.String getDescription()

Description copied from interface: ProofMacro

Gets the description of this macro. Used as tooltip.

Returns:

a non-null constant string

canApplyTo

public boolean canApplyTo(Proof proof,
                          ImmutableList<Goal> goals,
                          PosInOccurrence posInOcc)

Description copied from interface: ProofMacro

Can this macro be applied on the given goals? This method should not make any changes but check if the macro can be applied or not on the given goals. This method may be called from within the GUI thread and be compatible with that fact.

Parameters:

proof - the current Proof (not null)

goals - the goals (not null)

posInOcc - the position in occurrence (may be null)

Returns:

true, if the macro is allowed to be applied

applyTo

public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic,
                                      Proof proof,
                                      ImmutableList<Goal> goals,
                                      PosInOccurrence posInOcc,
                                      ProverTaskListener listener)
                               throws java.lang.InterruptedException,
                                      java.lang.Exception

Description copied from interface: ProofMacro

Apply this macro on the given goals. This method can change the proof by applying rules to it. This method is usually called from a dedicated thread and not the GUI thread. The thread it runs on may be interrupted. In this case, the macro may report the interruption by an InterruptedException. A ProverTaskListener can be provided to which the progress will be reported. If no reports are desired, null cna be used for this parameter. If more than one listener is needed, consider combining them using a single listener object using the composite pattern.

Parameters:

uic - the UserInterfaceControl to use

proof - the current Proof (not null)

goals - the goals (not null)

posInOcc - the position in occurrence (may be null)

listener - the listener to use for progress reports (may be null)

Throws:

java.lang.InterruptedException - if the application of the macro has been interrupted.

java.lang.Exception

getProofMacro

protected abstract ProofMacro getProofMacro()

Gets the proof macro.

Returns:

the proofMacro.

getAltProofMacro

protected abstract ProofMacro getAltProofMacro()

Gets the alternative proof macro for the else-branch.

Returns:

the proofMacro.

getCondition

protected abstract boolean getCondition()