Verificación de algoritmos y estructuras de datos en Dafny
Contribuinte(s) |
Martí Oliet, Narciso Pita Andreu, Isabel Verdejo López, Alberto |
---|---|
Data(s) |
2016
|
Resumo |
La verificación formal de un programa es la demostración de que este funciona de acuerdo a una descripción del comportamiento esperado en toda posible ejecución. La especificación de lo deseado puede utilizar técnicas diversas y entrar en mayor o menor detalle, pero para ganarse el título de formal esta ha de ser matemáticamente rigurosa. El estudio y ejercicio manual de alguna de esas técnicas forma parte del currículo común a los estudios de grado de la Facultad de Informática y del itinerario de Ciencias de la Computación de la Facultad de Ciencias Matemáticas de la Universidad Complutense de Madrid, como es el caso de la verificación con pre- y postcondiciones o lógica de Hoare. En el presente trabajo se explora la automatización de estos métodos mediante el lenguaje y verificador Dafny, con el que se especifican y verifican algoritmos y estructuras de datos de diversa complejidad. Dafny es un lenguaje de programación diseñado para integrar la especificación y permitir la verificación automática de sus programas, con la ayuda del programador y de un demostrador de teoremas en la sombra. Dafny es un proyecto en desarrollo activo aunque suficientemente maduro, que genera programas ejecutables. |
Formato |
application/pdf |
Identificador | |
Idioma(s) |
en |
Relação |
http://eprints.ucm.es/38702/ |
Direitos |
info:eu-repo/semantics/openAccess |
Palavras-Chave | #Lenguajes de programación #Lógica simbólica y matemática |
Tipo |
info:eu-repo/semantics/bachelorThesis PeerReviewed |