Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.symbolic_execution.rule | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.ui | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Class and Description |
---|
ProofEnvironment
The unique environment a proof is performed in.
|
SpecificationRepository
Central storage for all specification elements, such as contracts, class
axioms, and loop invariants.
|
Class and Description |
---|
BasicTask
Captures a node in the TaskTree which contains exactly one
proof.
|
ProofEnvironmentListener |
TaskTreeModel |
TaskTreeNode |
Class and Description |
---|
SpecificationRepository
Central storage for all specification elements, such as contracts, class
axioms, and loop invariants.
|
Class and Description |
---|
ProofCorrectnessMgt |
ProofEnvironment
The unique environment a proof is performed in.
|
ProofStatus |
Class and Description |
---|
RuleJustification |
RuleJustificationInfo |
SpecificationRepository
Central storage for all specification elements, such as contracts, class
axioms, and loop invariants.
|
Class and Description |
---|
AxiomJustification |
ComplexRuleJustification |
LemmaJustification
RuleJustification for taclets, that can be proven from other taclets. |
ProofEnvironment
The unique environment a proof is performed in.
|
ProofEnvironmentEvent |
ProofEnvironmentListener |
ProofStatus |
RuleJustification |
RuleJustificationBySpec |
RuleJustificationInfo |
TaskTreeModel |
TaskTreeNode |
Class and Description |
---|
RuleJustification |
SpecificationRepository
Central storage for all specification elements, such as contracts, class
axioms, and loop invariants.
|
Class and Description |
---|
ProofEnvironment
The unique environment a proof is performed in.
|
Class and Description |
---|
ProofEnvironment
The unique environment a proof is performed in.
|
Class and Description |
---|
ProofEnvironment
The unique environment a proof is performed in.
|
Class and Description |
---|
ProofEnvironment
The unique environment a proof is performed in.
|
ProofEnvironmentEvent |
ProofEnvironmentListener |
Class and Description |
---|
ProofEnvironment
The unique environment a proof is performed in.
|
Copyright © 2003-2019 The KeY-Project.