Poscondición

En programación informática, una postcondición es una condición o predicado que siempre debe ser cierto 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 condiciones posteriores a veces se prueban utilizando aserciones 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 condiciones posteriores de que el resultado después del cálculo sea un número entero y que sea mayor o igual que 1. Otro ejemplo: un programa que calcula la raíz cuadrada de un número de entrada puede tener las condiciones posteriores de que el resultado sea un número y que su cuadrado sea igual a la entrada.

Postcondiciones en programación orientada a objetos

En algunos enfoques de diseño de software, las condiciones posteriores, junto con las condiciones previas y las invariantes de clase, son componentes del diseño del método de construcción de software por contrato.

La condición posterior de cualquier rutina es una declaración de las propiedades que se garantizan al finalizar la ejecución de la rutina. En lo que se refiere al contrato de la rutina, la poscondición ofrece seguridad a los posibles llamantes de que, en los casos en los que se llama a la rutina en un estado en el que se cumple su precondición, las propiedades declaradas por la poscondición están aseguradas.

Ejemplo de Eiffel

El siguiente ejemplo escrito en Eiffel establece el valor de un atributo de clase hora basado en un argumento proporcionado por la persona que llama a_hour. La condición posterior sigue a la palabra clave ensure. En este ejemplo, la poscondición garantiza, en los casos en los que se cumple la precondición (es decir, cuando a_hour representa una hora válida del día), que después de la ejecución de set_hour, el atributo de clase hora tendrá 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 condición posterior en tiempo de ejecución.

 set_hour ()a horas: INTEGER) -- Set `hour' to `a_hour ' necesidad valid_argument: 0 . a horas y a horas . 23 do hora := a horas asegurar hour_set: hora = a horas final

Postcondiciones y herencia

En presencia de herencia, las rutinas heredadas por las clases descendientes (subclases) lo hacen con sus contratos, es decir, sus condiciones previas y posteriores, en vigor. Esto significa que cualquier implementación o redefinición de rutinas heredadas también debe escribirse para cumplir con sus contratos heredados. Las condiciones posteriores se pueden modificar en rutinas redefinidas, pero solo se pueden fortalecer. Es decir, la rutina redefinida puede aumentar los beneficios que brinda al cliente, pero no puede disminuir esos beneficios.