Formal correctness proofs are intricate even
for fairly simple programs.
How formal correctness proofs can be used in
practice?
ANSWER: We need not go through a complete
specification and its correctness proofs to
assess the program.
If there are critical facts that we want
to verify, then we may specify and analyzep
ONLY THAT PART in a formal way.
For a program module, the assertions:
pre-conditions and
post-conditions
are be used in correctness proofs, and
informally used in debugging.
Last but not least, automated tools will
help in correctness proofs.