| Package Name | Comment |
| de.uka.ilkd.key | |
| de.uka.ilkd.key.casetool | |
| de.uka.ilkd.key.casetool.eclipse | |
| de.uka.ilkd.key.casetool.patternimplementor | |
| de.uka.ilkd.key.casetool.patternimplementor.patterns | |
| de.uka.ilkd.key.casetool.together | |
| de.uka.ilkd.key.casetool.together.keydebugclassloader | |
| de.uka.ilkd.key.casetool.together.patterns.HelperClasses.MyParser | |
| de.uka.ilkd.key.casetool.together.patterns.HelperClasses.MyPatternBase | |
| de.uka.ilkd.key.casetool.together.patterns.JAVA.CLASS.KeY_GoF.Composite | |
| de.uka.ilkd.key.casetool.together.patterns.JAVA.CLASS.KeY_GoF.Decorator | |
| de.uka.ilkd.key.casetool.together.patterns.JAVA.CLASS.KeY_GoF.Observer | |
| de.uka.ilkd.key.casetool.together.patterns.JAVA.CLASS.KeY_Idiom.InvariantConstraints | |
| de.uka.ilkd.key.casetool.together.patterns.JAVA.MEMBER.KeY_Idiom.MethSpecConstraints | |
| de.uka.ilkd.key.casetool.together.scripts.menuextension | |
| de.uka.ilkd.key.casetool.together.scripts.patternmechanism | |
| de.uka.ilkd.key.casetool.together.scripts.patternupdate | |
| de.uka.ilkd.key.casetool.together.scripts.probe.helloworldcall | |
| de.uka.ilkd.key.collection | |
| de.uka.ilkd.key.counterexample | |
| de.uka.ilkd.key.cspec |
Contains classes for computing the specification of a program
Contains classes for computing the specification of a program.
This package is responsible for the inverse process of inferring the
specification of a program from its source code.
|
| de.uka.ilkd.key.gui | |
| de.uka.ilkd.key.gui.assistant | |
| de.uka.ilkd.key.gui.configuration | |
| 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.prooftree | |
| de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
The classes in the subpackages are mainly taken from the Recoder
framework and made immutable. They are transformed into this data
structure from a Recoder structure by {@link
de.uka.ilkd.key.java.Recoder2KeY} or {@link
de.uka.ilkd.key.SchemaRecoder2KeY}. However, in some details both
data structures might differ more.
The following explanations are adapted from the
documentation of the Recoder framework.
- Source and Program Elements
-
A {@link de.uka.ilkd.key.java.SourceElement} is a syntactical entity and not
necessary a {@link de.uka.ilkd.key.java.ModelElement}, such as a {@link de.uka.ilkd.key.java.Comment}.
A {@link de.uka.ilkd.key.java.ProgramElement} is a {@link de.uka.ilkd.key.java.SourceElement}
and a {@link de.uka.ilkd.key.ModelElement}. It is aware of its parent in the syntax
tree, while a pure {@link de.uka.ilkd.key.java.SourceElement} is not considered as a
member of the AST even though it is represented in the sources.
{@link de.uka.ilkd.key.java.ProgramElement}s are further
classified into {@link de.uka.ilkd.key.java.TerminalProgramElement}s and
{@link de.uka.ilkd.key.java.NonTerminalProgramElement}s. While {@link de.uka.ilkd.key.java.TerminalProgramElement}
is just a tag class, {@link de.uka.ilkd.key.java.NonTerminalProgramElement}s know
their AST children (while it is possible that they do not have any).
A complete source file occurs as a {@link de.uka.ilkd.key.java.CompilationUnit}.
{@link de.uka.ilkd.key.java.JavaSourceElement} and
{@link de.uka.ilkd.key.java.JavaProgramElement} are abstract classes defining
standard implementations that already know their
{@link de.uka.ilkd.key.java.JavaProgramFactory}.
- Expressions and Statements
-
{@link de.uka.ilkd.key.java.Expression} and {@link de.uka.ilkd.key.java.Statement} are
self-explanatory. A {@link de.uka.ilkd.key.java.LoopInitializer} is a special
{@link de.uka.ilkd.key.java.Statement} valid as initializer of
{@link de.uka.ilkd.key.java.statement.For} loops.
{@link de.uka.ilkd.key.java.LoopInitializer} is subtyped by
{@link de.uka.ilkd.key.java.expression.ExpressionStatement} and
{@link de.uka.ilkd.key.java.declaration.LocalVariableDeclaration}).
Concrete classes and further abstractions are bundled in the
{@link de.uka.ilkd.key.java.expression} and {@link de.uka.ilkd.key.java.statement} packages.
- Syntax Tree Parents
-
There are a couple of abstractions dealing with properties of being a
parent node.
These are {@link de.uka.ilkd.key.java.declaration.TypeDeclarationContainer},
{@link de.uka.ilkd.key.java.ExpressionContainer},
{@link de.uka.ilkd.key.java.StatementContainer},
{@link de.uka.ilkd.key.java.ParameterContainer},
{@link de.uka.ilkd.key.java.NamedProgramElement} and
{@link de.uka.ilkd.key.java.reference.TypeReferenceContainer}. A
An {@link de.uka.ilkd.key.java.ExpressionContainer} contains
{@link de.uka.ilkd.key.java.Expression}s, a
{@link de.uka.ilkd.key.java.StatementContainer} contains
{@link de.uka.ilkd.key.java.Statement}s, a
{@link de.uka.ilkd.key.java.ParameterContainer}
(either a {@link de.uka.ilkd.key.java.declaration.MethodDeclaration} or a
{@link de.uka.ilkd.key.java.statement.Catch} statement) contains
{@link de.uka.ilkd.key.java.declaration.ParameterDeclaration}s.
A {@link de.uka.ilkd.key.java.NamedProgramElement} is a subtype of
{@link de.uka.ilkd.key.NamedModelElement}.
A {@link de.uka.ilkd.key.java.reference.TypeReferenceContainer} contains one or
several names, but these are names of types that are referred to explicitely
by a {@link de.uka.ilkd.key.java.reference.TypeReference}.
- References
-
A {@link de.uka.ilkd.key.java.Reference} is an explicite use of an entity. Most of
these {@link de.uka.ilkd.key.java.Reference}s are
{@link de.uka.ilkd.key.java.reference.NameReference}s
and as such {@link de.uka.ilkd.key.java.NamedProgramElement}s, e.g. the
{@link de.uka.ilkd.key.java.reference.TypeReference}.
Subtypes of {@link de.uka.ilkd.key.java.Reference}s are bundled in the
{@link de.uka.ilkd.key.java.reference} package.
- Modifiers and Declarations
-
{@link de.uka.ilkd.key.java.declaration.Modifier}s are (exclusively) used in the
context of {@link de.uka.ilkd.key.java.Declaration}s.
{@link de.uka.ilkd.key.java.declaration.Modifier}s occur explictely, since they occur
as syntactical tokens that might be indented and commented.
{@link de.uka.ilkd.key.java.Declaration}s are either
declarations of types or other entities such as
{@link de.uka.ilkd.key.java.declaration.MemberDeclaration} or
{@link de.uka.ilkd.key.java.declaration.VariableDeclaration}. Concrete
{@link de.uka.ilkd.key.java.declaration.Modifier}s and
{@link de.uka.ilkd.key.java.Declaration}s are
bundled in the {@link de.uka.ilkd.key.java.declaration.modifier} and
{@link de.uka.ilkd.key.java.declaration} packages.
|
| de.uka.ilkd.key.java.abstraction |
This package contains the meta model abstractions as used by the
semantical services. The {@link recoder.abstraction.ProgramModelElement}s
hide the origin of the information, be it from Java source code,
Java byte code, or predefined lacking any syntactical representation.
There are three implicitly defined entities -
{@link recoder.abstraction.ArrayType},
{@link recoder.abstraction.DefaultConstructor}, and
{@link recoder.abstraction.Package}, as well as the predefined
types {@link recoder.abstraction.NullType} and the base class for
the small number of {@link recoder.abstraction.PrimitiveType}s.
{@link recoder.abstraction.Scope}s are attached to
{@link recoder.abstraction.ScopeDefiningElement}s by
{@link recoder.service.SourceInfo} implementations and should
not be modified from others.
|
| de.uka.ilkd.key.java.annotation | |
| de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
For each declaration, there exists a corresponding
{@link recoder.java.Reference} in the {@link recoder.java.reference}
package.
Each {@link recoder.java.Declaration}
provides some convenience methods that query the possible modifiers.
The modifiers themselves are collected in the subpackage
{@link recoder.java.declaration.modifier}.
|
| de.uka.ilkd.key.java.declaration.modifier |
This package collects all Java modifiers. The sole abstraction beneath
the parent {@link recoder.java.declaration.Modifier} is the
{@link recoder.java.declaration.modifier.VisibilityModifier}.
|
| de.uka.ilkd.key.java.expression |
Elements of the Java syntax tree representing expressions.
The various operators and literals are bundled in the corresponding
subpackages.
|
| de.uka.ilkd.key.java.expression.literal |
This package contains representations for the various Java literal types.
Quite special are the non-primitive
{@link recoder.java.expression.literal.NullLiteral} and
{@link recoder.java.expression.literal.StringLiteral}.
|
| de.uka.ilkd.key.java.expression.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
{@link recoder.java.expression.operator.New} is also considered an
operator ({@link recoder.java.expression.operator.TypeOperator}).
|
| de.uka.ilkd.key.java.recoderext | |
| 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.
Besides these other valid statements are the various expressions with
side effects ({@link recoder.java.expression.ExpressionStatement}s).
|
| de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
Last modified: Tue Nov 26 08:54:55 MET 2002
|
| de.uka.ilkd.key.javacard | |
| de.uka.ilkd.key.jml | |
| de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure. The structure of a term is defined in {@link
de.uka.ilkd.key.logic.Term}. Subclasses of {@link
de.uka.ilkd.key.logic.Term} provide representations for special
kinds of terms. However, these subclasses are supposed to be not
directly accessed. Instead, {@link de.uka.ilkd.key.logic.Term}
provides methods for all the methods of the
subclasses. Moreover, {@link de.uka.ilkd.key.logic.Term}s (or
their subclasses) are supposed to be never constructed by
constructors of their own, but by instances of {@link
de.uka.ilkd.key.logic.TermFactory}.
The function of {@link de.uka.ilkd.key.logic.Term}s (e.g., if
they represent a conjunction of subterms, a quantified
formula,...) is only determined by an {@link
de.uka.ilkd.key.logic.op.Operator} that is assigned to a {@link
de.uka.ilkd.key.logic.Term} when the {@link
de.uka.ilkd.key.logic.Term} is constructed.
{@link de.uka.ilkd.key.logic.Sequent}s consist of two {@link
de.uka.ilkd.key.logic.Semisequent}s which represent a
duplicate-free list of a {@link
de.uka.ilkd.key.logic.ConstrainedFormula}s. The latter consist of
a {@link de.uka.ilkd.key.logic.Constraint} and a {@link
de.uka.ilkd.key.logic.Term} of a special sort {@link
de.uka.ilkd.key.logic.sort.Sort#FORMULA}.
{@link de.uka.ilkd.key.logic.Sequent}s and {@link
de.uka.ilkd.key.logic.Term}s are immutable.
Last modified: Wed Dec 4 15:11:14 MET 2002
|
| de.uka.ilkd.key.logic.ldt |
contains the language data types for integer arithmetic, the Java boolean and Object type.
Last modified: Tue Nov 26 08:54:55 MET 2002
|
| de.uka.ilkd.key.logic.op |
contains the operators of {@link
de.uka.ilkd.key.logic.Term}s. Operators may be {@link
de.uka.ilkd.key.logic.op.Quantifier}s or {@link
de.uka.ilkd.key.logic.op.SubstOp}s that bind variables for
subterms, but also {@link de.uka.ilkd.key.logic.op.Modality}s, or
{@link de.uka.ilkd.key.logic.op.QuanUpdateOperator}s. Many of the operators
are constantly defined in {@link de.uka.ilkd.key.logic.op.Op}s.
An operator can be a {@link de.uka.ilkd.key.logic.op.TermSymbol}s,
such as a {@link de.uka.ilkd.key.logic.op.Function} or a
variable. There are several kind of variables: {@link
de.uka.ilkd.key.logic.op.LogicVariable}s (variables that must be
bound but do not occur in programs), {@link
de.uka.ilkd.key.logic.op.ProgramVariable}s (allowed both in
programs and in logic, but not boundable), {@link
de.uka.ilkd.key.logic.op.Metavariable}s, and {@link
de.uka.ilkd.key.logic.op.SchemaVariable}s for {@link
de.uka.ilkd.key.rule.Taclet}s.
Last modified: Mon Apr 18 09:42:36 MEST 2005
|
| de.uka.ilkd.key.logic.op.oclop |
Used for OCL Simplification, i.e. not for usual logic terms.
The operators in this package
makes it possible to build OCL expressions in the form of
{@link de.uka.ilkd.key.logic.Term}s, with the ultimate goal of
applying simplification taclets to these {@link de.uka.ilkd.key.logic.Term}s
and then pretty-print the simplified expressions back to usual
OCL syntax again.
Most of the pre-defined OCL operations can be expressed using
{@link de.uka.ilkd.key.logic.op.Function}, but some of them
need more complex operators. These more complex
operators are collected in this package. There is also in this
package a class {@link de.uka.ilkd.key.logic.op.oclop.OclOp} containing
all pre-defined OCL operations, also the ones based on
{@link de.uka.ilkd.key.logic.op.Function}, in form of constants.
The operators defined in this package all extend
{@link de.uka.ilkd.key.logic.op.TermSymbol}.
One thing that makes {@link de.uka.ilkd.key.logic.op.Function}
inappropriate to use for some OCL operations is the fact
that it assumes that the type/sort of a term is only dependent
on its top-level operator, while in OCL the type of an
expression can also depend on its sub expressions. For example:
collection->iterate(elem ; acc:T=init_expr | expr_with_elem_and_acc)
The type of this expression is determined by the type of the
accumulator acc.
Last modified: Thu Jan 27 10:13:36 MET 2005
|
| de.uka.ilkd.key.logic.sort |
This package contains different kinds and implementations subtyping interface Sort.
Each logic term has an assigned a sort. In order to support special concepts like
arrays, objects, primitive types, it is useful to support different kinds of sorts.
This allows to distinguish diffent categories of terms by looking on the sort type
rather than on the name.
In KeY we distinguish formulas from terms by the special sort instance
Sort.Formula.
Last modified: Tue Nov 26 08:54:55 MET 2002
|
| de.uka.ilkd.key.logic.sort.oclsort |
Used for OCL Simplification, i.e. not for usual logic terms.
Instead of creating the sorts in this package directly,
use the constants defined in
{@link de.uka.ilkd.key.logic.sort.oclsort.OclSort}.
This package contains representations of the pre-defined types
in OCL: OclAny, OclType, Boolean, Real,
Integer, String.
It also contains means to represent the pre-defined Collection
types: Collection(T), Set(T), Bag(T),
and Sequence(T), where
T is one of the types enumerated above.
Moreover, we need a type that represents the classifiers
defined in the UML model associated with a specific OCL constraint.
We call this representation {@link de.uka.ilkd.key.logic.sort.oclsort.ClassifierSort}.
This sort can be
viewed as a super type of all classifiers in the model.
We don't need more specific type information of the classifiers,
since our simplification rules are based only on our knowledge
of the pre-defined OCL operations - not the properties of a
specific UML model.
Finally, to be able to check for type conformance when building
OCL expressions, we need a sort called
{@link de.uka.ilkd.key.logic.sort.oclsort.OclGenericSort}. Its existence
is motivated in the context of assigning an element type to
an empty Collection. The problem is that when we, for instance,
build an expression like collection->forAll(s:T | e(s))
we want to check that the element type of collection conforms
to the type T. This must hold also for the special case:
Set{}->forAll(s:T | e(s)). In other words, the element type of
Set{} must conform to every other basic type. At the same time,
when we build a collection, we want to check that the types of
the elements in the collection conforms to the element type of
the collection. Using the taclet syntax, $insert_set(elem, $empty_set),
we want to check that the type of elem conforms to the element
type of $empty_set/Set{}. In other words, the element type of
Set{} must be such that any other basic type conforms to it.
We therefore need a type with the property that it conforms to
any other basic type, and any other basic type conforms to it.
{@link de.uka.ilkd.key.logic.sort.oclsort.OclGenericSort} has this property.
Last modified: Thu Jan 27 15:20:36 MET 2005
|
| de.uka.ilkd.key.logic.util | |
| de.uka.ilkd.key.ocl | |
| de.uka.ilkd.key.ocl.gf | |
| de.uka.ilkd.key.parser | |
| de.uka.ilkd.key.parser.jml | |
| de.uka.ilkd.key.parser.ocl | |
| de.uka.ilkd.key.pp | |
| de.uka.ilkd.key.proof | |
| de.uka.ilkd.key.proof.decproc | |
| de.uka.ilkd.key.proof.decproc.smtlib | |
| de.uka.ilkd.key.proof.decproc.translation | |
| de.uka.ilkd.key.proof.examples | |
| de.uka.ilkd.key.proof.incclosure | |
| de.uka.ilkd.key.proof.init | |
| de.uka.ilkd.key.proof.mgt | |
| de.uka.ilkd.key.proof.proofevent | |
| de.uka.ilkd.key.proof.reuse | |
| de.uka.ilkd.key.rule |
contains classes for implementing rules. For now, there are only
taclet rules, represented by {@link
de.uka.ilkd.key.rule.Taclet}. The package includes the
representation of applications of taclets ({@link
de.uka.ilkd.key.rule.TacletApp}) and the builders of taclets ({@link
de.uka.ilkd.key.rule.TacletBuilder}).
Last modified: Tue Nov 26 08:54:55 MET 2002
|
| de.uka.ilkd.key.rule.conditions | |
| de.uka.ilkd.key.rule.encapsulation | |
| de.uka.ilkd.key.rule.export | |
| de.uka.ilkd.key.rule.export.html | |
| de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of {@link
de.uka.ilkd.key.rule.Taclet}s.
Last modified: Tue Nov 26 08:54:55 MET 2002
|
| de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of {@link
de.uka.ilkd.key.rule.Taclet}s.
Last modified: Tue Nov 26 08:54:55 MET 2002
|
| de.uka.ilkd.key.rule.metaconstruct.arith |
contains classes representing the special meta constructs of {@link
de.uka.ilkd.key.rule.Taclet}s performing arithmetic operations.
Last modified: Tue Nov 26 08:54:55 MET 2002
|
| de.uka.ilkd.key.rule.soundness | |
| de.uka.ilkd.key.rule.updatesimplifier | |
| de.uka.ilkd.key.speclang | |
| de.uka.ilkd.key.speclang.jml | |
| de.uka.ilkd.key.speclang.ocl | |
| de.uka.ilkd.key.strategy | |
| de.uka.ilkd.key.strategy.feature | |
| 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.unittest | |
| de.uka.ilkd.key.unittest.cogent | |
| de.uka.ilkd.key.unittest.simplify | |
| de.uka.ilkd.key.unittest.simplify.ast | |
| de.uka.ilkd.key.util | |
| de.uka.ilkd.key.util.install | |
| de.uka.ilkd.key.util.keydoc.html | |
| de.uka.ilkd.key.util.make | |
| de.uka.ilkd.key.util.pp |
A package to pretty-print information using line breaks and
indentation. For instance, it can be used to print
while (i>0) {
i--;
j++;
}
instead of
while (i>0) { i
--; j++;}
if a maximum line width of 15 characters is chosen. The frontend
to the Pretty-Printer is the {@link
de.uka.ilkd.key.util.pp.Layouter} class. You may configure what
happens with the output by implemenenting the {@link
de.uka.ilkd.key.util.pp.Backend} interface, or by using one of the
standard implementations {@link
de.uka.ilkd.key.util.pp.StringBackend} and {@link
de.uka.ilkd.key.util.pp.WriterBackend}.
@author Martin Giese
|
| de.uka.ilkd.key.visualdebugger | |
| de.uka.ilkd.key.visualdebugger.executiontree | |
| de.uka.ilkd.key.visualdebugger.statevisualisation | |
| de.uka.ilkd.key.visualization | |
| java.io | |
| java.lang | |
| java.math | |
| java.util | |
| javacard.framework | |
| junit.framework | |
| org.jmlspecs.lang | |
| org.jmlspecs.models | |
| proofVisualization | |
| proofVisualization.views | |
| src | |
| visualdebugger | |
| visualdebugger.actions | |
| visualdebugger.draw2d | |
| visualdebugger.views | |