Package | Description |
---|---|
de.uka.ilkd.key.proof_references | |
de.uka.ilkd.key.proof_references.analyst |
Modifier and Type | Field and Description |
---|---|
static ImmutableList<IProofReferencesAnalyst> |
ProofReferenceUtil.DEFAULT_ANALYSTS
The default
IProofReferencesAnalyst s. |
Modifier and Type | Method and Description |
---|---|
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Node node,
Services services,
ImmutableList<IProofReferencesAnalyst> analysts)
Computes the
IProofReference of the given Node . |
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Proof proof,
ImmutableList<IProofReferencesAnalyst> analysts)
|
Modifier and Type | Class and Description |
---|---|
class |
ClassAxiomAndInvariantProofReferencesAnalyst
Extracts used
ClassAxiom and ClassInvariant s. |
class |
ContractProofReferencesAnalyst
Extracts used contracts.
|
class |
MethodBodyExpandProofReferencesAnalyst
Extracts inlined methods.
|
class |
MethodCallProofReferencesAnalyst
Extracts called methods.
|
class |
ProgramVariableReferencesAnalyst
Extracts read and write access to fields (
IProgramVariable ) via assignments. |
Copyright © 2003-2019 The KeY-Project.