| Class | Description |
|---|---|
| ProgramMethodPO |
This proof obligation executes an
IProgramMethod with
an optional precondition. |
| ProgramMethodSubsetPO |
This proof obligation executes selected statements of the body
of a given
IProgramMethod. |
| TruthValuePOExtension |
Implementation of
POExtension to support truth value evaluation. |