Cálculo de refinamiento - Refinement calculus

El cálculo de refinamiento es un enfoque formalizado para el refinamiento gradual 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 preservan la corrección en un programa ejecutable eficientemente.

Los proponentes incluyen 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, 2a edición, 1994, ISBN  0-13 -123274-6 ). En el último caso, la motivación fue vincular la notación Z de especificación 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 . En este caso, la preservación del comportamiento significa que cualquier triple de Hoare satisfecho por un programa también debe satisfacerse mediante cualquier refinamiento del mismo, noción que conduce directamente a declaraciones de especificación como condiciones previas y posteriores que se mantienen, por sí solas, para cualquier programa que pueda ser sólido. colocado entre ellos.

Referencias

enlaces externos