Tasistro Souto, Álvaro Daniel2024-06-042024-06-042024Colina Candiota, C. S. & Armas Baison, G. de (2024). Mecanización de verificación formal de programas en Dafny (Proyecto) Universidad ORT Uruguay, Facultad de Ingeniería. Recuperado de https://rad.ort.edu.uy/handle/20.500.11968/6957https://hdl.handle.net/20.500.11968/6957Incluye bibliografía.El siguiente proyecto presenta un generador de condiciones de verificación que se ha desarrollado en Dafny, diseñado para un pequeño lenguaje imperativo. Este lenguaje incluye características como asignación múltiple, secuenciación, selección e iteración. El propósito fundamental de este generador es derivar, a partir de un programa anotado con pre y post condiciones, así como invariantes de cada iteración, un árbol de Hoare y condiciones de verificación asociadas. Se destaca que si las condiciones son demostradas, el programa resulta parcialmente correcto respecto a las pre y post condiciones dadas. Asimismo, se verifica que todo el programa compiló correctamente.36 p.PDFAcceso abiertoPROYECTOS-IDLENGUAJES DE PROGRAMACIÓN-DAFNYVERIFICACIÓN AUTOMÁTICAMÉTODOS FORMALESTrabajo final de carrera