Browsing by Author "Pérez Pedetti, Santiago"

Now showing 1 - 1 of 1
  • Thumbnail Image
    Item
    Formalization of graphs in Dafny
    (Universidad ORT Uruguay, 2024) Bordagorry Burgueño, Juan Martín; Pérez Pedetti, Santiago; Tasistro Souto, Álvaro Daniel; Garbervetsky, Diego David; Calegari García, Daniel
    Dafny es un lenguaje orientado a especificaciones que provee un marco para verificar formalmente programas. En este proyecto, se presenta la experiencia de formalizar grafos y lograr la verificación parcial de algoritmos conocidos utilizando Dafny (Prim y Kruskal). En el cuerpo de este trabajo, también se presentan las pruebas de las secciones de los algoritmos que se verificaron, y cuales secciones fueron determinadas como trabajo a futuro. Se concluye que las especificaciones en Dafny son extremadamente poderosas si son bien ejecutadas, pero además requieren un conocimiento profundo de los algoritmos que se quiere especificar y de los problemas que resuelven, además de un manejo experto de Dafny para algoritmos complejos.