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

• Must give formal specifications (pre-conditions and post-conditions)
• 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