public class FullAutoPilotWithJMLSpecJoinsProofMacro extends SequentialProofMacro
It is experimental. It performs the following steps:
FullAutoPilotProofMacro
ProofMacro.ProgressBarListener
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 and Description |
---|
FullAutoPilotWithJMLSpecJoinsProofMacro() |
Modifier and Type | Method and Description |
---|---|
protected ProofMacro[] |
createProofMacroArray()
Creates the proof macro array.
|
String |
getCategory()
Gets the category of this macro.
|
String |
getDescription()
Gets the description of this macro.
|
String |
getName()
Gets the name of this macro.
|
applyTo, canApplyTo, getProofMacros
applyTo, canApplyTo, getMaxSteps, getScriptCommandName
private static final int NUMBER_OF_TRY_STEPS
TryCloseMacro
before retracting. This overrides the strategy setting.public FullAutoPilotWithJMLSpecJoinsProofMacro()
public String getName()
ProofMacro
null
constant stringpublic String getCategory()
ProofMacro
null
if no submenu is to be created.null
public String getDescription()
ProofMacro
null
constant stringprotected ProofMacro[] createProofMacroArray()
SequentialProofMacro
createProofMacroArray
in class SequentialProofMacro