Package | Description |
---|---|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
Modifier and Type | Field and Description |
---|---|
OriginTermLabel.SpecType |
OriginTermLabel.Origin.specType
The spec type the term originates from.
|
Modifier and Type | Method and Description |
---|---|
static OriginTermLabel.SpecType |
OriginTermLabel.SpecType.valueOf(java.lang.String name)
Returns the enum constant of this type with the specified name.
|
static OriginTermLabel.SpecType[] |
OriginTermLabel.SpecType.values()
Returns an array containing the constants of this enum type, in
the order they are declared.
|
Constructor and Description |
---|
FileOrigin(OriginTermLabel.SpecType specType,
java.lang.String fileName,
int line)
Creates a new
OriginTermLabel.Origin . |
NodeOrigin(OriginTermLabel.SpecType specType,
java.lang.String ruleName,
int nodeNr)
Creates a new
OriginTermLabel.Origin . |
Origin(OriginTermLabel.SpecType specType)
Creates a new
OriginTermLabel.Origin . |
Modifier and Type | Method and Description |
---|---|
Pair<Label,Term> |
JmlIO.translateLabeledClause(LabeledParserRuleContext parserRuleContext,
OriginTermLabel.SpecType type)
Interpret a labeled term (breaks clauses, continue clauses).
|
Term |
JmlIO.translateTerm(LabeledParserRuleContext expr,
OriginTermLabel.SpecType type)
Interpret the given parse tree as an JML expression in the current context.
|
Term |
JmlIO.translateTerm(org.antlr.v4.runtime.ParserRuleContext expr,
OriginTermLabel.SpecType type)
Interpret the given parse tree as an JML expression in the current context.
|
Constructor and Description |
---|
LabeledParserRuleContext(org.antlr.v4.runtime.ParserRuleContext ctx,
OriginTermLabel.SpecType specType) |
Copyright © 2003-2019 The KeY-Project.