Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
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.
|
de.uka.ilkd.key.speclang.jml |
Modifier and Type | Method and Description |
---|---|
static boolean |
JavaInfo.isVisibleTo(SpecificationElement ax,
KeYJavaType visibleTo) |
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addSpecs(ImmutableSet<SpecificationElement> specs) |
Modifier and Type | Interface and Description |
---|---|
interface |
AuxiliaryContract
Super-interface for
BlockContract and LoopContract . |
interface |
BlockContract
A block contract.
|
interface |
ClassInvariant
A class invariant.
|
interface |
Contract
A contractual agreement about an ObserverFunction.
|
interface |
DependencyContract
A contract about the dependencies of an observer symbol, consisting of
a precondition, a depends clause, and a measured-by clause.
|
interface |
FunctionalOperationContract
A contract about an operation (i.e., a method or a constructor), consisting
of a precondition, a postcondition, a modifies clause, a measured-by clause,
and a modality.
|
interface |
InformationFlowContract
A contract about the dependencies of an observer symbol, consisting of
a precondition, a depends clause, and a measured-by clause.
|
interface |
InitiallyClause |
interface |
LoopContract
A contract for a block that begins with a loop.
|
interface |
LoopSpecification
A loop invariant, consisting of an invariant formula, a set of loop
predicates, a modifies clause, and a variant term.
|
interface |
MergeContract
Specification of a
MergePointStatement . |
interface |
OperationContract |
Modifier and Type | Class and Description |
---|---|
class |
AbstractAuxiliaryContractImpl
Abstract base class for all default implementations of the sub-interfaces of
AuxiliaryContract . |
class |
BlockContractImpl
Default implementation of
BlockContract . |
class |
BlockWellDefinedness
A contract for checking the well-definedness of a jml block contract.
|
class |
ClassAxiom
An axiom originating from a (JML) specification, belonging to a particular
class, and constraining a particular observer symbol.
|
class |
ClassAxiomImpl
Represents an axiom specified in a class.
|
class |
ClassInvariantImpl
Standard implementation of the ClassInvariant interface.
|
class |
ClassWellDefinedness
A contract for checking the well-definedness of a specification for a class invariant.
|
class |
ContractAxiom |
class |
DependencyContractImpl
Standard implementation of the DependencyContract interface.
|
class |
FunctionalAuxiliaryContract<T extends AuxiliaryContract>
This class is only used to generate a proof obligation for an
AuxiliaryContract . |
class |
FunctionalBlockContract
This class is only used to generate a proof obligation for a block (see
FunctionalBlockContractPO . |
class |
FunctionalLoopContract
This class is only used to generate a proof obligation for a block that starts with a loop (see
FunctionalLoopContractPO . |
class |
FunctionalOperationContractImpl
Standard implementation of the OperationContract interface.
|
class |
InformationFlowContractImpl
Standard implementation of the DependencyContract interface.
|
class |
InitiallyClauseImpl
Standard implementation of the InitiallyClause interface.
|
class |
LoopContractImpl
Default implementation for
LoopContract . |
class |
LoopSpecImpl
Standard implementation of the LoopInvariant interface.
|
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 |
ModelMethodExecution |
class |
PartialInvAxiom
A class axiom which is essentially of the form "o.
|
class |
PredicateAbstractionMergeContract
|
class |
QueryAxiom
A class axiom that connects an observer symbol representing a Java
method (i.e., an object of type IProgramMethod), with the corresponding
method body.
|
class |
RepresentsAxiom
A class axiom corresponding to a JML* represents clause.
|
class |
StatementWellDefinedness
A contract for checking the well-definedness of a jml statement.
|
class |
UnparameterizedMergeContract
|
class |
WellDefinednessCheck
A contract for checking the well-definedness of a jml specification element
(i.e.
|
Modifier and Type | Method and Description |
---|---|
abstract SpecificationElement |
StatementWellDefinedness.getStatement() |
SpecificationElement |
PartialInvAxiom.map(java.util.function.UnaryOperator<Term> op,
Services services) |
SpecificationElement |
RepresentsAxiom.map(java.util.function.UnaryOperator<Term> op,
Services services) |
SpecificationElement |
SpecificationElement.map(java.util.function.UnaryOperator<Term> op,
Services services)
Applies a unary operator to every term in this specification element.
|
Modifier and Type | Method and Description |
---|---|
ImmutableSet<SpecificationElement> |
SpecExtractor.extractClassSpecs(KeYJavaType kjt)
Returns the class invariants for the passed type.
|
ImmutableSet<SpecificationElement> |
SpecExtractor.extractMethodSpecs(IProgramMethod pm)
Returns the operation contracts for the passed operation.
|
ImmutableSet<SpecificationElement> |
SpecExtractor.extractMethodSpecs(IProgramMethod pm,
boolean addInvariant) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<SpecificationElement> |
JMLSpecExtractor.extractClassSpecs(KeYJavaType kjt) |
ImmutableSet<SpecificationElement> |
JMLSpecExtractor.extractMethodSpecs(IProgramMethod pm) |
ImmutableSet<SpecificationElement> |
JMLSpecExtractor.extractMethodSpecs(IProgramMethod pm,
boolean addInvariant)
Extracts method specifications (i.e., contracts) from Java+JML input.
|
Copyright © 2003-2019 The KeY-Project.