Browsing by Author "Hernández Lorenzo, Matías Sebastián"

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    Lógica de programación con Dafny
    (Universidad ORT Uruguay, 2021) Hernández Lorenzo, Matías Sebastián; Tasistro Souto, Álvaro Daniel; Michelini Jorge, Juan Pedro; Szasz Cerutti, Nora Adriana
    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, 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.
  • Thumbnail Image
    Item
    Metodología de Programación con Dafny y KeY
    (Universidad ORT Uruguay, 2022) Hernández Lorenzo, Matías Sebastián; Drago Ciliano, Gianfranco; Tasistro Souto, Álvaro Daniel; Olsina Santos, Luis Antonio; Luna García, Carlos Daniel
    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.