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  slide -- Keyboard shortcut: 't'  Help page about these notes  Alphabetic index  Course home  Page 6 : 46
Forelæsningsnoter i Objekt-orienteret Programmering
Test og Dokumentation
Programbevis

Et programbevis er et matematisk ræsonnement som overbeviser os om korrektheden af et program. Dette står i modsætning til en test, som er en empirisk sandsynliggørelse af, at der ikke er fejl i programmet. Vi ser, at der er tale om to vidt forskellige aktiviteter

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

Den form for bevis, vi diskuterer her, kaldes partiel korrekthed. Årsagen er at vi forudsætter at programmet terminerer (kører til ende). Hvis vi ikke forudsætter terminering taler vi om en endnu stærkere form for korrekthed, nemlig total korrekthed

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