de.uka.ilkd.key.proof_references.analyst

Interface IProofReferencesAnalyst

All Known Implementing Classes:

ClassAxiomAndInvariantProofReferencesAnalyst, ContractProofReferencesAnalyst, MethodBodyExpandProofReferencesAnalyst, MethodCallProofReferencesAnalyst, ProgramVariableReferencesAnalyst

public interface IProofReferencesAnalyst

Instances of this class are used to compute IProofReference for a given Node based on the applied rule. Each instance of this class has the knowledge to extract the references for a single rule or a group of similar rules.

The complete extraction is done via static methods of ProofReferenceUtil.

Author:

Martin Hentschel

See Also:

ProofReferenceUtil, IProofReference

Method Summary

Modifier and Type	Method and Description
java.util.LinkedHashSet<IProofReference<?>>	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.

Method Detail

computeReferences

java.util.LinkedHashSet<IProofReference<?>> 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.

Parameters:

node - The Node to compute its IProofReferences.

services - The Services to use.

Returns:

The found IProofReference or null/empty set if the applied rule is not supported.