- 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 |