Package de.uka.ilkd.key.logic.label

Interface Summary

Interface	Description
TermLabel	The interface for term labels.
TermLabelFactory<T extends TermLabel>	A factory for creating TermLabel objects.

Class Summary

Class	Description
BlockContractValidityTermLabel	Label attached to the modality of the validity branch of a block contract.
BlockContractValidityTermLabelFactory	A factory for creating BlockContractValidityTermLabel objects.
FormulaTermLabel	Label attached to a predicates for instance in postconditions, loop invariants or precondition checks of applied operation contracts.
FormulaTermLabelFactory	A factory for creating FormulaTermLabel objects.
ParameterlessTermLabel	The Class ParameterlessTermLabel can be used to define labels without parameters.
SingletonLabelFactory<T extends TermLabel>	A factory for creating singleton TermLabel.
SymbolicExecutionTermLabel	Label attached to a symbolic execution thread.
SymbolicExecutionTermLabelFactory	A factory for creating SymbolicExecutionTermLabel objects.
TermLabelManager	This class provides access to the functionality of term labels.
TermLabelManager.RefactoringsContainer	Utility class used by TermLabelManager#computeRefactorings( TermLabelState, TermServices, PosInOccurrence, Term, Rule, Goal, Term).
TermLabelManager.TermLabelConfiguration	Instances of this class are used to group everything which is required to support one specific TermLabel.
TermLabelOperationsInterpreter	A collection of static methods to deal with TermLabel.
TermLabelState	A TermLabelState is used to share information between participants which manage TermLabels during rule application.

Exception Summary

Exception	Description
TermLabelException	An exception which can be thrown by the term label system.