public abstract class AbstractFinishAuxiliaryComputationMacro extends AbstractProofMacro
ProofMacro.ProgressBarListener
Constructor and Description |
---|
AbstractFinishAuxiliaryComputationMacro() |
Modifier and Type | Method and Description |
---|---|
protected static void |
addContractApplicationTaclets(Goal initiatingGoal,
Proof symbExecProof) |
private static Term[] |
buildExecution(ProofObligationVars c,
java.util.Map<Term,Term> vsMap,
ImmutableList<Goal> symbExecGoals,
Goal initGoal) |
private static Term |
buildFormulaFromGoal(Goal symbExecGoal) |
private static Term[] |
buildFormulasFromGoals(ImmutableList<Goal> symbExecGoals) |
(package private) static Term |
calculateResultingTerm(Proof proof,
IFProofObligationVars ifVars,
Goal initGoal) |
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, canApplyTo, getMaxSteps, getScriptCommandName, hasParameter, resetParams, setParameter
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
applyTo, canApplyTo
public AbstractFinishAuxiliaryComputationMacro()
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 stringstatic Term calculateResultingTerm(Proof proof, IFProofObligationVars ifVars, Goal initGoal)
private static Term[] buildExecution(ProofObligationVars c, java.util.Map<Term,Term> vsMap, ImmutableList<Goal> symbExecGoals, Goal initGoal)
private static Term[] buildFormulasFromGoals(ImmutableList<Goal> symbExecGoals)