La precondizione di un'operazione è una condizione che deve essere soddisfatta prima che l'operazione possa essere eseguita.
La postcondizione di un'operazione è una condizione che deve essere soddisfatta dopo che l'operazione è stata eseguita.
Prendiamo quindi alcune operazioni e deduciamo logicamente le loro pre e postcondizioni.
- Prelievo di denaro dal conto di debito in ATM. La somma che viene prelevata deve essere minore o uguale alla somma che rimane sul conto (1a precondizione) e minore della somma che rimane nel bancomat (2a precondizione). Dopo aver prelevato il denaro, i promemoria del denaro sia nel bancomat che sul conto devono essere uguali ai loro valori originali meno la somma che viene prelevata (2 postcondizioni).
- Sposare una donna. La precondizione è che la donna non sia già sposata (a meno che la poliandria sia legale). La postcondizione è che dopo aver sposato una donna, questa deve diventare sposata (in modo che qualcun altro non la sposi accidentalmente).
- Sposare oggetti dalla pila. Precondizione: il numero di oggetti in pila deve essere maggiore di zero. Postcondizione: il numero di elementi su uno stack dovrebbe essere il suo valore originale meno uno e il valore restituito dovrebbe essere uguale alla cima dello stack.
- Scaricare un file. Condizione preliminare: la memoria di destinazione deve avere abbastanza spazio per il file e il sito di download deve essere accessibile. Postcondizione: lo spazio di archiviazione disponibile dovrebbe diminuire della dimensione del file.
- Mangiare la pizza. Condizione preliminare: c'è la pizza. Postcondizione: non c'è la pizza.