Postcondición

Este artículo o sección necesita referencias que aparezcan en una publicación acreditada.
Busca fuentes: «Postcondición» – noticias · libros · académico · imágenes

Este aviso fue puesto el 11 de enero de 2013.

En programación, una postcondición es una condición o predicado lógico que siempre debe cumplirse justamente después de la ejecución de una sección de código o de una operación (especificación formal). Las postcondiciones se prueban a veces mediante aserciones incluidas en el código. A menudo, las postcondiciones se incluyen simplemente en la documentación de la correspondiente sección de código.

Por ejemplo: el resultado de un factorial es siempre un entero mayor o igual que 1. De este modo un programa que calcula el factorial de un número dado tendría como postcondiciones que el resultado debe ser un entero y que este debe ser mayor o igual que 1.