de.uka.ilkd.key.macros

Class TestGenMacro

java.lang.Object

de.uka.ilkd.key.macros.AbstractProofMacro

de.uka.ilkd.key.macros.StrategyProofMacro

de.uka.ilkd.key.macros.TestGenMacro

All Implemented Interfaces:

ProofMacro

public class TestGenMacro
extends StrategyProofMacro

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	TestGenMacro.TestGenStrategy The Class FilterAppManager is a special strategy assigning to any rule infinite costs if the goal has no modality

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

ProofMacro.ProgressBarListener

Constructor Summary

Constructors

Constructor and Description
TestGenMacro()

Method Summary

Modifier and Type	Method and Description
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.
private static boolean	hasModality(Node node)
private static boolean	hasModality(Term term)

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

applyTo, canApplyTo, doPostProcessing

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

TestGenMacro

public TestGenMacro()

Method Detail

hasModality

private static boolean hasModality(Node node)

hasModality

private static boolean hasModality(Term term)

createStrategy

protected Strategy createStrategy(Proof proof,
                                  PosInOccurrence posInOcc)

Specified by:

createStrategy in class StrategyProofMacro

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

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