Verificación de algoritmos y estructuras de datos en Dafny

Abstract

La verificación formal de un programa es la demostración de que este funciona de acuerdo a una descripción del comportamiento esperado en toda posible ejecución. La especificación de lo deseado puede utilizar técnicas diversas y entrar en mayor o menor detalle, pero para ganarse el título de formal esta ha de ser matemáticamente rigurosa. El estudio y ejercicio manual de alguna de esas técnicas forma parte del currículo común a los estudios de grado de la Facultad de Informática y del itinerario de Ciencias de la Computación de la Facultad de Ciencias Matemáticas de la Universidad Complutense de Madrid, como es el caso de la verificación con pre- y postcondiciones o lógica de Hoare. En el presente trabajo se explora la automatización de estos métodos mediante el lenguaje y verificador Dafny, con el que se especifican y verifican algoritmos y estructuras de datos de diversa complejidad. Dafny es un lenguaje de programación diseñado para integrar la especificación y permitir la verificación automática de sus programas, con la ayuda del programador y de un demostrador de teoremas en la sombra. Dafny es un proyecto en desarrollo activo aunque suficientemente maduro, que genera programas ejecutables.

The formal verification of a program is the proof that it works according to a description of its expected behaviour in any possible execution. The specification of what is desired can use different techniques and go into more or less detail, but to win the formal title it must be mathematically rigorous. The study and manual exercise of some of those techniques is part of the common curriculum of the degree studies at the School of Computer Science and of the Computer Science itinerary at the School of Mathematics at the Universidad Complutense de Madrid, such as verification with pre- and postconditions or Hoare logic. In the current work, the automation of those methods is explored through the language and verifier Dafny, with has been used to specify and verify some algorithms and data structures of diverse complexity. Dafny is a programming language designed to integrate specification and allow automatic verification of its programs, with the help of the programmer and a theorem prover in the shade. Dafny is in active development but mature enough and it generates executable programs.