Interface | Description |
---|---|
IProofReferencesAnalyst |
Instances of this class are used to compute
IProofReference for
a given Node based on the applied rule. |
Class | Description |
---|---|
ClassAxiomAndInvariantProofReferencesAnalyst |
Extracts used
ClassAxiom and ClassInvariant s. |
ContractProofReferencesAnalyst |
Extracts used contracts.
|
MethodBodyExpandProofReferencesAnalyst |
Extracts inlined methods.
|
MethodCallProofReferencesAnalyst |
Extracts called methods.
|
ProgramVariableReferencesAnalyst |
Extracts read and write access to fields (
IProgramVariable ) via assignments. |