Precondiciones, conjunto de condiciones que se deben dar antes de un cierto punto. Postcondiciones, conjunto de condiciones que se deben dar después de un cierto punto. Invariantes, conjunto de condiciones que se deben dar durante la ejecución de un cierto bloque de instrucciones.