Package | Description |
---|---|
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.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.speclang.translation |
Modifier and Type | Method and Description |
---|---|
VisibilityModifier |
JavaDeclaration.getVisibilityModifier()
Returns a Public, Protected, or Private Modifier, if there
is one, null otherwise.
|
Modifier and Type | Class and Description |
---|---|
class |
Private
Private.
|
class |
Protected
Protected.
|
class |
Public
Public.
|
Modifier and Type | Method and Description |
---|---|
static boolean |
VisibilityModifier.allowsInheritance(VisibilityModifier vm)
Whether it represents at least a
protected modifier. |
int |
Public.compareTo(VisibilityModifier arg0) |
int |
Protected.compareTo(VisibilityModifier arg0) |
int |
Private.compareTo(VisibilityModifier arg0) |
static boolean |
VisibilityModifier.isPackageVisible(VisibilityModifier vm)
Whether it represents at least default (package-private) visibility.
|
static boolean |
VisibilityModifier.isPrivate(VisibilityModifier vm)
Whether it represents a
private modifier. |
static boolean |
VisibilityModifier.isPublic(VisibilityModifier vm)
Whether it represents a
public modifier. |
Constructor and Description |
---|
ClassAxiomImpl(java.lang.String name,
KeYJavaType kjt,
VisibilityModifier visibility,
Term rep,
ProgramVariable selfVar) |
ClassAxiomImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term rep,
ProgramVariable selfVar) |
ClassInvariantImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term inv,
ParsableVariable selfVar)
Creates a class invariant.
|
ContractAxiom(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term post,
Term mby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
ContractAxiom(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term originalPre,
Term originalPost,
Term originalMby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
InitiallyClauseImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term inv,
ParsableVariable selfVar,
LabeledParserRuleContext originalSpec)
Creates a class invariant.
|
ModelMethodExecution(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility) |
ModelMethodExecution(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility) |
RepresentsAxiom(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term rep,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars) |
RepresentsAxiom(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term rep,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars) |
Modifier and Type | Method and Description |
---|---|
VisibilityModifier |
JMLResolverManager.getSpecVisibility(MemberDeclaration md) |
Modifier and Type | Method and Description |
---|---|
ClassInvariant |
JMLSpecFactory.createJMLClassInvariant(KeYJavaType kjt,
VisibilityModifier visibility,
boolean isStatic,
LabeledParserRuleContext originalInv) |
InitiallyClause |
JMLSpecFactory.createJMLInitiallyClause(KeYJavaType kjt,
VisibilityModifier visibility,
LabeledParserRuleContext original) |
ClassAxiom |
JMLSpecFactory.createJMLRepresents(KeYJavaType kjt,
VisibilityModifier visibility,
LabeledParserRuleContext originalRep,
boolean isStatic) |
Modifier and Type | Method and Description |
---|---|
VisibilityModifier |
SLResolverManager.getSpecVisibility(MemberDeclaration md)
Returns a specification-language based visibility level for the
passed member that should take precedence over Java's ordinary
visibility, or null.
|
Copyright © 2003-2019 The KeY-Project.