Skip navigation links
KeY 2.7.1589_4abe0e7c170fc61dd74a695a6efcf763b0f06898

KeY API Documentation 2.7.1589_4abe0e7c170fc61dd74a695a6efcf763b0f06898

Packages 
Package Description
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
This package contains RecodeR
de.uka.ilkd.key.java.recoderext.expression.literal  
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  
Skip navigation links
KeY 2.7.1589_4abe0e7c170fc61dd74a695a6efcf763b0f06898