Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.core | |
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.recoderext | |
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.op |
contains the operators of
Term s. |
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.scripts |
Proof script commands are a simple proof automation facility.
|
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
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.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.conditions | |
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.merge.procedures | |
de.uka.ilkd.key.rule.tacletbuilder | |
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.hierarchy | |
de.uka.ilkd.key.smt.model | |
de.uka.ilkd.key.smt.newsmt2 | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.strategy.feature | |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.strategy.termfeature | |
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.rule | |
de.uka.ilkd.key.symbolic_execution.util | |
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.util |
This package is a grab bag of miscellaneous useful code fragments.
|
de.uka.ilkd.key.util.mergerule |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
ProgramSVSort
Special "sorts" used for schema variables matching program constructs
(class ProgramSV).
|
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
GenericSort
Sort used for generic taclets
Within an SVInstantiations-object a generic sort is instantiated by
a concrete sort, which has to be a subsort of the instantiations of
the supersorts of this sort
|
ProgramSVSort
Special "sorts" used for schema variables matching program constructs
(class ProgramSV).
|
Sort |
Class and Description |
---|
AbstractSort
Abstract base class for implementations of the Sort interface.
|
ArraySort
The objects of this class represent array sorts (in the sense of *Java*
arrays).
|
GenericSupersortException
this exception is thrown if a generic sort has been declared with
an illegal supersort
|
ProgramSVSort
Special "sorts" used for schema variables matching program constructs
(class ProgramSV).
|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
GenericSort
Sort used for generic taclets
Within an SVInstantiations-object a generic sort is instantiated by
a concrete sort, which has to be a subsort of the instantiations of
the supersorts of this sort
|
Sort |
Class and Description |
---|
GenericSort
Sort used for generic taclets
Within an SVInstantiations-object a generic sort is instantiated by
a concrete sort, which has to be a subsort of the instantiations of
the supersorts of this sort
|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
GenericSort
Sort used for generic taclets
Within an SVInstantiations-object a generic sort is instantiated by
a concrete sort, which has to be a subsort of the instantiations of
the supersorts of this sort
|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Class and Description |
---|
Sort |
Copyright © 2003-2019 The KeY-Project.