El uso de los demostradores automáticos de teoremas para la enseñanza de la programación

La verificación formal de algoritmos, impartida en los estudios de Ingeniería Informática como parte de las asignaturas de programación, se suele explicar de manera “teórica” introduciendo los axiomas de la lógica de Hoare y realizando diversos ejercicios de verificación (a mano) de pequeños programas. Aunque los alumnos han debido adquirir previamente los conocimientos de Lógica necesarios, muchos de ellos presentan serias dificultades para expresar formalmente los distintos pasos de las pruebas de corrección planteadas. En esta experiencia se ha decidido utilizar como herramienta de apoyo para explicar la verificación formal de algoritmos un demostrador automático de teoremas llamado Krakatoa. Esta herramienta permitirá a los estudiantes visualizar de manera interactiva los distintos pasos necesarios para probar la corrección de un programa, reflexionar sobre los razonamientos seguidos y comprender la importancia de la verificación de algoritmos para mejorar la fiabilidad de nuestros programas.Formal verification of algorithms, taught in Computer Engineering studies as part of programming subjects, is usually explained in a “theoretical” way introducing the different axioms of Hoare logic and doing (by hand) various exercises of verification of small programs. Although students are supposed to have previously acquired the necessary logic concepts, many of them have serious difficulties to formally express the different steps of the considered correction proofs. In this experience we have decided to explain formal verification of algorithms by using, as a support tool, an automatic theorem prover called Krakatoa. This tool will allow students to interactively visualize the various steps required to prove the correctness of a program, to think about the used reasoning and to understand the importance of verification of algorithms to improve the reliability of our programs