de.uka.ilkd.key.proof_references.reference

Interface IProofReference<T>

All Known Implementing Classes:

DefaultProofReference

public interface IProofReference<T>

A proof reference which points to a source member used during proof. By default, instances are created via IProofReferencesAnalysts during reference computation via static methods of ProofReferenceUtil.

Author:

Martin Hentschel

See Also:

ProofReferenceUtil, IProofReferencesAnalyst.

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	ACCESS Read/Write access of a field like instance or class variables during proof.
static java.lang.String	CALL_METHOD A method call which determines the possible implementations of a called method.
static java.lang.String	INLINE_METHOD The proof step "methodBodyExpand" that inlines methods.
static java.lang.String	USE_AXIOM Used axioms during proof.
static java.lang.String	USE_CONTRACT The proof step "Use Operation Contract" which approximates a method call via its method contract and also the usage of dependency contracts.
static java.lang.String	USE_INVARIANT Used invariants during proof.

Method Summary

Modifier and Type	Method and Description
void	addNodes(java.util.Collection<Node> nodes) Adds the given Nodes to the own Nodes.
java.lang.String	getKind() Returns the reference kind which is a human readable String.
java.util.LinkedHashSet<Node>	getNodes() Returns the Nodes in which the reference was found.
Proof	getSource() Returns the source Proof.
T	getTarget() Returns the target source member.

Field Detail

CALL_METHOD

static final java.lang.String CALL_METHOD

A method call which determines the possible implementations of a called method.

References of this kind should provide an IProgramMethod as target (getTarget()).

See Also:

Constant Field Values

INLINE_METHOD

static final java.lang.String INLINE_METHOD

The proof step "methodBodyExpand" that inlines methods.

References of this kind should provide an IProgramMethod as target (getTarget()).

See Also:

Constant Field Values

USE_CONTRACT

static final java.lang.String USE_CONTRACT

The proof step "Use Operation Contract" which approximates a method call via its method contract and also the usage of dependency contracts.

References of this kind should provide a Contract as target (getTarget()).

See Also:

Constant Field Values

ACCESS

static final java.lang.String ACCESS

Read/Write access of a field like instance or class variables during proof.

References of this kind should provide an IProgramVariable as target (getTarget()).

See Also:

Constant Field Values

USE_INVARIANT

static final java.lang.String USE_INVARIANT

Used invariants during proof.

References of this kind should provide an ClassInvariant as target (getTarget()).

See Also:

Constant Field Values

USE_AXIOM

static final java.lang.String USE_AXIOM

Used axioms during proof.

References of this kind should provide an ClassAxiom as target (getTarget()).

See Also:

Constant Field Values

Method Detail

getKind

java.lang.String getKind()

Returns the reference kind which is a human readable String.

Returns:

The reference kind as human readable String.

getNodes

java.util.LinkedHashSet<Node> getNodes()

Returns the Nodes in which the reference was found.

Returns:

The Nodes in which the reference was found.

addNodes

void addNodes(java.util.Collection<Node> nodes)

Adds the given Nodes to the own Nodes.

Parameters:

nodes - The Nodes to add.

getTarget

T getTarget()

Returns the target source member.

Returns:

The target source member.

getSource

Proof getSource()

Returns the source Proof.

Returns:

The source Proof.