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. |