Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.control | |
de.uka.ilkd.key.core | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.gui.lemmatagenerator | |
de.uka.ilkd.key.gui.mergerule | |
de.uka.ilkd.key.gui.mergerule.predicateabstraction | |
de.uka.ilkd.key.gui.smt |
This package contains the graphical user interface of the SMT backend.
|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.recoderext | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.nparser | |
de.uka.ilkd.key.nparser.builder | |
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.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.proof.io.intermediate | |
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.rule.merge | |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml.pretranslation | |
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.strategy.definition | |
de.uka.ilkd.key.symbolic_execution | |
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.
|
de.uka.ilkd.key.util.mergerule | |
de.uka.ilkd.key.util.rifl |
RIFL is short for "Requirements for Information Flow Language",
a tool-indepentent specification language developed in the RS3 project.
|
Class and Description |
---|
Pair |
Class and Description |
---|
Pair |
ProgressMonitor
An interface to some progress reporting mechanism.
|
Class and Description |
---|
CommandLine
A small framework to handle command lines.
|
Class and Description |
---|
Pair |
ProgressMonitor
An interface to some progress reporting mechanism.
|
XMLResources
An instance of this class loads several XML files, whose contents are
displayed in
InfoView . |
Class and Description |
---|
CommandLine
A small framework to handle command lines.
|
Class and Description |
---|
Pair |
Class and Description |
---|
Pair |
Class and Description |
---|
Pair |
Class and Description |
---|
FileCollection
This class encapsulates a collection of files which is arbitrarily organised.
|
KeYRecoderExcHandler |
Pair |
Class and Description |
---|
KeYRecoderExcHandler |
Class and Description |
---|
Pair |
Class and Description |
---|
Triple |
Class and Description |
---|
Pair |
Class and Description |
---|
InfFlowSpec |
LinkedHashMap |
Pair |
Class and Description |
---|
ProgressMonitor
An interface to some progress reporting mechanism.
|
Triple |
Class and Description |
---|
Pair |
ProgressMonitor
An interface to some progress reporting mechanism.
|
Class and Description |
---|
Pair |
Class and Description |
---|
Pair |
Class and Description |
---|
Pair |
Class and Description |
---|
Triple |
Class and Description |
---|
Pair |
Class and Description |
---|
InfFlowSpec |
Pair |
Triple |
Class and Description |
---|
Triple |
Class and Description |
---|
InfFlowSpec |
Class and Description |
---|
InfFlowSpec |
Pair |
Triple |
Class and Description |
---|
Triple |
Class and Description |
---|
Pair |
ProofStarter
This class encapsulates the registration of a proof for a given problem.
|
Class and Description |
---|
Triple |
Class and Description |
---|
Pair |
ProofStarter
This class encapsulates the registration of a proof for a given problem.
|
Triple |
Class and Description |
---|
ProgressMonitor
An interface to some progress reporting mechanism.
|
Class and Description |
---|
ProgressMonitor
An interface to some progress reporting mechanism.
|
Class and Description |
---|
CommandLineException
Exception used by
CommandLine . |
DebugMBean
This interface provides the class Debug with the possibility
to be administrated from within management tools such as
"jconsole".
|
EnhancedStringBuffer
StringBuffer with more functionality.
|
FileCollection
This class encapsulates a collection of files which is arbitrarily organised.
|
FileCollection.Walker
A Walker allows to iterate (once and one way) through a FileCollection.
|
InfFlowSpec |
KeYResourceManager |
Pair |
Position |
ProgressMonitor
An interface to some progress reporting mechanism.
|
ProgressMonitor.Empty
A progress monitor that does nothing.
|
ProofStarter
This class encapsulates the registration of a proof for a given problem.
|
ProofUserManager
This singleton class is used to manage user of a
Proof to make
sure that a Proof is only disposed via Proof.dispose() if
it is no longer in use (no user available). |
String8
Re-implementation of String using only 8bit encoding
as compared to standard 16bit.
|
Class and Description |
---|
Pair |
Triple |
Class and Description |
---|
KeYRecoderExcHandler |
Copyright © 2003-2019 The KeY-Project.