Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.informationflow.proof.init | |
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.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.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.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.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.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.proof_references.analyst | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
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.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml | |
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.symbolic_execution.model.impl | |
de.uka.ilkd.key.symbolic_execution.po | |
de.uka.ilkd.key.symbolic_execution.strategy.breakpoint | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.testgen | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
ArrayType
A program model element representing array types.
|
ClassType
A program model element representing class types.
|
Field
A program model element representing fields.
|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Method
A program model element representing methods.
|
PrimitiveType
A program model element representing primitive types.
|
Type
A program model element representing types.
|
Class and Description |
---|
ClassType
A program model element representing class types.
|
ClassTypeContainer
A program model element that may contain class types.
|
Constructor
A program model element representing constructors.
|
Field
A program model element representing fields.
|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Member
A program model element representing members.
|
Method
A program model element representing methods.
|
NullType
A program model element representing the null type.
|
Package
A program model element representing packages.
|
PrimitiveType
A program model element representing primitive types.
|
ProgramModelElement
An entity of the program meta model.
|
Type
A program model element representing types.
|
Variable
A program model element representing variables.
|
Class and Description |
---|
ArrayType
A program model element representing array types.
|
ClassType
A program model element representing class types.
|
ClassTypeContainer
A program model element that may contain class types.
|
Constructor
A program model element representing constructors.
|
Field
A program model element representing fields.
|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Member
A program model element representing members.
|
Method
A program model element representing methods.
|
Package
A program model element representing packages.
|
ProgramModelElement
An entity of the program meta model.
|
Type
A program model element representing types.
|
Variable
A program model element representing variables.
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
Type
A program model element representing types.
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
Type
A program model element representing types.
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Type
A program model element representing types.
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Type
A program model element representing types.
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
PrimitiveType
A program model element representing primitive types.
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Class and Description |
---|
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
Type
A program model element representing types.
|
Copyright © 2003-2019 The KeY-Project.