public interface IProofReference<T>
IProofReferencesAnalyst
s
during reference computation via static methods of ProofReferenceUtil
.ProofReferenceUtil
,
IProofReferencesAnalyst.
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.
|
Modifier and Type | Method and Description |
---|---|
void |
addNodes(java.util.Collection<Node> nodes)
|
java.lang.String |
getKind()
Returns the reference kind which is a human readable
String . |
java.util.LinkedHashSet<Node> |
getNodes()
Returns the
Node s in which the reference was found. |
Proof |
getSource()
Returns the source
Proof . |
T |
getTarget()
Returns the target source member.
|
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()
).
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()
).
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()
).
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()
).
static final java.lang.String USE_INVARIANT
Used invariants during proof.
References of this kind should provide an ClassInvariant
as target (getTarget()
).
static final java.lang.String USE_AXIOM
Used axioms during proof.
References of this kind should provide an ClassAxiom
as target (getTarget()
).
java.lang.String getKind()
String
.String
.java.util.LinkedHashSet<Node> getNodes()
Node
s in which the reference was found.Node
s in which the reference was found.T getTarget()