Verificación Formal de Programas
Verificación Formal de Programas
La verificación formal es un proceso utilizado para asegurarse de que un programa cumple con su especificación de forma rigurosa.
Triplas de Hoare
Las triplas de Hoare proveen un método para razonar sobre la corrección de los programas.
Precondiciones y postcondiciones
La estructura {P} C {Q} donde P y Q son afirmaciones lógicas y C es un comando.
Uso en bucles
Especial atención en los bucles para asegurar que la postcondición se mantenga tras la ejecución.
Ejemplos
Un ejemplo sería {x=0} x = x + 1 {x=1}, donde la precondición y postcondición son satisfechas.
Precondición más débil
Determina la condición más sencilla que debe satisfacer el estado inicial para que se cumpla la postcondición.
Definición
La condición más débil de una instrucción simple que garantiza la postcondición después de su ejecución.
Calculando PMD
La PMD para la asignación x := x + 1 y la postcondición {x=1} sería {x=0}.
Ejemplos
Ejemplos para instrucciones como asignaciones, comparaciones y operaciones aritméticas.
Teorema de invariancia
Fundamenta la razón por la cual ciertas propiedades se preservan a lo largo de la ejecución del programa.
Descripción
Afirma que si una propiedad invariante es verdadera antes de iniciar un ciclo, y si se mantiene en cada iteración, es verdadera al finalizar.
Aplicación
Se aplica generalmente para probar que los bucles no alteran las propiedades esenciales del programa.
Ejemplos
Demostrar que una variable contadora siempre se incrementa en cada iteración de un bucle.
Cota de ciclo
Establece una medida que decrece con cada iteración para asegurarse de que el bucle finalizará.
Función de cota
Una función de cota debe ser entera, positiva y decreciente en cada iteración.
Propósito
Garantiza la terminación de un bucle evitando ciclos infinitos.
Ejemplos
El número de elementos restantes por procesar en un arreglo puede ser una cota de ciclo.
Invariante de ciclo
Propiedades que se mantienen verdaderas antes y después de cada iteración de un bucle.
Concepto
La invariante ayuda a comprender y verificar el comportamiento del ciclo.
Utilidad
Es fundamental para demostrar la corrección parcial de bucles.
Ejemplos
Una invariante puede ser que la suma de los elementos procesados siempre es igual a un valor k.
Especificación de un programa
Define formalmente lo que el programa debe hacer, sirviendo como contrato entre el desarrollo y la verificación.
Requerimientos
Incluye precondiciones, postcondiciones y propiedades de los datos de entrada/salida.
Documentación
Sirve para documentar el comportamiento esperado y facilita la comunicación de las expectativas.
Ejemplos
Especificaciones para funciones matemáticas, manejo de errores, y condiciones de borde.