En programación informática , una precondición es una condición o predicado que siempre debe ser verdadero justo antes de la ejecución de alguna sección de código o antes de una operación en una especificación formal .
Si se viola una condición previa, el efecto de la sección de código se vuelve indefinido y, por lo tanto, puede o no realizar el trabajo previsto. Las condiciones previas que faltan, son insuficientes o no se han demostrado formalmente (o se ha intentado demostrarlas incorrectamente), o que no se comprueban de forma estática o dinámica, pueden dar lugar a problemas de seguridad , en particular en lenguajes no seguros que no están fuertemente tipados.
A menudo, las condiciones previas se incluyen simplemente en la documentación de la sección de código afectada. A veces, las condiciones previas se prueban utilizando protecciones o afirmaciones dentro del propio código, y algunos lenguajes tienen construcciones sintácticas específicas para hacerlo.
La función factorial solo se define cuando su parámetro es un entero mayor o igual a cero. Por lo tanto, una implementación de la función factorial tendría como condición previa que su parámetro sea un entero y que el parámetro sea mayor o igual a cero. Alternativamente, se puede utilizar el sistema de tipos del lenguaje para especificar que el parámetro de la función factorial es un número natural (entero sin signo), lo que se puede verificar formalmente de manera automática mediante el verificador de tipos de un compilador.
Además, cuando los tipos numéricos tienen un rango limitado (como ocurre en la mayoría de los lenguajes de programación), la condición previa también debe especificar el valor máximo que puede tener el parámetro para que no se produzca un desbordamiento (por ejemplo, si una implementación de factorial devuelve el resultado en un entero sin signo de 64 bits, entonces el parámetro debe ser menor que 21 porque factorial(21) es mayor que el entero sin signo máximo que se puede almacenar en 64 bits). Cuando el lenguaje admite subtipos de rango (por ejemplo, Ada ), el sistema de tipos puede verificar automáticamente dichas restricciones. Las restricciones más complejas se pueden verificar formalmente de forma interactiva con un asistente de prueba .
Las condiciones previas en el desarrollo de software orientado a objetos son una parte esencial del diseño por contrato . El diseño por contrato también incluye nociones de poscondición e invariante de clase .
La condición previa de cualquier rutina define las restricciones sobre el estado del objeto que son necesarias para una ejecución exitosa. Desde el punto de vista del desarrollador del programa, esto constituye la parte del contrato correspondiente al invocador de la rutina. El invocador está obligado entonces a garantizar que la condición previa se cumpla antes de invocar la rutina. La recompensa por el esfuerzo del invocador se expresa en la condición posterior de la rutina invocada . [1]
La rutina del siguiente ejemplo escrita en Eiffel toma como argumento un entero que debe ser un valor válido para una hora del día, es decir, de 0 a 23, inclusive. La condición previa sigue a la palabra clave require. Especifica que el argumento debe ser mayor o igual a cero y menor o igual a 23. La etiqueta " valid_argument:" describe esta cláusula de condición previa y sirve para identificarla en caso de una violación de la condición previa en tiempo de ejecución.
set_hour ( a_hour : INTEGER ) -- Establece `hora' en `a_hour' require valid_argument : 0 <= a_hour y a_hour <= 23 do hour := a_hour ensure hour_set : hour = a_hour end En presencia de herencia, las rutinas heredadas por las clases descendientes (subclases) lo hacen con sus precondiciones vigentes. Esto significa que cualquier implementación o redefinición de rutinas heredadas también debe escribirse para cumplir con su contrato heredado. Las precondiciones pueden modificarse en rutinas redefinidas, pero solo pueden debilitarse. [2] Es decir, la rutina redefinida puede disminuir la obligación del cliente, pero no aumentarla.