Forms of Correctness
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