public class WellDefinednessMacro extends StrategyProofMacro
WD_PREFIX
.
The macro is only applicable for proof obligations created in #WellDefinednessPO
and the Well-Definedness branches in #WhileInvariantRule
and #BlockContractRule
.Modifier and Type | Class and Description |
---|---|
private static class |
WellDefinednessMacro.WellDefinednessStrategy
This strategy accepts all rule apps for which the rule name is a
Well-Definedness rule and rejects everything else.
|
ProofMacro.ProgressBarListener
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
WD_BRANCH |
static java.lang.String |
WD_PREFIX |
Constructor and Description |
---|
WellDefinednessMacro() |
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 Strategy |
createStrategy(Proof proof,
PosInOccurrence posInOcc) |
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.
|
applyTo, doPostProcessing
applyTo, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
public static final java.lang.String WD_PREFIX
public static final java.lang.String WD_BRANCH
public java.lang.String getName()
ProofMacro
null
constant stringpublic java.lang.String getCategory()
ProofMacro
null
if no submenu is to be created.null
public java.lang.String getDescription()
ProofMacro
null
constant stringprotected Strategy createStrategy(Proof proof, PosInOccurrence posInOcc)
createStrategy
in class StrategyProofMacro
public boolean canApplyTo(Proof proof, ImmutableList<Goal> goals, PosInOccurrence posInOcc)
StrategyProofMacro
canApplyTo
in interface ProofMacro
canApplyTo
in class StrategyProofMacro
proof
- the current Proof
(not null
)goals
- the goals (not null
)posInOcc
- the position in occurrence (may be null
)true
, if the macro is allowed to be applied