Package de.uka.ilkd.key.proof.mgt

This package contains classes for proof environments and proof management.

See: Description

Interface Summary

Interface	Description
ComplexRuleJustification
ProofEnvironmentListener
RuleJustification
TaskTreeNode

Class Summary

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 Summary

Enum	Description
ProofStatus

Package de.uka.ilkd.key.proof.mgt Description

This package contains classes for proof environments and proof management. For example, proof management ensures that contract applications cannot lead to unsound cyclic dependencies between proofs.