Program Verification
Approach generates a mathematical proof that the program works for all
possible inputs.

Must give formal specifications (preconditions and postconditions)

Rules of logic analyze correctness at each stage of processing

Some notable successes with this approach, BUT

Automating the process of program verification would show that the program
stopped in every valid circumstance, and so would solve the Halting Problem
Limitation: Program Verification can produce helpful results, but
the process of checking the correctness of programs in all cases
cannot be fully automated.
created: 3 January 2007
last revised: 7 January 2007

previous next

