Package | Description |
---|---|
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.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.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.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
Modifier and Type | Method and Description |
---|---|
ProgramElementName |
Recoder2KeYConverter.convert(Identifier id)
convert a recoder Identifier to a KeY Identifier
|
ProgramElementName |
Recoder2KeYConverter.convert(ImplicitIdentifier id) |
ProgramElementName |
NamedProgramElement.getProgramElementName()
Get identifier.
|
Modifier and Type | Method and Description |
---|---|
static ProgramElement |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
ProgramElementName typeName,
int dimensions,
ReferencePrefix typePrefix,
KeYJavaType baseType)
Create a local array variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ProgramElementName name,
Expression init,
KeYJavaType type)
create a local variable declaration
type name = init; |
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ProgramElementName name,
KeYJavaType type)
Create a local variable declaration without initialization.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ProgramElementName name,
TypeReference typeRef)
creates a local variable declaration
typeRef name; |
static ProgramVariable |
KeYJavaASTFactory.localVariable(ProgramElementName name,
KeYJavaType kjt)
create a local variable
|
void |
PrettyPrinter.printProgramElementName(ProgramElementName x) |
Modifier and Type | Method and Description |
---|---|
ProgramElementName |
PrimitiveType.getArrayElementName()
Returns the specific name of this primitive type used
in array types.
|
Modifier and Type | Field and Description |
---|---|
protected ProgramElementName |
TypeDeclaration.fullName |
protected ProgramElementName |
TypeDeclaration.name |
protected ProgramElementName |
MethodDeclaration.name |
Modifier and Type | Method and Description |
---|---|
static ProgramElementName |
ArrayDeclaration.createName(TypeReference basetype) |
ProgramElementName |
TypeDeclaration.getProgramElementName()
Get ProgramElementName.
|
ProgramElementName |
VariableSpecification.getProgramElementName()
Get name.
|
ProgramElementName |
MethodDeclaration.getProgramElementName() |
Constructor and Description |
---|
ClassDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary) |
ClassDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary,
boolean innerClass,
boolean anonymousClass,
boolean localClass)
uses children list to create non-anonymous class
|
ClassDeclaration(Modifier[] mods,
ProgramElementName name,
Extends extended,
ProgramElementName fullName,
Implements implemented,
MemberDeclaration[] members,
boolean parentIsInterfaceDeclaration,
boolean isLibrary)
Class declaration.
|
ConstructorDeclaration(Modifier[] modifiers,
ProgramElementName name,
ParameterDeclaration[] parameters,
Throws exceptions,
StatementBlock body,
boolean parentIsInterfaceDeclaration)
Deprecated.
|
EnumClassDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary,
java.util.List<EnumConstantDeclaration> enumConstantDeclarations)
create a new EnumClassDeclaration that describes an enum defintion.
|
InterfaceDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary)
uses children list to create non-anonymous class
|
InterfaceDeclaration(Modifier[] modifiers,
ProgramElementName name,
Extends extended,
MemberDeclaration[] members,
boolean isLibrary)
Construct a new outer or member interface class.
|
InterfaceDeclaration(Modifier[] modifiers,
ProgramElementName name,
ProgramElementName fullName,
Extends extended,
MemberDeclaration[] members,
boolean isLibrary)
Construct a new outer or member interface class.
|
InterfaceDeclaration(ProgramElementName name) |
MethodDeclaration(Modifier[] modifiers,
TypeReference returnType,
ProgramElementName name,
ImmutableArray<ParameterDeclaration> parameters,
Throws exceptions,
StatementBlock body,
boolean parentIsInterfaceDeclaration)
Method declaration.
|
MethodDeclaration(Modifier[] modifiers,
TypeReference returnType,
ProgramElementName name,
ParameterDeclaration[] parameters,
Throws exceptions,
StatementBlock body,
boolean parentIsInterfaceDeclaration)
Method declaration.
|
TypeDeclaration(ExtList children,
ProgramElementName fullName,
boolean isLibrary) |
TypeDeclaration(ExtList children,
ProgramElementName name,
ProgramElementName fullName,
boolean isLibrary) |
TypeDeclaration(Modifier[] mods,
ProgramElementName name,
ProgramElementName fullName,
MemberDeclaration[] members,
boolean parentIsInterfaceDeclaration,
boolean isLibrary)
Type declaration.
|
Modifier and Type | Field and Description |
---|---|
protected ProgramElementName |
TypeReferenceImp.name
Name.
|
protected ProgramElementName |
PackageReference.name
Name.
|
Modifier and Type | Method and Description |
---|---|
ProgramElementName |
VariableReference.getIdentifier() |
ProgramElementName |
MethodReference.getProgramElementName()
Get identifier.
|
ProgramElementName |
TypeReferenceImp.getProgramElementName()
Get identifier.
|
ProgramElementName |
PackageReference.getProgramElementName()
Get identifier.
|
ProgramElementName |
VariableReference.getProgramElementName() |
ProgramElementName |
SchematicFieldReference.getProgramElementName() |
ProgramElementName |
TypeReference.getProgramElementName() |
Constructor and Description |
---|
PackageReference(ProgramElementName name,
ReferencePrefix prefix) |
SchemaTypeReference(ProgramElementName name,
int dimension,
ReferencePrefix prefix) |
TypeRef(ProgramElementName name,
int dimension,
ReferencePrefix prefix,
KeYJavaType kjt) |
TypeReferenceImp(ProgramElementName name) |
TypeReferenceImp(ProgramElementName name,
int dimension,
ReferencePrefix prefix) |
Modifier and Type | Method and Description |
---|---|
ProgramElementName |
LabeledStatement.getProgramElementName()
Get identifier.
|
ProgramElementName |
LabelJumpStatement.getProgramElementName()
Get identifier.
|
Modifier and Type | Method and Description |
---|---|
void |
Visitor.performActionOnProgramElementName(ProgramElementName x) |
void |
JavaASTVisitor.performActionOnProgramElementName(ProgramElementName x) |
Modifier and Type | Class and Description |
---|---|
static class |
VariableNamer.IndProgramElementName
ProgramElementName carrying an additional index
|
Modifier and Type | Method and Description |
---|---|
protected ProgramElementName |
VariableNamer.createName(java.lang.String basename,
int index,
NameCreationInfo creationInfo)
creates a ProgramElementName object to be used for permanent names
|
protected ProgramElementName |
VariableNamer.getNameProposalForSchemaVariable(java.lang.String basename,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
(like getProposal(), but somewhat less nicely)
|
ProgramElementName |
VariableNamer.getTemporaryNameProposal(java.lang.String basename)
proposes a unique name; intended for use in places where the information
required by getProposal() is not available
|
static ProgramElementName |
VariableNamer.parseName(java.lang.String name) |
static ProgramElementName |
VariableNamer.parseName(java.lang.String name,
Comment[] comments) |
static ProgramElementName |
VariableNamer.parseName(java.lang.String name,
NameCreationInfo creationInfo) |
static ProgramElementName |
VariableNamer.parseName(java.lang.String name,
NameCreationInfo creationInfo,
Comment[] comments)
parses the passed string and creates a suitable program element name
(this does *not* make the name unique - if that is necessary, use either
getTemporaryNameProposal() or getProposal())
|
Modifier and Type | Method and Description |
---|---|
protected java.lang.Iterable<ProgramElementName> |
VariableNamer.wrapGlobals(ImmutableList<? extends Named> globals)
creates a Globals object for use with other internal methods
|
protected java.lang.Iterable<ProgramElementName> |
VariableNamer.wrapGlobals(ImmutableSet<ProgramVariable> globals)
creates a Globals object for use with other internal methods
|
Modifier and Type | Method and Description |
---|---|
protected VariableNamer.BasenameAndIndex |
VariableNamer.getBasenameAndIndex(ProgramElementName name)
determines the passed ProgramElementName's basename and index (ignoring
temporary indices)
|
Modifier and Type | Method and Description |
---|---|
protected int |
VariableNamer.getMaxCounterInGlobals(java.lang.String basename,
java.lang.Iterable<ProgramElementName> globals)
returns the maximum counter value already associated with the passed
basename in the passed list of global variables, or -1
|
protected boolean |
VariableNamer.isUniqueInGlobals(java.lang.String name,
java.lang.Iterable<ProgramElementName> globals)
tells whether a name is unique in the passed list of global variables
|
Modifier and Type | Method and Description |
---|---|
static ProgramElementName |
ObserverFunction.createName(java.lang.String baseName,
KeYJavaType container) |
ProgramElementName |
ProgramVariable.getProgramElementName() |
ProgramElementName |
ProgramMethod.getProgramElementName() |
ProgramElementName |
IProgramMethod.getProgramElementName() |
ProgramElementName |
ProgramSV.getProgramElementName() |
Modifier and Type | Method and Description |
---|---|
static ProgramSV |
SchemaVariableFactory.createProgramSV(ProgramElementName name,
ProgramSVSort s,
boolean listSV)
creates a SchemaVariable representing a program construct
|
Constructor and Description |
---|
LocationVariable(ProgramElementName name,
KeYJavaType t) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
boolean isFinal) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
boolean isGhost,
boolean isFinal) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost,
boolean isFinal) |
LocationVariable(ProgramElementName name,
Sort s) |
ProgramConstant(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
Literal compileTimeConstant) |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost) |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost,
boolean isFinal) |
Modifier and Type | Method and Description |
---|---|
ProgramElementName |
ProgramTransformer.getProgramElementName() |
Constructor and Description |
---|
ForToWhileTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
Services services) |
WhileInvariantTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
ProgramVariable cont,
ProgramVariable exc,
ProgramVariable excParam,
ProgramVariable thrownException,
ProgramVariable brk,
ProgramVariable rtrn,
ProgramVariable returnExpr,
java.util.LinkedList<de.uka.ilkd.key.rule.metaconstruct.BreakToBeReplaced> breakList,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
WhileLoopTransformation(ProgramElement root,
ProgramElementName outerLabel,
ProgramElementName innerLabel,
Services services)
creates the WhileLoopTransformation for the transformation mode
|
Copyright © 2003-2019 The KeY-Project.