public final class ProofReferenceUtil
extends java.lang.Object
This class provides static methods to compute proof references. A proof reference is a source code member used during proof like methods, instance or class variables or operation contracts.
A found proof reference is an instance of IProofReference
.
Proof references are computed for each Node
separately based
on the applied rule. Instances of IProofReferencesAnalyst
are used
to implement the rule specific extraction of such references.
This functionality is used by the Eclipse Projects like Visual DbC.
IProofReference
,
IProofReferencesAnalyst.
Modifier and Type | Class and Description |
---|---|
private static class |
ProofReferenceUtil.ReferenceAnalaystProofVisitor
Utility class used by
KeyProofReferenceUtil#analyzeProof(KeyConnection, Services, Proof) . |
Modifier and Type | Field and Description |
---|---|
static ImmutableList<IProofReferencesAnalyst> |
DEFAULT_ANALYSTS
The default
IProofReferencesAnalyst s. |
Modifier | Constructor and Description |
---|---|
private |
ProofReferenceUtil()
Forbid instances.
|
Modifier and Type | Method and Description |
---|---|
static java.util.LinkedHashSet<IProofReference<?>> |
computeProofReferences(Node node,
Services services)
Computes the
IProofReference of the given Node . |
static java.util.LinkedHashSet<IProofReference<?>> |
computeProofReferences(Node node,
Services services,
ImmutableList<IProofReferencesAnalyst> analysts)
Computes the
IProofReference of the given Node . |
static java.util.LinkedHashSet<IProofReference<?>> |
computeProofReferences(Proof proof)
|
static java.util.LinkedHashSet<IProofReference<?>> |
computeProofReferences(Proof proof,
ImmutableList<IProofReferencesAnalyst> analysts)
|
static void |
merge(java.util.LinkedHashSet<IProofReference<?>> target,
IProofReference<?> reference)
Merges the
IProofReference into the target: |
static void |
merge(java.util.LinkedHashSet<IProofReference<?>> target,
java.util.LinkedHashSet<IProofReference<?>> toAdd)
Merges the
IProofReference s to add into the target. |
public static final ImmutableList<IProofReferencesAnalyst> DEFAULT_ANALYSTS
IProofReferencesAnalyst
s.public static java.util.LinkedHashSet<IProofReference<?>> computeProofReferences(Proof proof)
Computes all proof references in the given Proof
by
iterating over all Node
s in breath first order.
Changes during computation of the proof tree are not detected and should be avoided. Otherwise it is possible that the result is wrong.
proof
- The Proof
to compute its references.IProofReference
s.public static java.util.LinkedHashSet<IProofReference<?>> computeProofReferences(Proof proof, ImmutableList<IProofReferencesAnalyst> analysts)
Computes all proof references in the given Proof
by
iterating over all Node
s in breath first order.
Changes during computation of the proof tree are not detected and should be avoided. Otherwise it is possible that the result is wrong.
proof
- The Proof
to compute its references.analysts
- The IProofReferencesAnalyst
to use.IProofReference
s.public static java.util.LinkedHashSet<IProofReference<?>> computeProofReferences(Node node, Services services)
IProofReference
of the given Node
.node
- The Node
to compute its IProofReference
s.services
- The Services
to use.IProofReference
s.public static java.util.LinkedHashSet<IProofReference<?>> computeProofReferences(Node node, Services services, ImmutableList<IProofReferencesAnalyst> analysts)
IProofReference
of the given Node
.node
- The Node
to compute its IProofReference
s.services
- The Services
to use.analysts
- The IProofReferencesAnalyst
to use.IProofReference
s.public static void merge(java.util.LinkedHashSet<IProofReference<?>> target, java.util.LinkedHashSet<IProofReference<?>> toAdd)
IProofReference
s to add into the target.target
- The target to add to.toAdd
- The IProofReference
s to add.public static void merge(java.util.LinkedHashSet<IProofReference<?>> target, IProofReference<?> reference)
IProofReference
into the target:target
- The target to add to.reference
- The IProofReference
to add.