| de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
| de.uka.ilkd.key.axiom_abstraction |
|
| de.uka.ilkd.key.axiom_abstraction.boollattice |
|
| de.uka.ilkd.key.axiom_abstraction.predicateabstraction |
|
| de.uka.ilkd.key.axiom_abstraction.signanalysis |
|
| de.uka.ilkd.key.control |
|
| de.uka.ilkd.key.control.event |
|
| de.uka.ilkd.key.control.instantiation_model |
|
| 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.actions |
|
| de.uka.ilkd.key.gui.configuration |
This package contains classes to do with the configuration / settings of KeY.
|
| de.uka.ilkd.key.gui.ext |
|
| de.uka.ilkd.key.gui.fonticons |
|
| de.uka.ilkd.key.gui.interactionlog |
|
| de.uka.ilkd.key.gui.interactionlog.algo |
|
| de.uka.ilkd.key.gui.interactionlog.model |
|
| de.uka.ilkd.key.gui.interactionlog.model.builtin |
|
| de.uka.ilkd.key.gui.join |
|
| de.uka.ilkd.key.gui.lemmatagenerator |
|
| de.uka.ilkd.key.gui.mergerule |
|
| de.uka.ilkd.key.gui.mergerule.predicateabstraction |
|
| de.uka.ilkd.key.gui.nodeviews |
|
| de.uka.ilkd.key.gui.notification |
|
| de.uka.ilkd.key.gui.notification.actions |
|
| de.uka.ilkd.key.gui.notification.events |
|
| de.uka.ilkd.key.gui.proofdiff |
|
| de.uka.ilkd.key.gui.prooftree |
|
| de.uka.ilkd.key.gui.smt |
This package contains the graphical user interface of the SMT backend.
|
| de.uka.ilkd.key.gui.sourceview |
|
| de.uka.ilkd.key.gui.testgen |
This package contains the graphical user interface of the test generation backend.
|
| de.uka.ilkd.key.gui.utilities |
|
| de.uka.ilkd.key.informationflow.macros |
|
| de.uka.ilkd.key.informationflow.po |
|
| de.uka.ilkd.key.informationflow.po.snippet |
|
| de.uka.ilkd.key.informationflow.proof |
|
| de.uka.ilkd.key.informationflow.proof.init |
|
| de.uka.ilkd.key.informationflow.rule |
|
| de.uka.ilkd.key.informationflow.rule.executor |
|
| de.uka.ilkd.key.informationflow.rule.tacletbuilder |
|
| de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
| de.uka.ilkd.key.java.abstraction |
This package contains the meta model abstractions as used by the
semantical services.
|
| de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
| de.uka.ilkd.key.java.declaration.modifier |
This package collects all Java modifiers.
|
| de.uka.ilkd.key.java.expression |
Elements of the Java syntax tree representing expressions.
|
| de.uka.ilkd.key.java.expression.literal |
This package contains representations for the various Java literal types.
|
| de.uka.ilkd.key.java.expression.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
| de.uka.ilkd.key.java.expression.operator.adt |
|
| de.uka.ilkd.key.java.recoderext |
|
| de.uka.ilkd.key.java.recoderext.adt |
|
| de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
| de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
| de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
| de.uka.ilkd.key.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
| de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
| de.uka.ilkd.key.logic.label |
|
| de.uka.ilkd.key.logic.op |
contains the operators of Terms. |
| de.uka.ilkd.key.logic.sort |
This package contains different kinds and implementations subtyping interface Sort.
|
| de.uka.ilkd.key.logic.util |
|
| de.uka.ilkd.key.macros |
|
| de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
| de.uka.ilkd.key.macros.scripts.meta |
|
| de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
| de.uka.ilkd.key.parser.proofjava |
|
| de.uka.ilkd.key.parser.schemajava |
|
| de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
| 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_references |
|
| de.uka.ilkd.key.proof_references.analyst |
|
| de.uka.ilkd.key.proof_references.reference |
|
| de.uka.ilkd.key.proof.delayedcut |
|
| de.uka.ilkd.key.proof.event |
|
| 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.event |
|
| de.uka.ilkd.key.proof.io.intermediate |
|
| de.uka.ilkd.key.proof.join |
|
| de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
| de.uka.ilkd.key.proof.proofevent |
|
| de.uka.ilkd.key.proof.rulefilter |
|
| de.uka.ilkd.key.prover |
|
| de.uka.ilkd.key.prover.impl |
|
| de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
| de.uka.ilkd.key.rule.conditions |
|
| de.uka.ilkd.key.rule.executor |
|
| de.uka.ilkd.key.rule.executor.javadl |
|
| de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of Taclets.
|
| de.uka.ilkd.key.rule.label |
|
| de.uka.ilkd.key.rule.match |
|
| de.uka.ilkd.key.rule.match.legacy |
|
| de.uka.ilkd.key.rule.match.vm |
|
| de.uka.ilkd.key.rule.match.vm.instructions |
|
| de.uka.ilkd.key.rule.merge |
|
| de.uka.ilkd.key.rule.merge.procedures |
|
| de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of Taclets.
|
| de.uka.ilkd.key.rule.metaconstruct.arith |
contains classes representing the special meta constructs of Taclets performing arithmetic operations.
|
| de.uka.ilkd.key.rule.tacletbuilder |
|
| de.uka.ilkd.key.settings |
|
| de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
| de.uka.ilkd.key.smt.counterexample |
|
| de.uka.ilkd.key.smt.hierarchy |
|
| de.uka.ilkd.key.smt.lang |
|
| de.uka.ilkd.key.smt.model |
|
| de.uka.ilkd.key.smt.testgen |
|
| de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
| de.uka.ilkd.key.speclang.dl.translation |
|
| de.uka.ilkd.key.speclang.jml |
|
| de.uka.ilkd.key.speclang.jml.pretranslation |
|
| de.uka.ilkd.key.speclang.jml.translation |
|
| de.uka.ilkd.key.speclang.translation |
|
| de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
| de.uka.ilkd.key.strategy.definition |
|
| de.uka.ilkd.key.strategy.feature |
|
| de.uka.ilkd.key.strategy.feature.findprefix |
|
| de.uka.ilkd.key.strategy.feature.instantiator |
|
| de.uka.ilkd.key.strategy.quantifierHeuristics |
|
| de.uka.ilkd.key.strategy.termfeature |
|
| de.uka.ilkd.key.strategy.termgenerator |
|
| de.uka.ilkd.key.strategy.termProjection |
|
| de.uka.ilkd.key.symbolic_execution |
|
| de.uka.ilkd.key.symbolic_execution.model |
|
| de.uka.ilkd.key.symbolic_execution.model.impl |
|
| de.uka.ilkd.key.symbolic_execution.object_model |
|
| de.uka.ilkd.key.symbolic_execution.object_model.impl |
|
| de.uka.ilkd.key.symbolic_execution.po |
|
| de.uka.ilkd.key.symbolic_execution.profile |
|
| de.uka.ilkd.key.symbolic_execution.rule |
|
| de.uka.ilkd.key.symbolic_execution.slicing |
|
| de.uka.ilkd.key.symbolic_execution.strategy |
|
| de.uka.ilkd.key.symbolic_execution.strategy.breakpoint |
|
| de.uka.ilkd.key.symbolic_execution.util |
|
| de.uka.ilkd.key.symbolic_execution.util.event |
|
| de.uka.ilkd.key.taclettranslation |
|
| de.uka.ilkd.key.taclettranslation.assumptions |
|
| de.uka.ilkd.key.taclettranslation.lemma |
|
| de.uka.ilkd.key.testgen |
|
| de.uka.ilkd.key.testgen.oracle |
|
| 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.net |
|
| de.uka.ilkd.key.util.pp |
A package to pretty-print information using line breaks and
indentation.
|
| de.uka.ilkd.key.util.properties |
|
| 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.
|
| org.key_project.util |
|
| org.key_project.util.bean |
|
| org.key_project.util.bitops |
|
| org.key_project.util.collection |
|
| org.key_project.util.java |
|
| org.key_project.util.java.thread |
|
| org.key_project.util.reflection |
|
| recoder.service |
|