de.uka.ilkd.key.proof_references

Class ProofReferenceUtil

java.lang.Object

de.uka.ilkd.key.proof_references.ProofReferenceUtil

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.

Author:

Martin Hentschel

See Also:

IProofReference, IProofReferencesAnalyst.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private static class	ProofReferenceUtil.ReferenceAnalaystProofVisitor Utility class used by KeyProofReferenceUtil#analyzeProof(KeyConnection, Services, Proof).

Field Summary

Fields

Modifier and Type	Field and Description
static ImmutableList<IProofReferencesAnalyst>	DEFAULT_ANALYSTS The default IProofReferencesAnalysts.

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ProofReferenceUtil() Forbid instances.

Method Summary

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) Computes all proof references in the given Proof by iterating over all Nodes in breath first order.
static java.util.LinkedHashSet<IProofReference<?>>	computeProofReferences(Proof proof, ImmutableList<IProofReferencesAnalyst> analysts) Computes all proof references in the given Proof by iterating over all Nodes in breath first order.
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 IProofReferences to add into the target.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

DEFAULT_ANALYSTS

public static final ImmutableList<IProofReferencesAnalyst> DEFAULT_ANALYSTS

The default IProofReferencesAnalysts.

Constructor Detail

ProofReferenceUtil

private ProofReferenceUtil()

Forbid instances.

Method Detail

computeProofReferences

public static java.util.LinkedHashSet<IProofReference<?>> computeProofReferences(Proof proof)

Computes all proof references in the given Proof by iterating over all Nodes 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.

Parameters:

proof - The Proof to compute its references.

Returns:

The found IProofReferences.

computeProofReferences

public static java.util.LinkedHashSet<IProofReference<?>> computeProofReferences(Proof proof,
                                                                                 ImmutableList<IProofReferencesAnalyst> analysts)

Computes all proof references in the given Proof by iterating over all Nodes 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.

Parameters:

proof - The Proof to compute its references.

analysts - The IProofReferencesAnalyst to use.

Returns:

The found IProofReferences.

computeProofReferences

public static java.util.LinkedHashSet<IProofReference<?>> computeProofReferences(Node node,
                                                                                 Services services)

Computes the IProofReference of the given Node.

Parameters:

node - The Node to compute its IProofReferences.

services - The Services to use.

Returns:

The found IProofReferences.

computeProofReferences

public static java.util.LinkedHashSet<IProofReference<?>> computeProofReferences(Node node,
                                                                                 Services services,
                                                                                 ImmutableList<IProofReferencesAnalyst> analysts)

Computes the IProofReference of the given Node.

Parameters:

node - The Node to compute its IProofReferences.

services - The Services to use.

analysts - The IProofReferencesAnalyst to use.

Returns:

The found IProofReferences.

merge

public static void merge(java.util.LinkedHashSet<IProofReference<?>> target,
                         java.util.LinkedHashSet<IProofReference<?>> toAdd)

Merges the IProofReferences to add into the target.

Parameters:

target - The target to add to.

toAdd - The IProofReferences to add.

merge

public static void merge(java.util.LinkedHashSet<IProofReference<?>> target,
                         IProofReference<?> reference)

Merges the IProofReference into the target:

Parameters:

target - The target to add to.

reference - The IProofReference to add.