de.uka.ilkd.key.proof_references

Class ProofReferenceUtil.ReferenceAnalaystProofVisitor

java.lang.Object

de.uka.ilkd.key.proof_references.ProofReferenceUtil.ReferenceAnalaystProofVisitor

All Implemented Interfaces:

ProofVisitor

Enclosing class:

ProofReferenceUtil

private static class ProofReferenceUtil.ReferenceAnalaystProofVisitor
extends java.lang.Object
implements ProofVisitor

Utility class used by KeyProofReferenceUtil#analyzeProof(KeyConnection, Services, Proof).

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableList<IProofReferencesAnalyst>	analysts The IProofReferencesAnalysts to use.
private java.util.LinkedHashSet<IProofReference<?>>	result The result.
private Services	services The Services to use.

Constructor Summary

Constructors

Constructor and Description
ReferenceAnalaystProofVisitor(Services services, ImmutableList<IProofReferencesAnalyst> analysts) Constructor.

Method Summary

Modifier and Type	Method and Description
java.util.LinkedHashSet<IProofReference<?>>	getResult() Returns the result.
void	visit(Proof proof, Node visitedNode)

Methods inherited from class java.lang.Object

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

Field Detail

services

private Services services

The Services to use.

analysts

private ImmutableList<IProofReferencesAnalyst> analysts

The IProofReferencesAnalysts to use.

result

private java.util.LinkedHashSet<IProofReference<?>> result

The result.

Constructor Detail

ReferenceAnalaystProofVisitor

public ReferenceAnalaystProofVisitor(Services services,
                                     ImmutableList<IProofReferencesAnalyst> analysts)

Constructor.

Parameters:

services - The Services to use.

analysts - The IProofReferencesAnalysts to use.

Method Detail

visit

public void visit(Proof proof,
                  Node visitedNode)

Specified by:

visit in interface ProofVisitor

getResult

public java.util.LinkedHashSet<IProofReference<?>> getResult()

Returns the result.

Returns:

The result.