Implementación de métodos de verificación de programas

Chicharro García, Rafael (2009). Implementación de métodos de verificación de programas. Proyecto Fin de Carrera / Trabajo Fin de Grado, Facultad de Informática (UPM) [antigua denominación].

Descripción

Título: Implementación de métodos de verificación de programas
Autor/es:
  • Chicharro García, Rafael
Director/es:
  • Laita de la Rica, Luis M.
Tipo de Documento: Proyecto Fin de Carrera/Grado
Fecha: 2009
Materias:
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (898kB) | Vista Previa

Resumen

Un programa de ordenador puede considerarse como una función que lanza los individuos de un conjunto que se puede llamar "conjunto de estados de entrada" y otro conjunto que se puede denominar "conjunto de estados de salida". Si la función envía los elementos del "conjunto de entrada" dentro del "conjunto de salida" se dice que el programa representado por la función es correcto. El proceso de verificar la corrección de un programa se denomina "verificar el programa". Este es el objeto de este Proyecto Fin de Carrera. Confeccionar programas se puede considerar, según Gries, como un arte, pero también como una Ciencia. Casi todos los que programamos, en realidad, nos guiamos por intuiciones, costumbres u otros métodos como el coste tiempo-dinero de un programa, etc. A eso se le podría llamar arte. Lo que se presenta en este Proyecto es más bien una Ciencia de la programación, que utiliza metodologías exactas parecidas a las usadas en las Matemáticas o en las Ciencias Exactas como la Mecánica. Lo normal es programar como un arte, porque programar como una Ciencia llevaría a una pérdida de tiempo injustificada. La verificación como Ciencia es importante, sin embargo, en partes de los programas que requieren un esfuerzo detallado de verificación. Un ejemplo de estos métodos científicos es el de Wp (Precondición más débil), el cual es objeto de este Proyecto.

Más información

ID de Registro: 1680
Identificador DC: http://oa.upm.es/1680/
Identificador OAI: oai:oa.upm.es:1680
Depositado por: Archivo Digital UPM
Depositado el: 19 Jun 2009
Ultima Modificación: 20 Abr 2016 06:56
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM