Se presenta el diseño de una metodología para la especificación y derivación de algoritmos iterativos expresados en código imperativo.
Se utilizan las herramientas mecánicas KeY y Dafny para sus respectivas implementaciones.
En el cuerpo de la tesis, se muestran diversos algoritmos utilizando la metodología diseñada y su correspondiente implementación en las dos herramientas mencionadas anteriormente.
-
Título: Ingeniería en Sistemas
-
Autores: Matías Hernández y Gianfranco Drago
-
Tutor: Álvaro Tasistro
-
Correctores: Carlos Luna y Luis Olsina
-
Entrega: 28/09/2022
-
Defensa: 03/10/2022