Dafny 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, pre condiciones, post condiciones 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.
Como implicancia de esta tesis, se evaluará agregar Dafny en materias existentes del área de "Teoría de la computación" de la Universidad ORT Uruguay o la creación de una materia electiva con Dafny como principal herramienta de apoyo en el curso.
Título: Licenciado en Ingeniería de Software
Autor: Matías Hernández
Tutor: Álvaro Tasistro
Correctores: Juan Michelini y Nora Szasz
Entrega: 27/07/2021
Defensa: 19/08/2021
IDE: Visual Studio Code.
Extensions: Dafny.
Link: https://marketplace.visualstudio.com/items?itemName=correctnessLab.dafny-vscode
Right click on the .dfy file you want to run, then click on Dafny: Compile and Run.