Postcondizione

In programmazione, una postcondizione è una condizione o un predicato che deve essere sempre vero immediatamente dopo l'esecuzione di una sezione di codice o dopo un'operazione in una specifica formale. Le postcondizioni sono solitamente verificate utilizzando asserzioni all'interno dello stesso codice. Spesso, le postcondizioni sono solo incluse della documentazione del relativo segmento di codice. Ad esempio: il risultato di un fattoriale è sempre un numero intero maggiore o uguale ad 1. Quindi, un programma che calcola il fattoriale di un numero in input avrà come postcondizione che il risultato dopo il calcolo sia un intero e che sia maggiore od uguale ad 1. Un altro esempio: un programma che calcola la radice quadrata di un numero in input deve avere come postcondizioni che il risultato sia un numero e che il suo quadrato sia uguale all'input.