En ciencias de la computación , la derivación del programa es la derivación de un programa a partir de su especificación, por medios matemáticos.
Para obtener un medio de programa para escribir una especificación formal, que es por lo general no ejecutable, y luego aplicar reglas matemáticamente correctos con el fin de obtener un programa ejecutable satisfacer esa especificación. El programa así obtenido es entonces correcto por construcción. El programa y la prueba de corrección se construyen juntos.
El enfoque que se suele adoptar en la verificación formal es escribir primero un programa y luego proporcionar una prueba de que se ajusta a una especificación determinada . Los principales problemas con esto son que
- la prueba resultante suele ser larga y engorrosa;
- no se da una idea de cómo se desarrolló el programa; parece "como un conejo sacado de un sombrero";
- si el programa resultara incorrecto de alguna manera sutil, es probable que el intento de verificarlo sea largo y seguro que será infructuoso.
La derivación del programa intenta remediar estas deficiencias mediante
- mantener las pruebas más breves, mediante el desarrollo de notaciones matemáticas apropiadas;
- tomar decisiones de diseño mediante la manipulación formal de la especificación.
Los términos que son aproximadamente sinónimos de derivación de programas son: programación transformacional, algorítmica, programación deductiva.
El formalismo Bird-Meertens es un enfoque para la derivación de programas.
Ver también
Referencias
- Edsger W. Dijkstra , Wim HJ Feijen, A Method of Programming , Addison-Wesley, 1988, 188 páginas
- Edward Cohen, Programación en la década de 1990 , Springer-Verlag, 1990
- Anne Kaldewaij, Programación: La derivación de algoritmos , Prentice-Hall, 1990, 216 páginas
- David Gries, La ciencia de la programación , Springer-Verlag, 1981, 350 páginas
- Carroll Morgan (científico de la computación) , Programación a partir de especificaciones , Serie Internacional en Ciencias de la Computación (2a ed.), Prentice-Hall, 1998.
- Eric CR Hehner , una teoría práctica de la programación , 2008, 235 páginas
- AJM van Gasteren. Sobre la forma de los argumentos matemáticos . Lecture Notes in Computer Science # 445, Springer-Verlag, 1990. Enseña cómo escribir pruebas con claridad y precisión.
- Martin Rem. "Small Programming Exercises", apareció en Science of Computer Programming , Vol. 3 (1983) a Vol. 14 (1990).
- Roland Backhouse. Construcción del programa: cálculo de implementaciones a partir de especificaciones . Wiley, 2003. ISBN 978-0-470-84882-1 .
- Derrick G. Kourie, Bruce W. Watson. El enfoque de la programación de corrección por construcción . Springer-Verlag, 2012. ISBN 978-3-642-27919-5 . Proporciona una explicación paso a paso de cómo derivar algoritmos matemáticamente correctos utilizando refinamientos pequeños y manejables.