Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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.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.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
Modifier and Type | Interface and Description |
---|---|
interface |
Label |
interface |
ProgramVariableName |
Modifier and Type | Class and Description |
---|---|
class |
Modifier
Modifier.
|
Modifier and Type | Class and Description |
---|---|
class |
Abstract
Abstract.
|
class |
AnnotationUseSpecification |
class |
Final
Final.
|
class |
Ghost
The JML modifier "ghost".
|
class |
Model
The JML modifier "model".
|
class |
Native
Native.
|
class |
NoState
The JML modifier "no_state".
|
class |
Private
Private.
|
class |
Protected
Protected.
|
class |
Public
Public.
|
class |
Static
Static.
|
class |
StrictFp
Strict fp.
|
class |
Synchronized
Synchronized.
|
class |
Transient
Transient.
|
class |
TwoState
The JML modifier "two_state".
|
class |
VisibilityModifier
Visibility modifier.
|
class |
Volatile
Volatile.
|
Modifier and Type | Class and Description |
---|---|
class |
Literal
Literal.
|
Modifier and Type | Class and Description |
---|---|
class |
AbstractIntegerLiteral
This class is a superclass for integer literals (Int, Long, Char).
|
class |
BooleanLiteral
Boolean literal.
|
class |
CharLiteral
Char literal.
|
class |
DoubleLiteral
Double literal.
|
class |
EmptyMapLiteral |
class |
EmptySeqLiteral |
class |
EmptySetLiteral |
class |
FloatLiteral
Float literal.
|
class |
FreeLiteral |
class |
IntLiteral
Int literal.
|
class |
LongLiteral
Long literal.
|
class |
NullLiteral
Null literal.
|
class |
RealLiteral
JML \real literal.
|
class |
StringLiteral |
Modifier and Type | Interface and Description |
---|---|
interface |
MethodName
Method name.
|
Modifier and Type | Interface and Description |
---|---|
interface |
IForUpdates |
interface |
ILoopInit |
Modifier and Type | Class and Description |
---|---|
class |
EmptyStatement
Empty statement.
|
class |
ForUpdates |
class |
LoopInit |
Modifier and Type | Interface and Description |
---|---|
interface |
ProgramConstruct
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
Modifier and Type | Class and Description |
---|---|
class |
ProgramElementName |
static class |
VariableNamer.IndProgramElementName
ProgramElementName carrying an additional index
|
Modifier and Type | Interface and Description |
---|---|
interface |
IProgramVariable |
Modifier and Type | Class and Description |
---|---|
class |
LocationVariable
This class represents proper program variables, which are not program
constants.
|
class |
ProgramConstant
This class represents currently only static final fields initialised with
a compile time constant.
|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
class |
ProgramVariable
The objects of this class represent program variables and program
constants (resulting from static final declarations in programs; TODO: it is
weird that constants are a special case of variables).
|
Copyright © 2003-2019 The KeY-Project.