Lógica de programación con Dafny

Simple item page
dc.contributor.advisorTasistro Souto, Álvaro Daniel
dc.contributor.tribunalMichelini Jorge, Juan Pedro
dc.contributor.tribunalSzasz Cerutti, Nora Adriana
dc.creatorHernández Lorenzo, Matías Sebastián
dc.date.issued2021
dc.descriptionIncluye bibliografía.
dc.description.abstractDafny es un lenguaje diseñado por K. Rustan M. Leino en “Microsoft Research” que soporta la especificación formal de código a través del uso de invariantes, precondiciones, postcondiciones y lemas (propiedades). Se realizó una búsqueda de aplicaciones de Dafny a nivel educativo y se encontró que el “Imperial College London” introduce a sus alumnos el concepto de verificación completa de especificaciones de programas utilizando Dafny, lo cual motivó a realizar esta investigación para evaluar la aplicabilidad del lenguaje Dafny para entornos académicos. Para poder realizar la evaluación, se estarán abordando implementaciones de diferentes algoritmos conocidos de ordenamiento y búsqueda, junto a lemas que verifican sus propiedades. Las demostraciones se realizarán utilizando inducción y “calculations” los cuales permiten realizar demostraciones muy intuitivas. Como metodología de desarrollo, se estará aplicando la metodología vista en “Fundamentos de la computación" para los algoritmos funcionales e invariantes al estilo Dijkstra para los algoritmos iterativos. Para finalizar, se analizará también a Dafny como herramienta productiva, reescribiendo los lemas del módulo educativo a su mínima expresión para evaluar el potencial del compilador de Dafny y por ende su aplicabilidad en entornos productivos. Se concluirá que Dafny tiene mucho potencial principalmente como herramienta educativa, pero además cierto nicho de mercado también podría beneficiarse del potencial del compilador en un entorno productivo.
dc.format.extent64 p.
dc.identifier.citationHernández Lorenzo, M. S. (2021). Lógica de programación con Dafny (Trabajo Integrador). Universidad ORT Uruguay, Facultad de Ingeniería.
dc.languageEspañol.
dc.publisherUniversidad ORT Uruguay
dc.relation.otherhttps://sisbibliotecas.ort.edu.uy/bib/91848
dc.subjectPROYECTOS-ID
dc.subjectESTRUCTURAS DE DATOS
dc.subjectVERIFICACIÓN AUTOMÁTICA
dc.titleLógica de programación con Dafny
dc.typeTrabajo final de carrera
ort.thesis.careerFI - Licenciatura en Ingeniería de software - ID
ort.thesis.degreegrantorFacultad de Ingeniería
ort.thesis.degreelevelCarrera Universitaria
ort.thesis.degreenameLicenciado en Ingeniería de Software
ort.thesis.degreetypeTrabajo Integrador
ort.thesis.noteTrabajo Integrador (Carrera Universitaria). Universidad ORT Uruguay, Facultad de Ingeniería
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Material completo.pdf
Size:
418.97 KB
Format:
Adobe Portable Document Format
Description:
description
Download
Collections
Trabajos finales de carrera de grado