Programbevis

Lecture overview -- Keyboard shortcut: 'u'

Previous page: Testutopi -- Keyboard shortcut: 'p'

Next page: White box testteknik [Section] -- Keyboard shortcut: 'n'

Lecture notes - all slides and notes together

Annotated slide -- Keyboard shortcut: 't'

Test og Dokumentation - slide 6 : 46

Programbevis

Et programbevis er et alternativ til en totaltest af et program

Programbeviser:
- Matematisk bevis for at 'programmets postbetingelse' er opfyldt efter programudførelsen såfremt:
  - programmets prebetingelse holder før programudførelsen
  - programmet terminerer
- Forudsætter at programmet er specificeret, således at programmet kan bevises relativt til specifikationen
  - Specifikation med logiske udtryk (assertions) er det sædvanlige grundlag for programbeviser
  - I praksis bliver man nødt til også at kalkulere med fejl i specifikationen og fejl i programbeviset

Et programbevis er så kompliceret at gennemføre, at det nødvendigvis skal automatiseres for at vi kan have tiltro til resultatet af beviset ('korrekt' eller 'ukorrekt')

Programbeviser af 'virkelige programmer' er stadigvæk på kanten af det praktisk gennemførbare