Skip navigation links

KeY JavaDoc (2.10.0) -- 20211223

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.colors  
de.uka.ilkd.key.gui.configuration
This package contains classes to do with the configuration / settings of KeY.
de.uka.ilkd.key.gui.docking  
de.uka.ilkd.key.gui.extension  
de.uka.ilkd.key.gui.extension.api  
de.uka.ilkd.key.gui.extension.impl  
de.uka.ilkd.key.gui.fonticons  
de.uka.ilkd.key.gui.help  
de.uka.ilkd.key.gui.join  
de.uka.ilkd.key.gui.keyshortcuts  
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.originlabels  
de.uka.ilkd.key.gui.proofdiff  
de.uka.ilkd.key.gui.prooftree  
de.uka.ilkd.key.gui.settings
This package provides a facility for a settings UI.
de.uka.ilkd.key.gui.smt
This package contains the graphical user interface of the SMT backend.
de.uka.ilkd.key.gui.smt.settings  
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 Operators which represent algebraic data type functions.
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.nparser  
de.uka.ilkd.key.nparser.builder  
de.uka.ilkd.key.nparser.varexp  
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.consistency  
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.communication
This package contains the classes and interfaces to create the external SMT solver processes and communicate with them: ExternalProcessLauncher creates and starts the external process and connects it to the pipe. Pipe is responsible for sending and receiving input/output strings to/from the external process.
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.newsmt2  
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.njml
This package provides the functionalities of parsing JML comments into KeY constructs.
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.parsing  
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.removegenerics  
de.uka.ilkd.key.util.removegenerics.monitor  
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  
org.key_project.example  
org.key_project.exploration  
org.key_project.exploration.actions  
org.key_project.exploration.ui  
org.key_project.ui  
org.key_project.ui.interactionlog  
org.key_project.ui.interactionlog.algo  
org.key_project.ui.interactionlog.api  
org.key_project.ui.interactionlog.model  
org.key_project.ui.interactionlog.model.builtin  
org.key_project.ui.markdown  
org.key_project.util  
org.key_project.util.bean  
org.key_project.util.bitops  
org.key_project.util.collection  
org.key_project.util.helper  
org.key_project.util.java  
org.key_project.util.java.thread  
org.key_project.util.lookup  
org.key_project.util.reflection  
org.key_project.util.testcategories
This file defines the different test categories.
recoder.service  
Skip navigation links

Copyright © 2003-2019 The KeY-Project.