La precondición de una operación es una condición que debe ser satisfecha antes de que la operación pueda ser realizada.
La postcondición de una operación es una condición que debe ser satisfecha después de que la operación haya sido realizada.
Entonces, tomemos algunas operaciones y deduzcamos lógicamente sus pre y postcondiciones.
- Retirar dinero de la cuenta de débito en el cajero automático. La suma que se retira debe ser menor o igual que la suma que queda en la cuenta (1ª precondición) y menor que la suma que queda en el cajero (2ª precondición). Después de retirar el dinero, los recordatorios de dinero tanto en el cajero como en la cuenta deben ser iguales a sus valores originales menos la suma que se retira (2 postcondiciones).
- Casarse con una mujer. La precondición es que la mujer no debe estar ya casada (a menos que la poliandria sea legal). La postcondición es que después de casarse una mujer debe casarse (para que otra persona no se case accidentalmente con ella).
- Sacar elementos de la pila. Precondición: el número de elementos en una pila debe ser mayor que cero. Postcondición: el número de elementos en una pila debe ser su valor original menos uno y el valor devuelto debe ser igual a la parte superior de la pila.
- Descargar un archivo. Precondición: el almacenamiento de destino debe tener suficiente espacio para el archivo y el sitio de descarga debe ser accesible. Postcondición: el almacenamiento disponible debe disminuir en el tamaño del archivo.
- Comer pizza. Precondición: hay pizza. Postcondición: no hay pizza.