Package | Description |
---|---|
de.uka.ilkd.key.proof_references | |
de.uka.ilkd.key.proof_references.analyst | |
de.uka.ilkd.key.proof_references.reference |
Modifier and Type | Method and Description |
---|---|
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Node node,
Services services)
Computes the
IProofReference of the given Node . |
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)
|
static java.util.LinkedHashSet<IProofReference<?>> |
ProofReferenceUtil.computeProofReferences(Proof proof,
ImmutableList<IProofReferencesAnalyst> analysts)
|
Modifier and Type | Method and Description |
---|---|
static void |
ProofReferenceUtil.merge(java.util.LinkedHashSet<IProofReference<?>> target,
IProofReference<?> reference)
Merges the
IProofReference into the target: |
Modifier and Type | Method and Description |
---|---|
static void |
ProofReferenceUtil.merge(java.util.LinkedHashSet<IProofReference<?>> target,
IProofReference<?> reference)
Merges the
IProofReference into the target: |
static void |
ProofReferenceUtil.merge(java.util.LinkedHashSet<IProofReference<?>> target,
java.util.LinkedHashSet<IProofReference<?>> toAdd)
Merges the
IProofReference s to add into the target. |
static void |
ProofReferenceUtil.merge(java.util.LinkedHashSet<IProofReference<?>> target,
java.util.LinkedHashSet<IProofReference<?>> toAdd)
Merges the
IProofReference s to add into the target. |
Modifier and Type | Method and Description |
---|---|
protected IProofReference<IProgramMethod> |
MethodCallProofReferencesAnalyst.createReference(Node node,
Services services,
ExecutionContext context,
MethodReference mr)
Creates an
IProofReference to the called IProgramMethod . |
Modifier and Type | Method and Description |
---|---|
java.util.LinkedHashSet<IProofReference<?>> |
ClassAxiomAndInvariantProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
ProgramVariableReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
MethodBodyExpandProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
ContractProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
IProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
java.util.LinkedHashSet<IProofReference<?>> |
MethodCallProofReferencesAnalyst.computeReferences(Node node,
Services services)
Computes the
IProofReference for the given Node which
can be null or an empty set if the applied rule is not supported by this IProofReferencesAnalyst . |
Modifier and Type | Method and Description |
---|---|
protected void |
ProgramVariableReferencesAnalyst.listReferences(Node node,
ProgramElement pe,
ProgramVariable arrayLength,
java.util.LinkedHashSet<IProofReference<?>> toFill,
boolean includeExpressionContainer)
Extracts the proof references recursive.
|
Modifier and Type | Class and Description |
---|---|
class |
DefaultProofReference<T>
Default implementation of
IProofReference . |
Copyright © 2003-2019 The KeY-Project.