{"id":71031,"date":"2018-03-09T23:15:32","date_gmt":"2018-03-09T23:15:32","guid":{"rendered":"https:\/\/www.deberes.net\/tesis\/sin-categoria\/estudio-de-la-verificacion-de-propiedades-de-programas-funcionales-de-las-pruebas-manuales-al-uso-de-asistentes-de-pruebas\/"},"modified":"2018-03-09T23:15:32","modified_gmt":"2018-03-09T23:15:32","slug":"estudio-de-la-verificacion-de-propiedades-de-programas-funcionales-de-las-pruebas-manuales-al-uso-de-asistentes-de-pruebas","status":"publish","type":"post","link":"https:\/\/www.deberes.net\/tesis\/matematicas\/estudio-de-la-verificacion-de-propiedades-de-programas-funcionales-de-las-pruebas-manuales-al-uso-de-asistentes-de-pruebas\/","title":{"rendered":"Estudio de la verificacion de propiedades de programas funcionales de las pruebas manuales al uso de asistentes de pruebas"},"content":{"rendered":"<h2>Tesis doctoral de <strong>  Jorge Castro Jos\u00e9 Santiago <\/strong><\/h2>\n<p>El principal objetivo de esta tesis es la investigaci\u00f3n de una metodolog\u00eda para producir software certificado, desde pruebas manuales hasta el uso de asistentes que supervisan y colaboran en el proceso de prueba. Estudiaremos el desarrollo de algoritmos probados formalmente para la computaci\u00f3n, explicando c\u00f3mo demostrar que una implementaci\u00f3n de un algoritmo cumple las propiedades esperadas, realizando este examen en base al estudio de distintos ejemplos en orden creciente de complejidad, teniendo en cuenta no s\u00f3lo la certificaci\u00f3n de los programas sino tambien de su eficiencia.  para cada uno de estos programas, presentamos en primer lugar, todas las definiciones y demostraciones de propiedades con pruebas hechas a mano en un estilo riguroso, donde cada paso est\u00e1 justificado por razonamiento matem\u00e1tico, y a continuaci\u00f3n presentamos una transformaci\u00f3n de la formalizaci\u00f3n de estas definiciones y pruebas a otras equivalentes en el sistema de pruebas coq. Como otros probadores de teoremas, este sistema proporciona control y asistencia durante los procesos de especificaci\u00f3n y prueba; por tanto evita errores que podr\u00edan introducirse en una prueba a mano. El asistente de pruebas coq es una implementaci\u00f3n del c\u00e1lculo de construcciones inductivas que es una teor\u00eda de tipos resultante de la combinaci\u00f3n de la teor\u00eda intuicionista de tipos de martin lof y el c\u00e1lculo polim\u00f3rfico de girard, fw. La teor\u00eda constructiva de tipos guarda similitudes con los lenguajes de programaci\u00f3n. la prueba de un teorema es una funci\u00f3n que a partir de las pruebas de las hip\u00f3tesis del teorema, calcula la prueba del enunciado. As\u00ed, las formalizaciones de los algoritmos en coq son compilables eficientemente us\u00e1ndose para la computaci\u00f3n.  las t\u00e9cnicas propuestas quedar\u00e1n ejemplificadas sobre programas no triviales, donde se describen formalmente los principios b\u00e1sico que hacen a estos algoritmos funcionar, quedando manifiesta la posibilidad de<\/p>\n<p>&nbsp;<\/p>\n<h3>Datos acad\u00e9micos de la tesis doctoral \u00ab<strong>Estudio de la verificacion de propiedades de programas funcionales de las pruebas manuales al uso de asistentes de pruebas<\/strong>\u00ab<\/h3>\n<ul>\n<li><strong>T\u00edtulo de la tesis:<\/strong>\u00a0 Estudio de la verificacion de propiedades de programas funcionales de las pruebas manuales al uso de asistentes de pruebas <\/li>\n<li><strong>Autor:<\/strong>\u00a0  Jorge Castro Jos\u00e9 Santiago <\/li>\n<li><strong>Universidad:<\/strong>\u00a0 A coru\u00f1a<\/li>\n<li><strong>Fecha de lectura de la tesis:<\/strong>\u00a0 29\/10\/2004<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<h3>Direcci\u00f3n y tribunal<\/h3>\n<ul>\n<li><strong>Director de la tesis<\/strong>\n<ul>\n<li> Freire Nistal Jos\u00e9 Luis<\/li>\n<\/ul>\n<\/li>\n<li><strong>Tribunal<\/strong>\n<ul>\n<li>Presidente del tribunal: roberto Moreno diaz <\/li>\n<li>Juan Llovet verdugo (vocal)<\/li>\n<li>Antonio Blanco ferro (vocal)<\/li>\n<li>Fernando Martin rubio (vocal)<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Tesis doctoral de Jorge Castro Jos\u00e9 Santiago El principal objetivo de esta tesis es la investigaci\u00f3n de una metodolog\u00eda para [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"site-sidebar-layout":"default","site-content-layout":"","ast-site-content-layout":"","site-content-style":"default","site-sidebar-style":"default","ast-global-header-display":"","ast-banner-title-visibility":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","astra-migrate-meta-layouts":"default","ast-page-background-enabled":"default","ast-page-background-meta":{"desktop":{"background-color":"var(--ast-global-color-4)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"ast-content-background-meta":{"desktop":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"tablet":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""},"mobile":{"background-color":"var(--ast-global-color-5)","background-image":"","background-repeat":"repeat","background-position":"center center","background-size":"auto","background-attachment":"scroll","background-type":"","background-media":"","overlay-type":"","overlay-color":"","overlay-gradient":""}},"footnotes":""},"categories":[18576,1890,13880,126,6473],"tags":[16154,4013,10525,154907,26353,16647],"class_list":["post-71031","post","type-post","status-publish","format-standard","hentry","category-a-coruna","category-ciencia-de-los-ordenadores","category-informatica","category-matematicas","category-teoria-de-la-programacion","tag-antonio-blanco-ferro","tag-fernando-martin-rubio","tag-freire-nistal-jose-luis","tag-jorge-castro-jose-santiago","tag-juan-llovet-verdugo","tag-roberto-moreno-diaz"],"_links":{"self":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/71031","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/comments?post=71031"}],"version-history":[{"count":0,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/posts\/71031\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/media?parent=71031"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/categories?post=71031"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.deberes.net\/tesis\/wp-json\/wp\/v2\/tags?post=71031"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}