de.uka.ilkd.key.informationflow.macros

Class FullInformationFlowAutoPilotMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.DoWhileFinallyMacro

de.uka.ilkd.key.informationflow.macros.FullInformationFlowAutoPilotMacro

All Implemented Interfaces:

ProofMacro

public class FullInformationFlowAutoPilotMacro
extends DoWhileFinallyMacro

Nested Class Summary

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

ProofMacro.ProgressBarListener

Field Summary

Fields

Modifier and Type	Field and Description
private static int	NUMBER_OF_TRY_STEPS The number of proof steps that should be run by the TryCloseMacro before retracting.

Constructor Summary

Constructors

Constructor and Description
FullInformationFlowAutoPilotMacro()

Method Summary

Modifier and Type	Method and Description
boolean	canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc) Can this macro be applied on the given goals?
protected ProofMacro	getAltProofMacro() Gets the alternative proof macro for the else-branch.
java.lang.String	getCategory() Gets the category of this macro.
protected boolean	getCondition()
java.lang.String	getDescription() Gets the description of this macro.
java.lang.String	getName() Gets the name of this macro.
protected ProofMacro	getProofMacro() Gets the proof macro.
java.lang.String	getScriptCommandName() Gets a unique short name for this macro that can be used in proof scripts.

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

applyTo

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

applyTo, canApplyTo, getMaxSteps, hasParameter, resetParams, setParameter

Methods inherited from class java.lang.Object

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

Field Detail

NUMBER_OF_TRY_STEPS

private static final int NUMBER_OF_TRY_STEPS

The number of proof steps that should be run by the TryCloseMacro before retracting. This overrides the strategy setting if set to a value greater or equal to 0.

See Also:

Constant Field Values

Constructor Detail

FullInformationFlowAutoPilotMacro

public FullInformationFlowAutoPilotMacro()

Method Detail

getName

public java.lang.String getName()

Description copied from interface: ProofMacro

Gets the name of this macro. Used as menu entry

Specified by:

getName in interface ProofMacro

Overrides:

getName in class DoWhileFinallyMacro

Returns:

a non-null constant string

getCategory

public java.lang.String getCategory()

Description copied from interface: ProofMacro

Gets the category of this macro. Used as name of the menu under which the macro is sorted. Return null if no submenu is to be created.

Returns:

a constant string, or null

getScriptCommandName

public java.lang.String getScriptCommandName()

Description copied from class: AbstractProofMacro

Gets a unique short name for this macro that can be used in proof scripts. If null is returned, the macro cannot be addressed from within scripts. By default, proof macros do not support scripts, thus null is returned.

Specified by:

getScriptCommandName in interface ProofMacro

Overrides:

getScriptCommandName in class AbstractProofMacro

Returns:

null if not supported, or a non-null constant string as the short name

getDescription

public java.lang.String getDescription()

Description copied from interface: ProofMacro

Gets the description of this macro. Used as tooltip.

Specified by:

getDescription in interface ProofMacro

Overrides:

getDescription in class DoWhileFinallyMacro

Returns:

a non-null constant string

getProofMacro

protected ProofMacro getProofMacro()

Description copied from class: DoWhileFinallyMacro

Gets the proof macro.

Specified by:

getProofMacro in class DoWhileFinallyMacro

Returns:

the proofMacro.

getAltProofMacro

protected ProofMacro getAltProofMacro()

Description copied from class: DoWhileFinallyMacro

Gets the alternative proof macro for the else-branch.

Specified by:

getAltProofMacro in class DoWhileFinallyMacro

Returns:

the proofMacro.

getCondition

protected boolean getCondition()

Specified by:

getCondition in class DoWhileFinallyMacro

canApplyTo

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

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.

This compound macro is applicable if and only if the first macro is applicable. If there is no first macro, this is not applicable.

Specified by:

canApplyTo in interface ProofMacro

Overrides:

canApplyTo in class DoWhileFinallyMacro

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