El cálculo de refinamiento es un método formalizado para el refinamiento gradual de 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 preservan la corrección hasta convertirse en un programa ejecutable de manera eficiente. [1]
Entre los defensores de esta metodología se encuentran Ralph-Johan Back , que la originó en su tesis doctoral de 1978, On the Correctness of Refinement Steps in Program Development , y Carroll Morgan , especialmente con su libro Programming from Specification (Prentice Hall, 2.ª edición, 1994, ISBN 0-13-123274-6 ). En este ú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 , con una notación de programación ejecutable basada en el lenguaje de comandos guardados de Dijkstra . La preservación del comportamiento en este caso significa que cualquier triple de Hoare satisfecho por un programa también debería ser satisfecho por cualquier refinamiento del mismo, lo que conduce directamente a las declaraciones de especificación como condiciones previas y posteriores que se mantienen, por sí mismas, para cualquier programa que pudiera colocarse sólidamente entre ellas.