Mostra el registre d'ítem simple
El Uso de los demostradores automáticos de teoremas para la enseñanza de la programación
dc.contributor.author | Romero, Ana |
dc.date.accessioned | 2014-10-13T08:21:14Z |
dc.date.available | 2014-10-13T08:21:14Z |
dc.date.issued | 2013-07-10 |
dc.identifier.citation | Romero, Ana. El Uso de los demostradores automáticos de teoremas para la enseñanza de la programación. A: JENUI. "Jornadas de Enseñanza Universitaria de la Informática (19es: 2013: Castelló de la Plana)". Castelló de la Plana: Universitat Jaume I. Escola Superior de Tecnologia i Ciències Experimentals, 2013. |
dc.identifier.isbn | 978-84-695-8051-6 |
dc.identifier.uri | http://hdl.handle.net/2099/15367 |
dc.description.abstract | 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. |
dc.description.abstract | SUMMARY -- 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 verificacion 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. |
dc.format.extent | 8 p. |
dc.language.iso | spa |
dc.publisher | Universitat Jaume I. Escola Superior de Tecnologia i Ciències Experimentals |
dc.relation.ispartof | Jornadas de Enseñanza Universitaria de la Informática (19es: 2013: Castelló de la Plana) |
dc.rights | Attribution-NonCommercial-NoDerivs 3.0 Spain |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/3.0/es/ |
dc.subject | Àrees temàtiques de la UPC::Informàtica |
dc.subject | Àrees temàtiques de la UPC::Ensenyament i aprenentatge |
dc.subject.lcsh | Computer science -- Study and teaching |
dc.subject.other | Verificación formal de algoritmos |
dc.subject.other | Krakatoa |
dc.subject.other | Pruebas de corrección |
dc.subject.other | Demostradores automáticos de teoremas |
dc.title | El Uso de los demostradores automáticos de teoremas para la enseñanza de la programación |
dc.type | Conference report |
dc.subject.lemac | Informàtica -- Ensenyament |
dc.rights.access | Open Access |
local.citation.author | Romero, Ana |
local.citation.contributor | JENUI |
local.citation.pubplace | Castelló de la Plana |
local.citation.publicationName | Jornadas de Enseñanza Universitaria de la Informática (19es: 2013: Castelló de la Plana) |
Fitxers d'aquest items
Aquest ítem apareix a les col·leccions següents
-
JENUI 2013 [44]
Castelló de la Plana, 10-12 julio de 2013