|
Class Summary |
| ConstructorPO |
This class describes proof obligations for a constructor and facilities
to calculate them. |
| MethodPO |
This class describes proof obligations for a method and facilities
to calculate them. |
| ProofObligation |
This abstract class describes a proof obligation and facilities to calculate
them. |
| SourceProofObligation |
This abstract class describes a proof obligation and facilities to calculate
them at source level. |
| StaticInitializationPO |
This class describes a proof obligation for a static initialization and
facilities to calculate them. |
| WellDefinedInvPO |
|
| WellDefinedSpecPO |
|