Package | Description |
---|---|
de.uka.ilkd.key.speclang.jml.pretranslation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
Modifier and Type | Class and Description |
---|---|
class |
TextualJMLAssertStatement
A JML assert/assume statement.
|
class |
TextualJMLClassAxiom
A JML axiom declaration in textual form.
|
class |
TextualJMLClassInv
A JML class invariant declaration in textual form.
|
class |
TextualJMLDepends
A JML depends / accessible clause for a model field in textual form.
|
class |
TextualJMLFieldDecl
A JML field declaration (ghost or model) in textual form.
|
class |
TextualJMLInitially
A JML initially clause declaration in textual form.
|
class |
TextualJMLLoopSpec
A JML loop specification (invariant, assignable clause, decreases
clause, ...) in textual form.
|
class |
TextualJMLMergePointDecl
A JML merge point declaration in textual form.
|
class |
TextualJMLMethodDecl
A JML model method declaration in textual form.
|
class |
TextualJMLRepresents
A JML represents clause in textual form.
|
class |
TextualJMLSetStatement
A JML set statement in textual form.
|
class |
TextualJMLSpecCase
A JML specification case (i.e., more or less an operation contract) in
textual form.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseClassLevel(JmlLexer lexer)
Parses a JML constructs on class level, e.g., invariants and methods contracts, and returns a parse tree.
|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseClassLevel(java.lang.String content)
Parses a JML constructs on class level, e.g., invariants and methods contracts, and returns a parse tree.
|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseClassLevel(java.lang.String concatenatedComment,
java.lang.String fileName,
Position pos)
Parse and interpret class level comments.
|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseMethodLevel(PositionedString positionedString)
Parses a JML constructs which occurs inside methods (mostly JML statements) and returns a parse tree.
|
ImmutableList<TextualJMLConstruct> |
JmlIO.parseMethodLevel(java.lang.String concatenatedComment,
java.lang.String fileName,
Position position)
Parse and interpret the given string as a method level construct.
|
Copyright © 2003-2019 The KeY-Project.