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. |
OriginTermLabel |
An
OriginTermLabel saves a term's origin in the JML specification
(OriginTermLabel.getOrigin() ) as well as the origins of all of its subterms and former
subterms (OriginTermLabel.getSubtermOrigins() ). |
OriginTermLabel.FileOrigin |
Origin for terms that originate from a file.
|
OriginTermLabel.NodeOrigin |
Origin for terms that originate from a proof node.
|
OriginTermLabel.Origin |
An origin encapsulates some information about where a term originates from.
|
OriginTermLabelFactory |
Factory for
OriginTermLabel s. |
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 . |
TermLabelState |
A
TermLabelState is used to share information between participants
which manage TermLabel s during rule application. |
Enum | Description |
---|---|
OriginTermLabel.SpecType |
A
SpecType is any type of JML specification which gets translated into JavaDL. |
Exception | Description |
---|---|
TermLabelException |
An exception which can be thrown by the term label system.
|
Copyright © 2003-2019 The KeY-Project.