l
The
main forms of correctness are:
lPartial
Correctness (PC):
lIf the input
assertion is satisfied when the program starts and the program eventually terminates, then the output
assertion will be satisfied
upon termination.
lTermination:
lIf the input
assertion is satisfied, then the program will eventually terminate
lTotal
Correctness (TC):
ldefined to be PC + termination