Postbetingelser

Postbetingelser er erklæringer om den tilstand, der skal være opfyldt efter en funktion eller operation er udført. De beskriver, hvilke egenskaber der gælder i resultatet og i ændringerne af tilstanden efter udførelsen. Postbetingelserne står i kontrast til forudsætninger (preconditions), som skal være opfyldt før koden køres. Sammen udgør de en kontrakt for en enhed eller procedure, og de bruges i design by contract (DbC) til at dokumentere og sikre forventet opførsel.

Postbetingelser udtrykkes ofte som krav til returværdien og til ændringer i programtilstanden. I sprog, der understøtter DbC, kaldes de ofte “ensures”-betingelser og kan referere til returnerede værdier, ændringer i objekters tilstand eller opretholdelser af invariants. De kan også anvendes i mere generel form gennem assertioner, som verificerer bestemte egenskaber efter udførelsen.

Et enkelt eksempel: en funktion add(a, b) der returnerer et heltal, kan have postbetingelsen: resultatet er lig med a + b. Dette fastlægger, hvad funktionen garanterer uanset interne detaljer, så læsere og verificeringsværktøjer ved, hvad der forventes.

Fordele ved postbetingelser inkluderer bedre dokumentation af forventet adfærd, lettere vedligeholdelse og mulighed for statisk eller formel verifikation af korrekthed. De giver også støtte til sikker fejlbehandling og simplificerer refaktorering ved at fastholde kontraktlige forventninger.

Begrænsningerne er, at postbetingelser kun beskriver en delmængde af adfærd og kan være udfordrende at opstille i tilstedeværende usikkerheder (f.eks. undtagelser eller ikke-deterministiske indslag). De skal være realistiske og konsekvente med præconditions og invariants.