de.uka.ilkd.key.proof_references.analyst

Class ContractProofReferencesAnalyst

java.lang.Object

de.uka.ilkd.key.proof_references.analyst.ContractProofReferencesAnalyst

All Implemented Interfaces:

IProofReferencesAnalyst

public class ContractProofReferencesAnalyst
extends java.lang.Object
implements IProofReferencesAnalyst

Extracts used contracts.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
ContractProofReferencesAnalyst()

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.

Methods inherited from class java.lang.Object

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

Constructor Detail

ContractProofReferencesAnalyst

public ContractProofReferencesAnalyst()

Method Detail

computeReferences

public 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.

Specified by:

computeReferences in interface 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.