de.uka.ilkd.key.proof_references.analyst

Class ClassAxiomAndInvariantProofReferencesAnalyst

java.lang.Object

de.uka.ilkd.key.proof_references.analyst.ClassAxiomAndInvariantProofReferencesAnalyst

All Implemented Interfaces:

IProofReferencesAnalyst

public class ClassAxiomAndInvariantProofReferencesAnalyst
extends java.lang.Object
implements IProofReferencesAnalyst

Extracts used ClassAxiom and ClassInvariants.

Author:

Martin Hentschel

Constructor Summary

Constructors

Constructor and Description
ClassAxiomAndInvariantProofReferencesAnalyst()

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.
protected KeYJavaType	findProofsKeYJavaType(Services services) Returns the KeYJavaType which provides the proof obligation of the current proof.

Methods inherited from class java.lang.Object

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

Constructor Detail

ClassAxiomAndInvariantProofReferencesAnalyst

public ClassAxiomAndInvariantProofReferencesAnalyst()

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.

findProofsKeYJavaType

protected KeYJavaType findProofsKeYJavaType(Services services)

Returns the KeYJavaType which provides the proof obligation of the current proof.

Parameters:

services - The Services to use.

Returns:

The KeYJavaType which provides the proof obligation or null if it was not possible to compute it.