Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
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.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.io |
Classes related to loading and saving proof files.
|
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.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.metaconstruct.arith |
contains classes representing the special meta constructs of
Taclet s performing arithmetic operations. |
de.uka.ilkd.key.testgen |
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
ContextStatementBlockInstantiation
this class is created if the scheme given by a context term has
matched to a java program.
|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
SVInstantiations.UpdateLabelPair |
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
ContextInstantiationEntry
This class is used to store the information about a matched
context of a dl formula.
|
GenericSortCondition
Abstract superclass for conditions controlling the instantiations
of generic sorts
|
GenericSortInstantiations
This class handles the instantiation of generic sorts (used for
generic taclets), i.e.
|
IllegalInstantiationException
this exception is thrown if an invalid instantiation for a schema
variable was given
|
InstantiationEntry
This is an abstract class that encapsulates an instantiation of a SchemaVariable.
|
ProgramList |
ProgramSVEntry
this class encapsulates a SchemaVariable and its corresponding
instantiation if it is a JavaProgramElement.
|
ProgramSVInstantiation
this class wrapps a ImmMap
|
SortException
this exception is thrown from an "SVInstantiations"-Object if the
sorts of a schema variable and its instantiation are not compatible
(and not generic)
|
SVInstantiations
This class wraps a ImmMap
|
SVInstantiations.UpdateLabelPair |
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Class and Description |
---|
SVInstantiations
This class wraps a ImmMap
|
Copyright © 2003-2019 The KeY-Project.