Package | Description |
---|---|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
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.
|
Class and Description |
---|
Behavior
Enum type for the JML behavior kinds.
|
Class and Description |
---|
Behavior
Enum type for the JML behavior kinds.
|
TextualJMLAssertStatement.Kind |
TextualJMLConstruct
Objects of this type represent the various JML specification constructs in textual, unprocessed
form.
|
TextualJMLLoopSpec
A JML loop specification (invariant, assignable clause, decreases
clause, ...) in textual form.
|
TextualJMLLoopSpec.ClauseHd
Heap-dependent clauses
|
TextualJMLSpecCase
A JML specification case (i.e., more or less an operation contract) in
textual form.
|
TextualJMLSpecCase.Clause
Heap-independent clauses
|
TextualJMLSpecCase.ClauseHd
Heap-dependent clauses
|
Class and Description |
---|
Behavior
Enum type for the JML behavior kinds.
|
TextualJMLClassAxiom
A JML axiom declaration in textual form.
|
TextualJMLClassInv
A JML class invariant declaration in textual form.
|
TextualJMLDepends
A JML depends / accessible clause for a model field in textual form.
|
TextualJMLInitially
A JML initially clause declaration in textual form.
|
TextualJMLLoopSpec
A JML loop specification (invariant, assignable clause, decreases
clause, ...) in textual form.
|
TextualJMLMergePointDecl
A JML merge point declaration in textual form.
|
TextualJMLRepresents
A JML represents clause in textual form.
|
TextualJMLSpecCase
A JML specification case (i.e., more or less an operation contract) in
textual form.
|
Class and Description |
---|
TextualJMLConstruct
Objects of this type represent the various JML specification constructs in textual, unprocessed
form.
|
Copyright © 2003-2019 The KeY-Project.