Reseña: El uso de los demostradores automáticos de teoremas para la enseñanza de la programación
Se ha publicado un artículo sobre el uso de Krakatoa en la enseñanza titulado El uso de los demostradores automáticos de teoremas para la enseñanza de la programación.
Su autora es Ana Romero (de la Universidad de la Rioja) y lo ha presentado en la Jenui 2013 (XIX Jornadas sobre la Enseñanza Universitaria de la Informática).
Su resumen es
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.