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 . En ocasiones, las poscondiciones 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. Por lo tanto, 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 igual a 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 la 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 para cualquier rutina es una declaración de las propiedades que están garantizadas al completar la ejecución de la rutina. [1] En lo que respecta al contrato de la rutina, la condición posterior ofrece seguridad a los potenciales llamadores de que, en los casos en los que la rutina se llama en un estado en el que se cumple su condición previa , las propiedades declaradas por la condición posterior están aseguradas.
Ejemplo de Eiffel
El siguiente ejemplo escrito en Eiffel establece el valor de un atributo de clase hour
basado en un argumento proporcionado por la persona que llama a_hour
. La poscondición sigue a la palabra clave ensure
. En este ejemplo, la condición a_hour
posterior garantiza, en los casos en que la condición previa se cumple (es decir, cuando representa una hora válida del día), que después de la ejecución de set_hour
, el atributo de clase hour
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 infracción de condición posterior en tiempo de ejecución.
set_hour ( a_hour : INTEGER ) - Establecer `hour 'en` a_hour' require valid_argument : 0 <= a_hour y a_hour <= 23 do hour : = a_hour asegurar hour_set : hour = a_hour end
Poscondiciones y herencia
En presencia de herencia , las rutinas heredadas por clases descendientes (subclases) lo hacen con sus contratos, es decir, sus precondiciones y poscondiciones, vigentes. 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 pueden modificarse en rutinas redefinidas, pero solo pueden fortalecerse. [2] Es decir, la rutina redefinida puede aumentar los beneficios que brinda al cliente, pero no puede disminuir esos beneficios.
Ver también
- Condición previa
- Diseño por contrato
- Lógica hoare
- Invariantes mantenidos por condiciones
- Activador de base de datos
Referencias
- ^ Meyer, Bertrand , Construcción de software orientado a objetos , segunda edición, Prentice Hall, 1997, p. 342.
- ^ Meyer, 1997, págs. 570–573.