See: Description
Interface | Description |
---|---|
ComplexRuleJustification | |
ProofEnvironmentListener | |
RuleJustification | |
TaskTreeNode |
Class | Description |
---|---|
AxiomJustification | |
BasicTask |
Captures a node in the TaskTree which contains exactly one
proof.
|
ComplexRuleJustificationBySpec | |
EnvNode | |
LemmaJustification |
RuleJustification for taclets, that can be proven from other taclets. |
ProofAggregateTask | |
ProofCorrectnessMgt | |
ProofEnvironment |
The unique environment a proof is performed in.
|
ProofEnvironmentEvent | |
RuleJustificationByAddRules | |
RuleJustificationBySpec | |
RuleJustificationInfo | |
SpecificationRepository |
Central storage for all specification elements, such as contracts, class
axioms, and loop invariants.
|
TaskTreeModel |
Enum | Description |
---|---|
ProofStatus |