El cálculo de refinamiento es un enfoque formalizado para el refinamiento paso a paso para la construcción de programas. El comportamiento requerido del programa ejecutable final se especifica como un "programa" abstracto y quizás no ejecutable, que luego se refina mediante una serie de transformaciones que conservan la corrección en un programa ejecutable de manera eficiente. [1]
Los defensores incluyen a Ralph-Johan Back , quien originó el enfoque en su tesis doctoral de 1978 Sobre la corrección de los pasos de refinamiento en el desarrollo de programas , y Carroll Morgan , especialmente con su libro Programación a partir de especificaciones (Prentice Hall, 2ª edición, 1994, ISBN 0-13 -123274-6 ). En el último caso, la motivación era vincular la notación de especificación Z de Abrial , a través de una relación rigurosa de refinamiento del programa que preserva el comportamiento , a una notación de programación ejecutable basada en el lenguaje de comandos protegidos de Dijkstra . Preservación del comportamientoen este caso significa que cualquier triple de Hoare satisfecho por un programa también debería ser satisfecho por cualquier refinamiento del mismo, cuya noción conduce directamente a declaraciones de especificación como condiciones previas y posteriores, por sí mismas, para cualquier programa que podría colocarse entre ellas. .