Tasistro Souto, Álvaro Daniel2022Herná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.Incluye bibliografía y anexos.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.124 p. tbls.PROYECTOS-IDINGENIERÍA DE SOFTWAREVERIFICACIÓN AUTOMÁTICAMÉTODOS FORMALESLENGUAJES DE PROGRAMACIÓN-DAFNYTrabajo final de carrera