En programación informática , una poscondición es una condición o predicado que siempre debe ser verdadero 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 . Las poscondiciones a veces se prueban utilizando afirmaciones dentro del propio código. A menudo, las poscondiciones 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. Por lo tanto, un programa que calcula el factorial de un número de entrada tendría como poscondiciones que el resultado después del cálculo sea un número entero y que sea mayor o igual a 1. Otro ejemplo: un programa que calcula la raíz cuadrada de un número de entrada podría tener como poscondiciones 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 de cualquier rutina es una declaración de las propiedades que se garantizan al completarse la ejecución de la rutina. [1] En relación con el contrato de la rutina, la poscondición ofrece garantías a los posibles invocadores de que, en los casos en que la rutina se invoca 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 el llamador a_hour. La condición posterior sigue a la palabra clave ensure. En este ejemplo, la condición posterior garantiza, en los casos en los que se cumple la condición previa (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 condición posterior y sirve para identificarla en caso de una violación de la condición posterior 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 contratos, es decir, sus precondiciones y postcondiciones, en vigor. Esto significa que cualquier implementación o redefinición de rutinas heredadas también tiene que ser escrita para cumplir con sus contratos heredados. Las postcondiciones pueden ser modificadas en rutinas redefinidas, pero solo pueden ser fortalecidas. [2] Es decir, la rutina redefinida puede aumentar los beneficios que proporciona al cliente, pero no puede disminuir esos beneficios.