Metodología de Programación con Dafny y KeY

Loading...
Thumbnail Image
Date
2022
Authors
Hernández Lorenzo, Matías Sebastián
Drago Ciliano, Gianfranco
Publisher
Universidad ORT Uruguay
DOI
ISSN
ISBN
URI
Abstract
El siguiente proyecto es una investigación que presenta el diseño de una metodología para la especificación y derivación de algoritmos iterativos expresados en código imperativo, utilizando las herramientas mecánicas KeY y Dafny para sus respectivas implementaciones. El enfoque metodológico pretende ayudar didácticamente a los lectores que están comenzando en el área de la verificación formal, para que estos puedan tener un pensamiento orientado a invariantes al momento de realizar algoritmos. A lo largo del proyecto se muestran diversos algoritmos; por ejemplo de división entera, potenciación, operaciones con arrays, búsquedas y ordenamiento, entre otros, utilizando la metodología diseñada y su correspondiente implementación en las dos herramientas KeY y Dafny. Como conclusión se obtiene una metodología propuesta que puede ser implementada en las materias Estructuras de Datos y Algoritmos 2 y en Lógica de la Programación, ambas de la carrera de Ingeniería en Sistemas de Universidad ORT Uruguay.
En
Thesis note
Proyecto (Carrera Universitaria). Universidad ORT Uruguay, Facultad de Ingeniería
Thesis degree name
Ingeniero en Sistemas
124 p. tbls.
Notes
Incluye bibliografía y anexos.
Subject
PROYECTOS-ID, INGENIERÍA DE SOFTWARE, VERIFICACIÓN AUTOMÁTICA, MÉTODOS FORMALES, LENGUAJES DE PROGRAMACIÓN-DAFNY
Type
Trabajo final de carrera
Access the full text
Citation
Hernández Lorenzo, M. S., & Drago Ciliano, G. (2022). Metodología de Programación con Dafny y KeY (Proyecto). Universidad ORT Uruguay, Facultad de Ingeniería.
Rights license