Interface | Description |
---|---|
TermLabel |
The interface for term labels.
|
TermLabelFactory<T extends TermLabel> |
A factory for creating TermLabel objects.
|
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 TermLabel s during rule application. |
Exception | Description |
---|---|
TermLabelException |
An exception which can be thrown by the term label system.
|