Introducción a la verificación de programas

Thumbnail Image
Date
2022-6
Authors
Rosenfeld, Ricardo Fabián
Journal Title
Journal ISSN
Volume Title
Publisher
Universidad Abierta Interamericana. Facultad de Tecnología Informática
Abstract
Iniciamos una serie de cuatro artículos introductorios sobre la verificación axiomática de programas, en el marco de los programas imperativos de entrada/salida. En este artículo introducimos el método axiomático de verificación para los programas secuenciales determinísticos, y desarrollamos ejemplos de aplicación. Si bien la verificación de programas se expone como una actividad a posteriori (dados un programa y una especificación, verificar que el programa satisface la especificación), la idea que se sostiene en el artículo, y en toda la serie, es tener en cuenta los axiomas y reglas del método para programar al mismo tiempo que verificar, de modo tal de obtener programas correctos por construcción. Con esta perspectiva, al final se ejemplifica un desarrollo sistemático de programa basado en la axiomática presentada.
Description
Keywords
programas, verificación axiomática
Citation
Rosenfeld, R. (2022). Introducción a la verificación de programas. En: Revista Abierta de Informática Aplicada (RAIA) 6(1):79-100