{"id":3443,"date":"2013-07-26T04:20:34","date_gmt":"2013-07-26T04:20:34","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3443"},"modified":"2013-07-26T04:21:50","modified_gmt":"2013-07-26T04:21:50","slug":"resena-el-uso-de-los-demostradores-automaticos-de-teoremas-para-la-ensenanza-de-la-programacion","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-el-uso-de-los-demostradores-automaticos-de-teoremas-para-la-ensenanza-de-la-programacion\/","title":{"rendered":"Rese\u00f1a: El uso de los demostradores autom\u00e1ticos de teoremas para la ense\u00f1anza de la programaci\u00f3n"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobre el uso de <a href=\"http:\/\/krakatoa.lri.fr\">Krakatoa<\/a> en la ense\u00f1anza titulado <a href=\"http:\/\/bioinfo.uib.es\/~joemiro\/aenui\/procJenui\/Jen2013\/p25.rom_elus.pdf\">El uso de los demostradores autom\u00e1ticos de teoremas para la ense\u00f1anza de la programaci\u00f3n<\/a>.<\/p>\n<p>Su autora es <a href=\"http:\/\/www.unirioja.es\/cu\/anromero\">Ana Romero<\/a> (de la Universidad de la Rioja) y lo ha presentado en la <a href=\"http:\/\/jenui2013.uji.es\">Jenui 2013<\/a> (<i>XIX Jornadas sobre la Ense\u00f1anza Universitaria de la Inform\u00e1tica<\/i>).<\/p>\n<p> Su resumen es<\/p>\n<blockquote><p>\nLa verificaci\u00f3n formal de algoritmos, impartida en los estudios de Ingenier\u00eda Inform\u00e1tica como parte de las asignaturas de programaci\u00f3n, se suele explicar de manera \u201cte\u00f3rica\u201d introduciendo los axiomas de la l\u00f3gica de Hoare y realizando diversos ejercicios de verificaci\u00f3n (a mano) de peque\u00f1os programas. Aunque los alumnos han debido adquirir previamente los conocimientos de L\u00f3gica necesarios, muchos de ellos presentan serias dificultades para expresar formalmente los distintos pasos de las pruebas de correcci\u00f3n planteadas. En esta experiencia se ha decidido utilizar como herramienta de apoyo para explicar la verificaci\u00f3n formal de algoritmos un demostrador autom\u00e1tico de teoremas llamado Krakatoa. Esta herramienta permitir\u00e1 a los estudiantes visualizar de manera interactiva los distintos pasos necesarios para probar la correcci\u00f3n de un programa, reflexionar sobre los razonamientos seguidos y comprender la importancia de la verificaci\u00f3n de algoritmos para mejorar la fiabilidad de nuestros programas.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre el uso de Krakatoa en la ense\u00f1anza titulado El uso de los demostradores autom\u00e1ticos de teoremas para la ense\u00f1anza de la programaci\u00f3n. Su autora es Ana Romero (de la Universidad de la Rioja) y lo ha presentado en la Jenui 2013 (XIX Jornadas sobre la Ense\u00f1anza Universitaria de la&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[213,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3443"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=3443"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3443\/revisions"}],"predecessor-version":[{"id":3445,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3443\/revisions\/3445"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3443"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3443"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3443"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}