"Forks without philosophers" o de cómo la cuantificación universal perdió una batalla y de las ventajas que ello reportó

Abstract

En sentido general, este trabajo trata sobre la construcción formal de programas. La necesidad de construir los programas formalmente ha sido ampliamente discutida a lo largo de los últimos años, y ha adquirido una importancia cada vez mayor. En los comienzos, la programación se realizaba de una forma intuitiva, casi se podría decir artística; con el correr de los años se comprobó que los métodos utilizados eran inadecuados, por lo que se desarrollaron nuevas técnicas, mediante las cuales un programa debía ser diseñado al mismo tiempo que la prueba de su corrección. Quizás la mejor metáfora para describir la necesidad de formalidad es la que D’Argenio describe en el prefacio de su tesis de grado, donde compara a los programas con moscas, y a los métodos formales con una máquina mata-moscas; si los programadores utilizasen sus zapatos para aplastar las moscas (no utilizando los métodos formales, sino la intuición), sucedería lo que se cita en el epígrafe. Es por ello que se hace tanto hincapié en la investigación de métodos que permitan un tratamiento formal del proceso de desarrollo de software, o bien para la construcción, o bien para la especificación y verificación. En esta tesis utilizaremos un método de construcción que consiste en realizar transformaciones sobre una especificación hasta obtener un programa que la satisfaga.