Browsing by Author "Armas Baison, Guillermo de"

Now showing 1 - 1 of 1
  • Thumbnail Image
    Item
    Mecanización de verificación formal de programas en Dafny
    (Universidad ORT Uruguay, 2024) Colina Candiota, Cristian Sebastián; Armas Baison, Guillermo de; Tasistro Souto, Álvaro Daniel; Garbervetsky, Diego David; Calegari García, Daniel
    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.