Package | Description |
---|---|
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
Modifier and Type | Method and Description |
---|---|
WellDefinednessCheck |
WellDefinednessPO.getContract() |
Constructor and Description |
---|
WellDefinednessPO(InitConfig initConfig,
WellDefinednessCheck check)
Constructor
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<WellDefinednessCheck> |
SpecificationRepository.getAllWdChecks()
Returns all registered well-definedness checks.
|
Modifier and Type | Class and Description |
---|---|
class |
BlockWellDefinedness
A contract for checking the well-definedness of a jml block contract.
|
class |
ClassWellDefinedness
A contract for checking the well-definedness of a specification for a class invariant.
|
class |
LoopWellDefinedness
A contract for checking the well-definedness of a jml loop invariant.
|
class |
MethodWellDefinedness
A contract for checking the well-definedness of a specification for a method or model field.
|
class |
StatementWellDefinedness
A contract for checking the well-definedness of a jml statement.
|
Modifier and Type | Method and Description |
---|---|
WellDefinednessCheck |
WellDefinednessCheck.addRepresents(Term rep) |
WellDefinednessCheck |
WellDefinednessCheck.combine(WellDefinednessCheck wdc,
TermServices services)
Combines two well-definedness checks having the same name, id, target, type,
behaviour and are either both model fields or both not a model field.
|
abstract WellDefinednessCheck |
WellDefinednessCheck.map(java.util.function.UnaryOperator<Term> op,
Services services) |
Modifier and Type | Method and Description |
---|---|
MethodWellDefinedness |
MethodWellDefinedness.combine(WellDefinednessCheck wdc,
TermServices services) |
ClassWellDefinedness |
ClassWellDefinedness.combine(WellDefinednessCheck wdc,
TermServices services) |
WellDefinednessCheck |
WellDefinednessCheck.combine(WellDefinednessCheck wdc,
TermServices services)
Combines two well-definedness checks having the same name, id, target, type,
behaviour and are either both model fields or both not a model field.
|
LoopWellDefinedness |
LoopWellDefinedness.combine(WellDefinednessCheck wdc,
TermServices services) |
BlockWellDefinedness |
BlockWellDefinedness.combine(WellDefinednessCheck wdc,
TermServices services) |
Copyright © 2003-2019 The KeY-Project.