de.uka.ilkd.key.informationflow.macros

Class StateExpansionAndInfFlowContractApplicationMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.SequentialProofMacro

de.uka.ilkd.key.informationflow.macros.StateExpansionAndInfFlowContractApplicationMacro

All Implemented Interfaces:

ProofMacro

public class StateExpansionAndInfFlowContractApplicationMacro
extends SequentialProofMacro

Author:

christoph scheben

Nested Class Summary

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

ProofMacro.ProgressBarListener

Constructor Summary

Constructors

Constructor and Description
StateExpansionAndInfFlowContractApplicationMacro()

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[]	createProofMacroArray() Creates the proof macro array.
java.lang.String	getCategory() Gets the category of this macro.
java.lang.String	getDescription() Gets the description of this macro.
java.lang.String	getName() Gets the name of this macro.

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

applyTo, getProofMacros

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

Constructor Detail

StateExpansionAndInfFlowContractApplicationMacro

public StateExpansionAndInfFlowContractApplicationMacro()

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

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

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

createProofMacroArray

protected ProofMacro[] createProofMacroArray()

Description copied from class: SequentialProofMacro

Creates the proof macro array. Override this method by returning an array with the macros you want to call in the order of execution.

Specified by:

createProofMacroArray in class SequentialProofMacro

Returns:

a non-null array which should not be altered afterwards.

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.

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 SequentialProofMacro

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