| 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 ClassInvariants. |
| ContractProofReferencesAnalyst |
Extracts used contracts.
|
| MethodBodyExpandProofReferencesAnalyst |
Extracts inlined methods.
|
| MethodCallProofReferencesAnalyst |
Extracts called methods.
|
| ProgramVariableReferencesAnalyst |
Extracts read and write access to fields (
IProgramVariable) via assignments. |