En informática , la derivación de programas es la derivación de un programa a partir de su especificación, por medios matemáticos.
Derivar un programa significa escribir una especificación formal , que normalmente no es ejecutable, y luego aplicar reglas matemáticamente correctas para obtener un programa ejecutable que satisfaga esa especificación. El programa así obtenido es 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 consiste en escribir primero un programa y luego proporcionar una prueba de que cumple una especificación determinada . Los principales problemas que esto presenta son los siguientes:
- La prueba resultante suele ser larga y engorrosa;
- No se da ninguna idea de cómo se desarrolló el programa; parece "un conejo salido de un sombrero";
- Si el programa resulta ser incorrecto de alguna manera sutil, el intento de verificarlo probablemente será largo y con toda seguridad infructuoso.
La derivación de programas intenta remediar estas deficiencias mediante:
- mantener las pruebas más breves, mediante el desarrollo de notaciones matemáticas apropiadas;
- tomar decisiones de diseño a través de la manipulación formal de la especificación.
Términos que son aproximadamente sinónimos de derivación de programas son: programación transformacional, algorítmica, programación deductiva.
El formalismo de Bird-Meertens es un enfoque para la derivación de programas.
Los enfoques para lograr la corrección en la computación distribuida incluyen lenguajes de investigación como el lenguaje de programación P.
Véase también
Referencias
- Edsger W. Dijkstra , Wim HJ Feijen, Un método de programación , Addison-Wesley, 1988, 188 páginas
- Edward Cohen, Programación en los años 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 informático) , Programación a partir de especificaciones, Serie internacional en ciencias de la computación (2.ª 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 demostraciones con claridad y precisión.
- Martin Rem. "Pequeños ejercicios de programación", publicado en Science of Computer Programming , vol. 3 (1983) a vol. 14 (1990).
- Roland Backhouse. Construcción de programas: cálculo de implementaciones a partir de especificaciones . Wiley, 2003. ISBN 978-0-470-84882-1 .
- Derrick G. Kourie, Bruce W. Watson. The Correctness-by-Construction Approach to Programming (El enfoque de corrección por construcción para la programació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 mediante pequeños y manejables refinamientos.
