Package | Description |
---|---|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml | |
de.uka.ilkd.key.speclang.jml.pretranslation | |
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.speclang.translation |
Modifier and Type | Method and Description |
---|---|
LabeledParserRuleContext |
InitiallyClauseImpl.getOriginalSpec() |
LabeledParserRuleContext |
InitiallyClause.getOriginalSpec() |
Constructor and Description |
---|
InitiallyClauseImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term inv,
ParsableVariable selfVar,
LabeledParserRuleContext originalSpec)
Creates a class invariant.
|
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<LabeledParserRuleContext> |
JMLSpecExtractor.createNonNullPositionedString(java.lang.String varName,
KeYJavaType kjt,
boolean isImplicitVar,
java.lang.String fileName,
Position pos,
Services services)
creates a JML specification expressing that the given variable/field is
not null and in case of a reference array type that also its elements are
non-null In case of implicit fields or primitive typed fields/variables
the empty set is returned
|
Modifier and Type | Method and Description |
---|---|
LabeledParserRuleContext |
TextualJMLClassAxiom.getAxiom() |
LabeledParserRuleContext |
TextualJMLAssertStatement.getContext() |
LabeledParserRuleContext |
TextualJMLInitially.getInv() |
LabeledParserRuleContext |
TextualJMLRepresents.getRepresents() |
LabeledParserRuleContext |
TextualJMLLoopSpec.getVariant() |
Modifier and Type | Method and Description |
---|---|
protected void |
TextualJMLConstruct.addGeneric(java.util.Map<java.lang.String,ImmutableList<LabeledParserRuleContext>> item,
LabeledParserRuleContext ps)
Deprecated.
|
Constructor and Description |
---|
TextualJMLAssertStatement(TextualJMLAssertStatement.Kind kind,
LabeledParserRuleContext clause) |
TextualJMLClassAxiom(ImmutableList<java.lang.String> mods,
LabeledParserRuleContext inv)
new textual representation.
|
TextualJMLClassAxiom(ImmutableList<java.lang.String> mods,
LabeledParserRuleContext inv,
java.lang.String name) |
TextualJMLDepends(ImmutableList<java.lang.String> mods,
Name[] heaps,
LabeledParserRuleContext depends) |
TextualJMLInitially(ImmutableList<java.lang.String> mods,
LabeledParserRuleContext inv) |
TextualJMLRepresents(ImmutableList<java.lang.String> mods,
LabeledParserRuleContext represents) |
TextualJMLRepresents(ImmutableList<java.lang.String> mods,
LabeledParserRuleContext represents,
java.lang.String name) |
Modifier and Type | Method and Description |
---|---|
ClassInvariant |
JMLSpecFactory.createJMLClassInvariant(KeYJavaType kjt,
VisibilityModifier visibility,
boolean isStatic,
LabeledParserRuleContext originalInv) |
Contract |
JMLSpecFactory.createJMLDependencyContract(KeYJavaType kjt,
LocationVariable targetHeap,
LabeledParserRuleContext originalDep) |
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 |
---|---|
Triple<IObserverFunction,Term,Term> |
JmlIO.translateDependencyContract(LabeledParserRuleContext ctx)
Translates a dependency contract.
|
InfFlowSpec |
JmlIO.translateInfFlow(LabeledParserRuleContext expr)
Translate the given context into an information flow specification.
|
Pair<Label,Term> |
JmlIO.translateLabeledClause(LabeledParserRuleContext parserRuleContext,
OriginTermLabel.SpecType type)
Interpret a labeled term (breaks clauses, continue clauses).
|
Pair<IObserverFunction,Term> |
JmlIO.translateRepresents(LabeledParserRuleContext clause)
Interpret a given represents clause.
|
Term |
JmlIO.translateTerm(LabeledParserRuleContext expr)
Interpret the given parse tree as an JML expression in the current context.
|
Term |
JmlIO.translateTerm(LabeledParserRuleContext expr,
OriginTermLabel.SpecType type)
Interpret the given parse tree as an JML expression in the current context.
|
Constructor and Description |
---|
SLTranslationException(java.lang.String message,
LabeledParserRuleContext expr) |
Copyright © 2003-2019 The KeY-Project.