public class ClassAxiomAndInvariantProofReferencesAnalyst extends java.lang.Object implements IProofReferencesAnalyst
ClassAxiom
and ClassInvariant
s.Constructor and Description |
---|
ClassAxiomAndInvariantProofReferencesAnalyst() |
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. |
public ClassAxiomAndInvariantProofReferencesAnalyst()
public java.util.LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services)
IProofReference
for the given Node
which
can be null
or an empty set if the applied rule is not supported by this IProofReferencesAnalyst
.computeReferences
in interface IProofReferencesAnalyst
node
- The Node
to compute its IProofReference
s.services
- The Services
to use.IProofReference
or null
/empty set if the applied rule is not supported.protected KeYJavaType findProofsKeYJavaType(Services services)
KeYJavaType
which provides the proof obligation of the current proof.services
- The Services
to use.KeYJavaType
which provides the proof obligation or null
if it was not possible to compute it.