En programación de computadoras , una poscondición es una condición o predicado que siempre debe ser verdadera justo después de la ejecución de alguna sección de código o después de una operación en una especificación formal . A veces, las poscondiciones se prueban mediante afirmaciones dentro del propio código. A menudo, las condiciones posteriores simplemente se incluyen en la documentación de la sección de código afectada.
Por ejemplo: El resultado de un factorial es siempre un número entero y mayor o igual a 1. Entonces, un programa que calcula el factorial de un número de entrada tendría como condiciones posteriores que el resultado después del cálculo sea un número entero y que sea mayor o igual a 1. igual a 1. Otro ejemplo: un programa que calcula la raíz cuadrada de un número de entrada podría tener como condiciones posteriores que el resultado sea un número y que su cuadrado sea igual a la entrada.
En algunos enfoques de diseño de software, las poscondiciones, junto con las precondiciones y las invariantes de clase , son componentes del método de construcción de software diseño por contrato .
La poscondición para cualquier rutina es una declaración de las propiedades que están garantizadas al finalizar la ejecución de la rutina. [1] En lo que respecta al contrato de la rutina, la poscondición ofrece seguridad a los potenciales llamadores de que, en los casos en que la rutina se llama en un estado en el que se cumple su condición previa , las propiedades declaradas por la poscondición están aseguradas.
El siguiente ejemplo escrito en Eiffel establece el valor de un atributo de clase houren función de un argumento proporcionado por la persona que llama a_hour. La poscondición sigue a la palabra clave ensure. En este ejemplo, la poscondición garantiza, en los casos en los que la precondición se cumple (es decir, cuando a_hourrepresenta una hora válida del día), que después de la ejecución de set_hour, el atributo de clase hourtendrá el mismo valor que a_hour. La etiqueta " hour_set:" describe esta cláusula de poscondición y sirve para identificarla en caso de una violación de la poscondición en tiempo de ejecución.
set_hour ( a_hour : INTEGER ) - Establecer `hora' en `a_hour' requiere valid_argument : 0 <= a_hour y a_hour <= 23 do hour := a_hour asegurar hour_set : hora = a_hour end En presencia de herencia , las rutinas heredadas por las clases descendientes (subclases) lo hacen con sus contratos, es decir, sus precondiciones y postcondiciones, vigentes. Esto significa que cualquier implementación o redefinición de rutinas heredadas también debe escribirse para cumplir con sus contratos heredados. Las poscondiciones pueden modificarse en rutinas redefinidas, pero sólo pueden reforzarse. [2] Es decir, la rutina redefinida puede aumentar los beneficios que proporciona al cliente, pero no puede disminuir esos beneficios.