Cálculo de refinamiento

El cálculo de refinamiento es un enfoque formalizado para el refinamiento por etapas en la construcción de programas. El comportamiento requerido del programa ejecutable final se especifica como un "programa" abstracto y posiblemente no ejecutable, que luego se refina mediante una serie de transformaciones que preservan la corrección hasta convertirlo en un programa ejecutable de manera eficiente. ^{[ 1 ]}

Entre sus defensores se encuentran Ralph-Johan Back , quien originó este enfoque en su tesis doctoral de 1978 titulada " 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-6En este último caso, la motivación era vincular la notación de especificación Z de Abrial , mediante una relación rigurosa de refinamiento de programas que preserva el comportamiento , con una notación de programación ejecutable basada en el lenguaje de comandos protegidos de Dijkstra . Preservar el comportamiento en este caso significa que cualquier triple de Hoare satisfecha por un programa también debería ser satisfecha por cualquier refinamiento del mismo, noción que conduce directamente a declaraciones de especificación como precondiciones y postcondiciones que existen por sí mismas para cualquier programa que pueda ubicarse sólidamente entre ellas.