From Program Test to Program Proof

Lecture overview -- Keyboard shortcut: 'u'

Previous page: Test Utopia -- Keyboard shortcut: 'p'

Next page: White Box Testing [Section] -- Keyboard shortcut: 'n'

Lecture notes - all slides together

Annotated slide -- Keyboard shortcut: 't'

Textbook -- Keyboard shortcut: 'v'

Alphabetic index

Help page about these notes

Test of Object-oriented Programs - slide 6 : 35

From Program Test to Program Proof

A mathematical program proof is an alternative to program testing

Program proofs
- Prove that the postcondition of the program is true, given that
  - The precondition of the program is true
  - The program terminates
- Relies on
  - A decoration of the program with mathematical assertions which reflect the intended result of the program relative to the initial program assumptions
  - Proof rules for all constructs of the program

Manually performed program proofs are likely to have more errors in the proof than in the program

Therefore only automatic program proofs will improve our confidence